Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/Ex1_GM03)

The rewrite relation of the following TRS is considered.

p(0) → 0 (1)
p(s(X)) → X (2)
leq(0,Y) → true (3)
leq(s(X),0) → false (4)
leq(s(X),s(Y)) → leq(X,Y) (5)
if(true,X,Y) → X (6)
if(false,X,Y) → Y (7)
diff(X,Y) → if(leq(X,Y),0,s(diff(p(X),Y))) (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 = diff(X,Y)
→ if(leq(X,Y),0,s(diff(p(X),Y)))
= t1
where t1 = C[t0σ] and σ = {X/p(X), Y/Y} and C = if(leq(X,Y),0,s(☐))