Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExAppendixB_AEL03_FR)

The rewrite relation of the following TRS is considered.

from(X)	→	cons(X,n__from(n__s(X)))	(1)
2ndspos(0,Z)	→	rnil	(2)
2ndspos(s(N),cons(X,Z))	→	2ndspos(s(N),cons2(X,activate(Z)))	(3)
2ndspos(s(N),cons2(X,cons(Y,Z)))	→	rcons(posrecip(Y),2ndsneg(N,activate(Z)))	(4)
2ndsneg(0,Z)	→	rnil	(5)
2ndsneg(s(N),cons(X,Z))	→	2ndsneg(s(N),cons2(X,activate(Z)))	(6)
2ndsneg(s(N),cons2(X,cons(Y,Z)))	→	rcons(negrecip(Y),2ndspos(N,activate(Z)))	(7)
pi(X)	→	2ndspos(X,from(0))	(8)
plus(0,Y)	→	Y	(9)
plus(s(X),Y)	→	s(plus(X,Y))	(10)
times(0,Y)	→	0	(11)
times(s(X),Y)	→	plus(Y,times(X,Y))	(12)
square(X)	→	times(X,X)	(13)
from(X)	→	n__from(X)	(14)
s(X)	→	n__s(X)	(15)
activate(n__from(X))	→	from(activate(X))	(16)
activate(n__s(X))	→	s(activate(X))	(17)
activate(X)	→	X	(18)

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.

2ndsneg^#(s(N),cons(X,Z))	→	activate^#(Z)	(19)
2ndsneg^#(s(N),cons2(X,cons(Y,Z)))	→	2ndspos^#(N,activate(Z))	(20)
activate^#(n__from(X))	→	activate^#(X)	(21)
plus^#(s(X),Y)	→	plus^#(X,Y)	(22)
activate^#(n__s(X))	→	activate^#(X)	(23)
activate^#(n__from(X))	→	from^#(activate(X))	(24)
2ndspos^#(s(N),cons(X,Z))	→	2ndspos^#(s(N),cons2(X,activate(Z)))	(25)
2ndsneg^#(s(N),cons2(X,cons(Y,Z)))	→	activate^#(Z)	(26)
activate^#(n__s(X))	→	s^#(activate(X))	(27)
times^#(s(X),Y)	→	times^#(X,Y)	(28)
pi^#(X)	→	from^#(0)	(29)
2ndspos^#(s(N),cons2(X,cons(Y,Z)))	→	activate^#(Z)	(30)
pi^#(X)	→	2ndspos^#(X,from(0))	(31)
square^#(X)	→	times^#(X,X)	(32)
2ndsneg^#(s(N),cons(X,Z))	→	2ndsneg^#(s(N),cons2(X,activate(Z)))	(33)
plus^#(s(X),Y)	→	s^#(plus(X,Y))	(34)
2ndspos^#(s(N),cons(X,Z))	→	activate^#(Z)	(35)
times^#(s(X),Y)	→	plus^#(Y,times(X,Y))	(36)
2ndspos^#(s(N),cons2(X,cons(Y,Z)))	→	2ndsneg^#(N,activate(Z))	(37)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.

The 1^st component contains the pair

