Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PEANO_nokinds_GM)

The rewrite relation of the following TRS is considered.

a__U11(tt,N)	→	mark(N)	(1)
a__U21(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(2)
a__and(tt,X)	→	mark(X)	(3)
a__isNat(0)	→	tt	(4)
a__isNat(plus(V1,V2))	→	a__and(a__isNat(V1),isNat(V2))	(5)
a__isNat(s(V1))	→	a__isNat(V1)	(6)
a__plus(N,0)	→	a__U11(a__isNat(N),N)	(7)
a__plus(N,s(M))	→	a__U21(a__and(a__isNat(M),isNat(N)),M,N)	(8)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(9)
mark(U21(X1,X2,X3))	→	a__U21(mark(X1),X2,X3)	(10)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(11)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(12)
mark(isNat(X))	→	a__isNat(X)	(13)
mark(tt)	→	tt	(14)
mark(s(X))	→	s(mark(X))	(15)
mark(0)	→	0	(16)
a__U11(X1,X2)	→	U11(X1,X2)	(17)
a__U21(X1,X2,X3)	→	U21(X1,X2,X3)	(18)
a__plus(X1,X2)	→	plus(X1,X2)	(19)
a__and(X1,X2)	→	and(X1,X2)	(20)
a__isNat(X)	→	isNat(X)	(21)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

a__U11^#(tt,N)	→	mark^#(N)	(22)
a__U21^#(tt,M,N)	→	mark^#(M)	(23)
a__U21^#(tt,M,N)	→	mark^#(N)	(24)
a__U21^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(25)
a__and^#(tt,X)	→	mark^#(X)	(26)
a__isNat^#(plus(V1,V2))	→	a__isNat^#(V1)	(27)
a__isNat^#(plus(V1,V2))	→	a__and^#(a__isNat(V1),isNat(V2))	(28)
a__isNat^#(s(V1))	→	a__isNat^#(V1)	(29)
a__plus^#(N,0)	→	a__isNat^#(N)	(30)
a__plus^#(N,0)	→	a__U11^#(a__isNat(N),N)	(31)
a__plus^#(N,s(M))	→	a__isNat^#(M)	(32)
a__plus^#(N,s(M))	→	a__and^#(a__isNat(M),isNat(N))	(33)
a__plus^#(N,s(M))	→	a__U21^#(a__and(a__isNat(M),isNat(N)),M,N)	(34)
mark^#(U11(X1,X2))	→	mark^#(X1)	(35)
mark^#(U11(X1,X2))	→	a__U11^#(mark(X1),X2)	(36)
mark^#(U21(X1,X2,X3))	→	mark^#(X1)	(37)
mark^#(U21(X1,X2,X3))	→	a__U21^#(mark(X1),X2,X3)	(38)
mark^#(plus(X1,X2))	→	mark^#(X2)	(39)
mark^#(plus(X1,X2))	→	mark^#(X1)	(40)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(41)
mark^#(and(X1,X2))	→	mark^#(X1)	(42)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(43)
mark^#(isNat(X))	→	a__isNat^#(X)	(44)
mark^#(s(X))	→	mark^#(X)	(45)

1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the rationals with delta = 1/64

[a__and^#(x₁, x₂)]	=	0 · x₁ + 1/2 · x₂ + 0
[a__plus(x₁, x₂)]	=	2 · x₁ + 2 · x₂ + 1
[mark^#(x₁)]	=	1/2 · x₁ + 0
[a__isNat(x₁)]	=	0 · x₁ + 0
[a__U11(x₁, x₂)]	=	1 · x₁ + 1 · x₂ + 0
[a__U21(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃ + 3
[a__U21^#(x₁, x₂, x₃)]	=	0 · x₁ + 1/2 · x₂ + 1/2 · x₃ + 3/2
[a__isNat^#(x₁)]	=	0 · x₁ + 0
[a__plus^#(x₁, x₂)]	=	1/2 · x₁ + 1/2 · x₂ + 1/2
[s(x₁)]	=	1 · x₁ + 2
[isNat(x₁)]	=	0 · x₁ + 0
[tt]	=	0
[0]	=	0
[a__U11^#(x₁, x₂)]	=	0 · x₁ + 1/2 · x₂ + 0
[U21(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃ + 3
[U11(x₁, x₂)]	=	1 · x₁ + 1 · x₂ + 0
[plus(x₁, x₂)]	=	2 · x₁ + 2 · x₂ + 1
[and(x₁, x₂)]	=	1 · x₁ + 1 · x₂ + 0
[a__and(x₁, x₂)]	=	1 · x₁ + 1 · x₂ + 0
[mark(x₁)]	=	1 · x₁ + 0

together with the usable rules

a__U11(tt,N)	→	mark(N)	(1)
a__U21(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(2)
a__and(tt,X)	→	mark(X)	(3)
a__isNat(0)	→	tt	(4)
a__isNat(plus(V1,V2))	→	a__and(a__isNat(V1),isNat(V2))	(5)
a__isNat(s(V1))	→	a__isNat(V1)	(6)
a__plus(N,0)	→	a__U11(a__isNat(N),N)	(7)
a__plus(N,s(M))	→	a__U21(a__and(a__isNat(M),isNat(N)),M,N)	(8)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(9)
mark(U21(X1,X2,X3))	→	a__U21(mark(X1),X2,X3)	(10)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(11)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(12)
mark(isNat(X))	→	a__isNat(X)	(13)
mark(tt)	→	tt	(14)
mark(s(X))	→	s(mark(X))	(15)
mark(0)	→	0	(16)
a__U11(X1,X2)	→	U11(X1,X2)	(17)
a__U21(X1,X2,X3)	→	U21(X1,X2,X3)	(18)
a__plus(X1,X2)	→	plus(X1,X2)	(19)
a__and(X1,X2)	→	and(X1,X2)	(20)
a__isNat(X)	→	isNat(X)	(21)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

a__U21^#(tt,M,N)	→	mark^#(M)	(23)
a__U21^#(tt,M,N)	→	mark^#(N)	(24)
a__U21^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(25)
a__plus^#(N,0)	→	a__isNat^#(N)	(30)
a__plus^#(N,0)	→	a__U11^#(a__isNat(N),N)	(31)
a__plus^#(N,s(M))	→	a__isNat^#(M)	(32)
a__plus^#(N,s(M))	→	a__and^#(a__isNat(M),isNat(N))	(33)
mark^#(U21(X1,X2,X3))	→	mark^#(X1)	(37)
mark^#(plus(X1,X2))	→	mark^#(X2)	(39)
mark^#(plus(X1,X2))	→	mark^#(X1)	(40)
mark^#(s(X))	→	mark^#(X)	(45)

could be deleted.

1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

a__isNat^#(plus(V1,V2))	→	a__isNat^#(V1)	(27)
a__isNat^#(plus(V1,V2))	→	a__and^#(a__isNat(V1),isNat(V2))	(28)
a__and^#(tt,X)	→	mark^#(X)	(26)
mark^#(U11(X1,X2))	→	mark^#(X1)	(35)
mark^#(U11(X1,X2))	→	a__U11^#(mark(X1),X2)	(36)
a__U11^#(tt,N)	→	mark^#(N)	(22)
mark^#(and(X1,X2))	→	mark^#(X1)	(42)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(43)
mark^#(isNat(X))	→	a__isNat^#(X)	(44)
a__isNat^#(s(V1))	→	a__isNat^#(V1)	(29)

1.1.1.1 Subterm Criterion Processor

We use the projection to multisets

π(a__isNat^#)	=	{ 1 }
π(a__and^#)	=	{ 2 }
π(mark^#)	=	{ 1 }
π(a__U11^#)	=	{ 2 }
π(isNat)	=	{ 1 }

to remove the pairs:

a__isNat^#(plus(V1,V2))	→	a__isNat^#(V1)	(27)
a__isNat^#(plus(V1,V2))	→	a__and^#(a__isNat(V1),isNat(V2))	(28)
mark^#(U11(X1,X2))	→	mark^#(X1)	(35)
mark^#(U11(X1,X2))	→	a__U11^#(mark(X1),X2)	(36)
mark^#(and(X1,X2))	→	mark^#(X1)	(42)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(43)
a__isNat^#(s(V1))	→	a__isNat^#(V1)	(29)

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.