Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PEANO_nokinds_Z)

The rewrite relation of the following TRS is considered.

U11(tt,N)	→	activate(N)	(1)
U21(tt,M,N)	→	s(plus(activate(N),activate(M)))	(2)
and(tt,X)	→	activate(X)	(3)
isNat(n__0)	→	tt	(4)
isNat(n__plus(V1,V2))	→	and(isNat(activate(V1)),n__isNat(activate(V2)))	(5)
isNat(n__s(V1))	→	isNat(activate(V1))	(6)
plus(N,0)	→	U11(isNat(N),N)	(7)
plus(N,s(M))	→	U21(and(isNat(M),n__isNat(N)),M,N)	(8)
0	→	n__0	(9)
plus(X1,X2)	→	n__plus(X1,X2)	(10)
isNat(X)	→	n__isNat(X)	(11)
s(X)	→	n__s(X)	(12)
activate(n__0)	→	0	(13)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(14)
activate(n__isNat(X))	→	isNat(X)	(15)
activate(n__s(X))	→	s(X)	(16)
activate(X)	→	X	(17)

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.

U11^#(tt,N)	→	activate^#(N)	(18)
U21^#(tt,M,N)	→	activate^#(M)	(19)
U21^#(tt,M,N)	→	activate^#(N)	(20)
U21^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(21)
U21^#(tt,M,N)	→	s^#(plus(activate(N),activate(M)))	(22)
and^#(tt,X)	→	activate^#(X)	(23)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(24)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(25)
isNat^#(n__plus(V1,V2))	→	isNat^#(activate(V1))	(26)
isNat^#(n__plus(V1,V2))	→	and^#(isNat(activate(V1)),n__isNat(activate(V2)))	(27)
isNat^#(n__s(V1))	→	activate^#(V1)	(28)
isNat^#(n__s(V1))	→	isNat^#(activate(V1))	(29)
plus^#(N,0)	→	isNat^#(N)	(30)
plus^#(N,0)	→	U11^#(isNat(N),N)	(31)
plus^#(N,s(M))	→	isNat^#(M)	(32)
plus^#(N,s(M))	→	and^#(isNat(M),n__isNat(N))	(33)
plus^#(N,s(M))	→	U21^#(and(isNat(M),n__isNat(N)),M,N)	(34)
activate^#(n__0)	→	0^#	(35)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(36)
activate^#(n__isNat(X))	→	isNat^#(X)	(37)
activate^#(n__s(X))	→	s^#(X)	(38)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

isNat^#(n__s(V1))	→	isNat^#(activate(V1))	(29)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(24)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(36)
plus^#(N,0)	→	isNat^#(N)	(30)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(25)
activate^#(n__isNat(X))	→	isNat^#(X)	(37)
isNat^#(n__plus(V1,V2))	→	isNat^#(activate(V1))	(26)
isNat^#(n__plus(V1,V2))	→	and^#(isNat(activate(V1)),n__isNat(activate(V2)))	(27)
and^#(tt,X)	→	activate^#(X)	(23)
isNat^#(n__s(V1))	→	activate^#(V1)	(28)
plus^#(N,0)	→	U11^#(isNat(N),N)	(31)
U11^#(tt,N)	→	activate^#(N)	(18)
plus^#(N,s(M))	→	isNat^#(M)	(32)
plus^#(N,s(M))	→	and^#(isNat(M),n__isNat(N))	(33)
plus^#(N,s(M))	→	U21^#(and(isNat(M),n__isNat(N)),M,N)	(34)
U21^#(tt,M,N)	→	activate^#(M)	(19)
U21^#(tt,M,N)	→	activate^#(N)	(20)
U21^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(21)

