Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/PEANO_nosorts-noand_L)

The rewrite relation of the following TRS is considered.

U12(tt) → s(plus(N,M)) (1)
U11(tt) → U12(tt) (2)
plus(N,0) → N (3)
plus(N,s(M)) → U11(tt) (4)
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 = plus(N,U12(tt))
→ plus(N,s(plus(U12(tt),U12(tt))))
→ U11(tt)
→ U12(tt)
→ s(plus(U12(tt),U12(tt)))
= t4
where t4 = C[t0σ] and σ = {N/U12(tt)} and C = s(☐)