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 NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

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

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

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

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

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

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

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

a__and^#(tt,X)	→	mark^#(X)	(37)
a__isNat^#(plus(V1,V2))	→	a__isNat^#(V1)	(45)
a__isNat^#(plus(V1,V2))	→	a__and^#(a__isNat(V1),isNat(V2))	(36)
mark^#(and(X1,X2))	→	mark^#(X1)	(29)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(26)
mark^#(isNat(X))	→	a__isNat^#(X)	(34)
a__isNat^#(s(V1))	→	a__isNat^#(V1)	(44)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__plus(x₁, x₂)]	=	x₁ + x₂ + 70
[U21(x₁, x₂, x₃)]	=	x₂ + x₃ + 74
[U11(x₁, x₂)]	=	x₁ + 2449
[s(x₁)]	=	x₁ + 1
[a__isNat^#(x₁)]	=	x₁ + 20586
[and(x₁, x₂)]	=	x₁ + x₂ + 2
[a__U11^#(x₁, x₂)]	=	1
[a__U21^#(x₁, x₂, x₃)]	=	1
[a__plus^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	146
[a__and^#(x₁, x₂)]	=	x₂ + 1
[a__U21(x₁, x₂, x₃)]	=	77
[mark(x₁)]	=	x₁ + 3
[a__U11(x₁, x₂)]	=	x₂ + 2453
[isNat(x₁)]	=	x₁ + 20587
[plus(x₁, x₂)]	=	x₁ + x₂ + 71
[tt]	=	0
[a__isNat(x₁)]	=	2
[a__and(x₁, x₂)]	=	2

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

a__and^#(tt,X)	→	mark^#(X)	(37)
a__isNat^#(plus(V1,V2))	→	a__isNat^#(V1)	(45)
a__isNat^#(plus(V1,V2))	→	a__and^#(a__isNat(V1),isNat(V2))	(36)
mark^#(and(X1,X2))	→	mark^#(X1)	(29)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(26)
mark^#(isNat(X))	→	a__isNat^#(X)	(34)
a__isNat^#(s(V1))	→	a__isNat^#(V1)	(44)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.