Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex14_AEGL02_Z)

The rewrite relation of the following TRS is considered.

from(X) → cons(X,n__from(s(X))) (1)
length(n__nil) → 0 (2)
length(n__cons(X,Y)) → s(length1(activate(Y))) (3)
length1(X) → length(activate(X)) (4)
from(X) → n__from(X) (5)
nil → n__nil (6)
cons(X1,X2) → n__cons(X1,X2) (7)
activate(n__from(X)) → from(X) (8)
activate(n__nil) → nil (9)
activate(n__cons(X1,X2)) → cons(X1,X2) (10)
activate(X) → X (11)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by ttt2 @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t0 = length(n__cons(X,n__from(x42749)))
→ s(length1(activate(n__from(x42749))))
→ s(length(activate(activate(n__from(x42749)))))
→ s(length(activate(n__from(x42749))))
→ s(length(from(x42749)))
→ s(length(cons(x42749,n__from(s(x42749)))))
→ s(length(n__cons(x42749,n__from(s(x42749)))))
= t6
where t6 = C[t0σ] and σ = {x42749/s(x42749), X/x42749} and C = s(☐)