Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/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)
The evaluation strategy is outermost

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

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