Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/jwno4)

The rewrite relation of the following TRS is considered.

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