Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/LengthOfFiniteLists_nosorts_noand_GM)

The rewrite relation of the following TRS is considered.

a__zeros	→	cons(0,zeros)	(1)
a__U11(tt,L)	→	a__U12(tt,L)	(2)
a__U12(tt,L)	→	s(a__length(mark(L)))	(3)
a__length(nil)	→	0	(4)
a__length(cons(N,L))	→	a__U11(tt,L)	(5)
mark(zeros)	→	a__zeros	(6)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(7)
mark(U12(X1,X2))	→	a__U12(mark(X1),X2)	(8)
mark(length(X))	→	a__length(mark(X))	(9)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(10)
mark(0)	→	0	(11)
mark(tt)	→	tt	(12)
mark(s(X))	→	s(mark(X))	(13)
mark(nil)	→	nil	(14)
a__zeros	→	zeros	(15)
a__U11(X1,X2)	→	U11(X1,X2)	(16)
a__U12(X1,X2)	→	U12(X1,X2)	(17)
a__length(X)	→	length(X)	(18)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by ttt2 @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t₀	=	a__U11(tt,zeros)
	→	a__U12(tt,zeros)
	→	s(a__length(mark(zeros)))
	→	s(a__length(a__zeros))
	→	s(a__length(cons(0,zeros)))
	→	s(a__U11(tt,zeros))
	=	t₅

where t₅ = C[t₀] and C = s(☐)