Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/MYNAT_nosorts-noand_L)

The rewrite relation of the following TRS is considered.

U12(tt) → s(plus(N,M)) (1)
U22(tt) → plus(x(N,M),N) (2)
U11(tt) → U12(tt) (3)
U21(tt) → U22(tt) (4)
plus(N,0) → N (5)
plus(N,s(M)) → U11(tt) (6)
x(N,0) → 0 (7)
x(N,s(M)) → U21(tt) (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 = U22(tt)
→ plus(x(U22(tt),U22(tt)),U22(tt))
= t1
where t1 = C[t0] and C = plus(x(U22(tt),U22(tt)),☐)