Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/4.40)

The rewrite relation of the following TRS is considered.

f(f(f(a,x),y),z) → f(f(x,z),f(y,z)) (1)
f(f(b,x),y) → x (2)
f(c,y) → y (3)
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(f(b,f(f(a,a),b)),y'),f(f(b,f(a,f(f(b,f(f(a,a),b)),y'''))),y'')),y'''')
→ f(f(f(f(b,f(f(a,a),b)),y'),f(a,f(f(b,f(f(a,a),b)),y'''))),y'''')
→ f(f(f(f(a,a),b),f(a,f(f(b,f(f(a,a),b)),y'''))),y'''')
→ f(f(f(a,f(a,f(f(b,f(f(a,a),b)),y'''))),f(b,f(a,f(f(b,f(f(a,a),b)),y''')))),y'''')
→ f(f(f(a,f(f(b,f(f(a,a),b)),y''')),y''''),f(f(b,f(a,f(f(b,f(f(a,a),b)),y'''))),y''''))
→ f(f(f(f(b,f(f(a,a),b)),y'''),f(f(b,f(a,f(f(b,f(f(a,a),b)),y'''))),y'''')),f(y'''',f(f(b,f(a,f(f(b,f(f(a,a),b)),y'''))),y'''')))
= t5
where t5 = t0σ and σ = {y'/y''', y''/y'''', y''''/f(y'''',f(f(b,f(a,f(f(b,f(f(a,a),b)),y'''))),y''''))}