Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/LengthOfFiniteLists_nosorts_GM)

The rewrite relation of the following TRS is considered.

a__zeros	→	cons(0,zeros)	(1)
a__and(tt,X)	→	mark(X)	(2)
a__length(nil)	→	0	(3)
a__length(cons(N,L))	→	s(a__length(mark(L)))	(4)
mark(zeros)	→	a__zeros	(5)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(6)
mark(length(X))	→	a__length(mark(X))	(7)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(8)
mark(0)	→	0	(9)
mark(tt)	→	tt	(10)
mark(nil)	→	nil	(11)
mark(s(X))	→	s(mark(X))	(12)
a__zeros	→	zeros	(13)
a__and(X1,X2)	→	and(X1,X2)	(14)
a__length(X)	→	length(X)	(15)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by ttt2 @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t₀	=	a__length(cons(N,zeros))
	→	s(a__length(mark(zeros)))
	→	s(a__length(a__zeros))
	→	s(a__length(cons(0,zeros)))
	=	t₃

where t₃ = C[t₀σ] and σ = {N/0} and C = s(☐)