Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/LengthOfFiniteLists_nosorts-noand_Z)

The rewrite relation of the following TRS is considered.

zeros → cons(0,n__zeros) (1)
U11(tt,L) → U12(tt,activate(L)) (2)
U12(tt,L) → s(length(activate(L))) (3)
length(nil) → 0 (4)
length(cons(N,L)) → U11(tt,activate(L)) (5)
zeros → n__zeros (6)
activate(n__zeros) → zeros (7)
activate(X) → X (8)
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 = U12(tt,activate(activate(n__zeros)))
→ s(length(activate(activate(activate(n__zeros)))))
→ s(length(activate(activate(n__zeros))))
→ s(length(activate(n__zeros)))
→ s(length(zeros))
→ s(length(cons(0,n__zeros)))
→ s(U11(tt,activate(n__zeros)))
→ s(U12(tt,activate(activate(n__zeros))))
= t7
where t7 = C[t0] and C = s(☐)