Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExAppendixB_AEL03_Z)

The rewrite relation of the following TRS is considered.

from(X)	→	cons(X,n__from(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)
activate(n__from(X))	→	from(X)	(15)
activate(X)	→	X	(16)

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.

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

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair

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

1.1.1 Subterm Criterion Processor

We use the projection

π(2ndsneg^#)	=	1
π(2ndspos^#)	=	1

and remove the pairs:

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

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 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

times^#(s(X),Y) → times^#(X,Y) (28)

2 ≥ 2

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 3^rd component contains the pair
plus^#(s(X),Y) → plus^#(X,Y) (27)

1.1.3 Subterm Criterion Processor
We use the projection
π(plus^#) = 1
and remove the pairs:
plus^#(s(X),Y) → plus^#(X,Y) (27)

1.1.3.1 P is empty

There are no pairs anymore.