1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[and^#(x₁, x₂)]	=	0 · x₁ + 3 · x₂ + -∞
[plus(x₁, x₂)]	=	2 · x₁ + 2 · x₂ + 0
[U21^#(x₁, x₂, x₃)]	=	-∞ · x₁ + 5 · x₂ + 4 · x₃ + -∞
[isNat(x₁)]	=	0 · x₁ + -∞
[U11(x₁, x₂)]	=	0 · x₁ + 2 · x₂ + 2
[U21(x₁, x₂, x₃)]	=	-∞ · x₁ + 2 · x₂ + 2 · x₃ + 3
[plus^#(x₁, x₂)]	=	4 · x₁ + 5 · x₂ + -∞
[isNat^#(x₁)]	=	3 · x₁ + -∞
[s(x₁)]	=	0 · x₁ + 1
[n__isNat(x₁)]	=	0 · x₁ + -∞
[tt]	=	0
[n__0]	=	0
[activate^#(x₁)]	=	3 · x₁ + -∞
[0]	=	0
[n__s(x₁)]	=	0 · x₁ + 1
[n__plus(x₁, x₂)]	=	2 · x₁ + 2 · x₂ + 0
[U11^#(x₁, x₂)]	=	-∞ · x₁ + 4 · x₂ + 0
[and(x₁, x₂)]	=	1 · x₁ + 2 · x₂ + -∞
[activate(x₁)]	=	0 · x₁ + -∞

together with the usable rules

U11(tt,N)	→	activate(N)	(1)
U21(tt,M,N)	→	s(plus(activate(N),activate(M)))	(2)
and(tt,X)	→	activate(X)	(3)
isNat(n__0)	→	tt	(4)
isNat(n__plus(V1,V2))	→	and(isNat(activate(V1)),n__isNat(activate(V2)))	(5)
isNat(n__s(V1))	→	isNat(activate(V1))	(6)
plus(N,0)	→	U11(isNat(N),N)	(7)
plus(N,s(M))	→	U21(and(isNat(M),n__isNat(N)),M,N)	(8)
0	→	n__0	(9)
plus(X1,X2)	→	n__plus(X1,X2)	(10)
isNat(X)	→	n__isNat(X)	(11)
s(X)	→	n__s(X)	(12)
activate(n__0)	→	0	(13)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(14)
activate(n__isNat(X))	→	isNat(X)	(15)
activate(n__s(X))	→	s(X)	(16)
activate(X)	→	X	(17)

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

isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(24)
plus^#(N,0)	→	isNat^#(N)	(30)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(25)
isNat^#(n__plus(V1,V2))	→	isNat^#(activate(V1))	(26)
isNat^#(n__plus(V1,V2))	→	and^#(isNat(activate(V1)),n__isNat(activate(V2)))	(27)
U11^#(tt,N)	→	activate^#(N)	(18)
plus^#(N,s(M))	→	isNat^#(M)	(32)
plus^#(N,s(M))	→	and^#(isNat(M),n__isNat(N))	(33)
U21^#(tt,M,N)	→	activate^#(M)	(19)
U21^#(tt,M,N)	→	activate^#(N)	(20)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

isNat^#(n__s(V1))	→	isNat^#(activate(V1))	(29)
isNat^#(n__s(V1))	→	activate^#(V1)	(28)
activate^#(n__isNat(X))	→	isNat^#(X)	(37)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[plus(x₁, x₂)]	=	4 · x₁ + 5 · x₂ + 5
[isNat(x₁)]	=	2 · x₁ + 2
[U11(x₁, x₂)]	=	-∞ · x₁ + 4 · x₂ + 7
[U21(x₁, x₂, x₃)]	=	-∞ · x₁ + 5 · x₂ + 4 · x₃ + 5
[isNat^#(x₁)]	=	2 · x₁ + 2
[s(x₁)]	=	0 · x₁ + 0
[n__isNat(x₁)]	=	2 · x₁ + 2
[tt]	=	2
[n__0]	=	2
[activate^#(x₁)]	=	2 · x₁ + -∞
[0]	=	2
[n__s(x₁)]	=	0 · x₁ + 0
[n__plus(x₁, x₂)]	=	4 · x₁ + 5 · x₂ + 5
[and(x₁, x₂)]	=	2 · x₁ + 5 · x₂ + 0
[activate(x₁)]	=	0 · x₁ + -∞

together with the usable rules

U11(tt,N)	→	activate(N)	(1)
U21(tt,M,N)	→	s(plus(activate(N),activate(M)))	(2)
and(tt,X)	→	activate(X)	(3)
isNat(n__0)	→	tt	(4)
isNat(n__plus(V1,V2))	→	and(isNat(activate(V1)),n__isNat(activate(V2)))	(5)
isNat(n__s(V1))	→	isNat(activate(V1))	(6)
plus(N,0)	→	U11(isNat(N),N)	(7)
plus(N,s(M))	→	U21(and(isNat(M),n__isNat(N)),M,N)	(8)
0	→	n__0	(9)
plus(X1,X2)	→	n__plus(X1,X2)	(10)
isNat(X)	→	n__isNat(X)	(11)
s(X)	→	n__s(X)	(12)
activate(n__0)	→	0	(13)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(14)
activate(n__isNat(X))	→	isNat(X)	(15)
activate(n__s(X))	→	s(X)	(16)
activate(X)	→	X	(17)

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

activate^#(n__isNat(X))

→

isNat^#(X)

(37)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

isNat^#(n__s(V1))

→

isNat^#(activate(V1))

(29)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[plus(x₁, x₂)]	=	2 · x₁ + 3 · x₂ + 0
[isNat(x₁)]	=	2 · x₁ + 0
[U11(x₁, x₂)]	=	0 · x₁ + 2 · x₂ + 0
[U21(x₁, x₂, x₃)]	=	0 · x₁ + 3 · x₂ + 2 · x₃ + 1
[isNat^#(x₁)]	=	1 · x₁ + 6
[s(x₁)]	=	1 · x₁ + 1
[n__isNat(x₁)]	=	2 · x₁ + 0
[tt]	=	1
[n__0]	=	4
[0]	=	4
[n__s(x₁)]	=	1 · x₁ + 1
[n__plus(x₁, x₂)]	=	2 · x₁ + 3 · x₂ + 0
[and(x₁, x₂)]	=	1 · x₁ + 2 · x₂ + 0
[activate(x₁)]	=	1 · x₁ + 0

together with the usable rules

U11(tt,N)	→	activate(N)	(1)
U21(tt,M,N)	→	s(plus(activate(N),activate(M)))	(2)
and(tt,X)	→	activate(X)	(3)
isNat(n__0)	→	tt	(4)
isNat(n__plus(V1,V2))	→	and(isNat(activate(V1)),n__isNat(activate(V2)))	(5)
isNat(n__s(V1))	→	isNat(activate(V1))	(6)
plus(N,0)	→	U11(isNat(N),N)	(7)
plus(N,s(M))	→	U21(and(isNat(M),n__isNat(N)),M,N)	(8)
0	→	n__0	(9)
plus(X1,X2)	→	n__plus(X1,X2)	(10)
isNat(X)	→	n__isNat(X)	(11)
s(X)	→	n__s(X)	(12)
activate(n__0)	→	0	(13)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(14)
activate(n__isNat(X))	→	isNat(X)	(15)
activate(n__s(X))	→	s(X)	(16)
activate(X)	→	X	(17)

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

isNat^#(n__s(V1))

→

isNat^#(activate(V1))

(29)

could be deleted.

1.1.1.1.1.1.1.1 P is empty

There are no pairs anymore.

The 2^nd component contains the pair

plus^#(N,s(M))	→	U21^#(and(isNat(M),n__isNat(N)),M,N)	(34)
U21^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(21)

1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[plus(x₁, x₂)]	=	2 · x₁ + 1 · x₂ + 2
[U21^#(x₁, x₂, x₃)]	=	0 · x₁ + 1 · x₂ + 0 · x₃ + 2
[isNat(x₁)]	=	0 · x₁ + 0
[U11(x₁, x₂)]	=	0 · x₁ + 2 · x₂ + 1
[U21(x₁, x₂, x₃)]	=	0 · x₁ + 1 · x₂ + 2 · x₃ + 6
[plus^#(x₁, x₂)]	=	0 · x₁ + 1 · x₂ + 2
[s(x₁)]	=	1 · x₁ + 4
[n__isNat(x₁)]	=	0 · x₁ + 0
[tt]	=	0
[n__0]	=	0
[0]	=	0
[n__s(x₁)]	=	1 · x₁ + 4
[n__plus(x₁, x₂)]	=	2 · x₁ + 1 · x₂ + 2
[and(x₁, x₂)]	=	0 · x₁ + 4 · x₂ + 0
[activate(x₁)]	=	1 · x₁ + 0

together with the usable rules

U11(tt,N)	→	activate(N)	(1)
U21(tt,M,N)	→	s(plus(activate(N),activate(M)))	(2)
and(tt,X)	→	activate(X)	(3)
isNat(n__0)	→	tt	(4)
isNat(n__plus(V1,V2))	→	and(isNat(activate(V1)),n__isNat(activate(V2)))	(5)
isNat(n__s(V1))	→	isNat(activate(V1))	(6)
plus(N,0)	→	U11(isNat(N),N)	(7)
plus(N,s(M))	→	U21(and(isNat(M),n__isNat(N)),M,N)	(8)
0	→	n__0	(9)
plus(X1,X2)	→	n__plus(X1,X2)	(10)
isNat(X)	→	n__isNat(X)	(11)
s(X)	→	n__s(X)	(12)
activate(n__0)	→	0	(13)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(14)
activate(n__isNat(X))	→	isNat(X)	(15)
activate(n__s(X))	→	s(X)	(16)
activate(X)	→	X	(17)

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

plus^#(N,s(M))

→

U21^#(and(isNat(M),n__isNat(N)),M,N)

(34)

could be deleted.

1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.