Certification Problem

Input (TPDB TRS_Standard/Secret_05_TRS/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)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by ttt2 @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t0 = g(f(s(cons(s(a),s(b))),s(cons(s(a),s(b))),s(cons(s(a),s(b)))))
→ g(f(s(cons(s(a),s(b))),s(s(b)),s(cons(s(a),s(b)))))
→ g(f(s(s(a)),s(s(b)),s(cons(s(a),s(b)))))
→ g(f(s(a),s(b),s(cons(s(a),s(b)))))
→ g(f(s(cons(s(a),s(b))),s(cons(s(a),s(b))),s(cons(s(a),s(b)))))
= t4
where t4 = t0