Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/ttt1)

The rewrite relation of the following TRS is considered.

f(s(a),s(b),x) → f(x,x,x) (1)
g(f(s(x),s(y),z)) → g(f(x,y,z)) (2)
cons(x,y) → x (3)
cons(x,y) → y (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 = f(cons(s(a),s(b)),cons(s(a),s(b)),cons(s(a),s(b)))
→ f(cons(s(a),s(b)),s(b),cons(s(a),s(b)))
→ f(s(a),s(b),cons(s(a),s(b)))
→ f(cons(s(a),s(b)),cons(s(a),s(b)),cons(s(a),s(b)))
= t3
where t3 = t0