2ndspos^#(s(N),cons2(X,cons(Y,Z)))	→	2ndsneg^#(N,activate(Z))	(37)
2ndspos^#(s(N),cons(X,Z))	→	2ndspos^#(s(N),cons2(X,activate(Z)))	(25)
2ndsneg^#(s(N),cons(X,Z))	→	2ndsneg^#(s(N),cons2(X,activate(Z)))	(33)
2ndsneg^#(s(N),cons2(X,cons(Y,Z)))	→	2ndspos^#(N,activate(Z))	(20)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[negrecip(x₁)]	=	0
[s(x₁)]	=	x₁ + 1
[2ndspos(x₁, x₂)]	=	0
[activate(x₁)]	=	1
[rnil]	=	0
[plus^#(x₁, x₂)]	=	0
[n__from(x₁)]	=	3
[square(x₁)]	=	0
[activate^#(x₁)]	=	0
[square^#(x₁)]	=	0
[pi(x₁)]	=	0
[rcons(x₁, x₂)]	=	0
[n__s(x₁)]	=	x₁ + 1
[times^#(x₁, x₂)]	=	0
[0]	=	0
[from(x₁)]	=	2
[times(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[2ndsneg(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[2ndspos^#(x₁, x₂)]	=	x₁ + 0
[cons2(x₁, x₂)]	=	1
[from^#(x₁)]	=	0
[cons(x₁, x₂)]	=	3
[pi^#(x₁)]	=	0
[2ndsneg^#(x₁, x₂)]	=	x₁ + 0
[posrecip(x₁)]	=	0

together with the usable rule

s(X)

→

n__s(X)

(15)

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

2ndspos^#(s(N),cons2(X,cons(Y,Z)))	→	2ndsneg^#(N,activate(Z))	(37)
2ndsneg^#(s(N),cons2(X,cons(Y,Z)))	→	2ndspos^#(N,activate(Z))	(20)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

times^#(s(X),Y)

→

times^#(X,Y)

(28)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[negrecip(x₁)]	=	0
[s(x₁)]	=	x₁ + 3
[2ndspos(x₁, x₂)]	=	0
[activate(x₁)]	=	1
[rnil]	=	0
[plus^#(x₁, x₂)]	=	0
[n__from(x₁)]	=	3
[square(x₁)]	=	0
[activate^#(x₁)]	=	0
[square^#(x₁)]	=	0
[pi(x₁)]	=	0
[rcons(x₁, x₂)]	=	0
[n__s(x₁)]	=	x₁ + 1
[times^#(x₁, x₂)]	=	x₁ + 0
[0]	=	0
[from(x₁)]	=	2
[times(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[2ndsneg(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[2ndspos^#(x₁, x₂)]	=	x₁ + 0
[cons2(x₁, x₂)]	=	1
[from^#(x₁)]	=	0
[cons(x₁, x₂)]	=	3
[pi^#(x₁)]	=	0
[2ndsneg^#(x₁, x₂)]	=	x₁ + 0
[posrecip(x₁)]	=	0

together with the usable rule

s(X)

→

n__s(X)

(15)

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

times^#(s(X),Y)

→

times^#(X,Y)

(28)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

plus^#(s(X),Y)

→

plus^#(X,Y)

(22)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[negrecip(x₁)]	=	0
[s(x₁)]	=	x₁ + 3
[2ndspos(x₁, x₂)]	=	0
[activate(x₁)]	=	1
[rnil]	=	0
[plus^#(x₁, x₂)]	=	x₁ + 0
[n__from(x₁)]	=	3
[square(x₁)]	=	0
[activate^#(x₁)]	=	0
[square^#(x₁)]	=	0
[pi(x₁)]	=	0
[rcons(x₁, x₂)]	=	0
[n__s(x₁)]	=	x₁ + 1
[times^#(x₁, x₂)]	=	0
[0]	=	0
[from(x₁)]	=	2
[times(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[2ndsneg(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[2ndspos^#(x₁, x₂)]	=	x₁ + 0
[cons2(x₁, x₂)]	=	1
[from^#(x₁)]	=	0
[cons(x₁, x₂)]	=	3
[pi^#(x₁)]	=	0
[2ndsneg^#(x₁, x₂)]	=	x₁ + 0
[posrecip(x₁)]	=	0

together with the usable rule

s(X)

→

n__s(X)

(15)

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

plus^#(s(X),Y)

→

plus^#(X,Y)

(22)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 4^th component contains the pair

activate^#(n__s(X))	→	activate^#(X)	(23)
activate^#(n__from(X))	→	activate^#(X)	(21)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[negrecip(x₁)]	=	0
[s(x₁)]	=	x₁ + 1
[2ndspos(x₁, x₂)]	=	0
[activate(x₁)]	=	1
[rnil]	=	0
[plus^#(x₁, x₂)]	=	0
[n__from(x₁)]	=	x₁ + 3
[square(x₁)]	=	0
[activate^#(x₁)]	=	x₁ + 0
[square^#(x₁)]	=	0
[pi(x₁)]	=	0
[rcons(x₁, x₂)]	=	0
[n__s(x₁)]	=	x₁ + 0
[times^#(x₁, x₂)]	=	0
[0]	=	0
[from(x₁)]	=	2
[times(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[2ndsneg(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[2ndspos^#(x₁, x₂)]	=	x₁ + 0
[cons2(x₁, x₂)]	=	1
[from^#(x₁)]	=	0
[cons(x₁, x₂)]	=	3
[pi^#(x₁)]	=	0
[2ndsneg^#(x₁, x₂)]	=	x₁ + 0
[posrecip(x₁)]	=	0

together with the usable rule

s(X)

→

n__s(X)

(15)

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

activate^#(n__from(X))

→

activate^#(X)

(21)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

activate^#(n__s(X))

→

activate^#(X)

(23)

1.1.4.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[negrecip(x₁)]	=	0
[s(x₁)]	=	x₁ + 1
[2ndspos(x₁, x₂)]	=	0
[activate(x₁)]	=	1
[rnil]	=	0
[plus^#(x₁, x₂)]	=	0
[n__from(x₁)]	=	x₁ + 3
[square(x₁)]	=	0
[activate^#(x₁)]	=	x₁ + 0
[square^#(x₁)]	=	0
[pi(x₁)]	=	0
[rcons(x₁, x₂)]	=	0
[n__s(x₁)]	=	x₁ + 1
[times^#(x₁, x₂)]	=	0
[0]	=	0
[from(x₁)]	=	2
[times(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[2ndsneg(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[2ndspos^#(x₁, x₂)]	=	x₁ + 0
[cons2(x₁, x₂)]	=	1
[from^#(x₁)]	=	0
[cons(x₁, x₂)]	=	3
[pi^#(x₁)]	=	0
[2ndsneg^#(x₁, x₂)]	=	x₁ + 0
[posrecip(x₁)]	=	0

together with the usable rule

s(X)

→

n__s(X)

(15)

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

activate^#(n__s(X))

→

activate^#(X)

(23)

could be deleted.

1.1.4.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.