Certification Problem

Input (TPDB TRS_Standard/Strategy_removed_CSR_05/Ex26_Luc03b)

The rewrite relation of the following TRS is considered.

terms(N)	→	cons(recip(sqr(N)),terms(s(N)))	(1)
sqr(0)	→	0	(2)
sqr(s(X))	→	s(add(sqr(X),dbl(X)))	(3)
dbl(0)	→	0	(4)
dbl(s(X))	→	s(s(dbl(X)))	(5)
add(0,X)	→	X	(6)
add(s(X),Y)	→	s(add(X,Y))	(7)
first(0,X)	→	nil	(8)
first(s(X),cons(Y,Z))	→	cons(Y,first(X,Z))	(9)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by ttt2 @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t₀	=	terms(N)
	→	cons(recip(sqr(N)),terms(s(N)))
	=	t₁

where t₁ = C[t₀σ] and σ = {N/s(N)} and C = cons(recip(sqr(N)),☐)