Certification Problem

Input (TPDB TRS_Standard/Waldmann_06/jwno1)

The rewrite relation of the following TRS is considered.

f(h(x),y) → h(f(y,f(x,h(f(a,a))))) (1)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by ttt2 @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t0 = f(h(h(x1062)),h(h(x1398)))
→ h(f(h(h(x1398)),f(h(x1062),h(f(a,a)))))
→ h(h(f(f(h(x1062),h(f(a,a))),f(h(x1398),h(f(a,a))))))
→ h(h(f(h(f(h(f(a,a)),f(x1062,h(f(a,a))))),f(h(x1398),h(f(a,a))))))
→ h(h(f(h(h(f(f(x1062,h(f(a,a))),f(f(a,a),h(f(a,a)))))),f(h(x1398),h(f(a,a))))))
→ h(h(f(h(h(f(f(x1062,h(f(a,a))),f(f(a,a),h(f(a,a)))))),h(f(h(f(a,a)),f(x1398,h(f(a,a))))))))
→ h(h(f(h(h(f(f(x1062,h(f(a,a))),f(f(a,a),h(f(a,a)))))),h(h(f(f(x1398,h(f(a,a))),f(f(a,a),h(f(a,a)))))))))
= t6
where t6 = C[t0σ] and σ = {x1398/f(f(x1398,h(f(a,a))),f(f(a,a),h(f(a,a)))), x1062/f(f(x1062,h(f(a,a))),f(f(a,a),h(f(a,a))))} and C = h(h(☐))