Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/jwno6)

The rewrite relation of the following TRS is considered.

f(x,h(y)) → h(f(f(h(a),y),x)) (1)
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(f(h(y'''),f(x''',h(y'))),f(h(y''),f(x'',h(y))))
→ f(f(h(y'''),f(x''',h(y'))),f(h(y''),h(f(f(h(a),y),x''))))
→ f(f(h(y'''),f(x''',h(y'))),h(f(f(h(a),f(f(h(a),y),x'')),h(y''))))
→ h(f(f(h(a),f(f(h(a),f(f(h(a),y),x'')),h(y''))),f(h(y'''),f(x''',h(y')))))
= t3
where t3 = C[t0σ] and σ = {y/y', y'/y'', y''/y''', x''/x''', y'''/a, x'''/f(h(a),f(f(h(a),y),x''))} and C = h(☐)