Certification Problem

Input (TPDB TRS_Standard/Waldmann_06/jwno9)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by ttt2 @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t0 = f(f(a,f(a,x1775)),f(a,f(a,x1943)))
→ f(a,f(f(f(a,a),f(a,x1943)),f(a,f(a,x1775))))
→ f(a,f(a,f(f(f(a,a),f(a,x1775)),f(f(a,a),f(a,x1943)))))
→ f(a,f(a,f(f(a,f(f(f(a,a),x1775),f(a,a))),f(f(a,a),f(a,x1943)))))
→ f(a,f(a,f(f(a,f(a,f(f(f(a,a),a),f(f(a,a),x1775)))),f(f(a,a),f(a,x1943)))))
→ f(a,f(a,f(f(a,f(a,f(f(f(a,a),a),f(f(a,a),x1775)))),f(a,f(f(f(a,a),x1943),f(a,a))))))
→ f(a,f(a,f(f(a,f(a,f(f(f(a,a),a),f(f(a,a),x1775)))),f(a,f(a,f(f(f(a,a),a),f(f(a,a),x1943)))))))
= t6
where t6 = C[t0σ] and σ = {x1943/f(f(f(a,a),a),f(f(a,a),x1943)), x1775/f(f(f(a,a),a),f(f(a,a),x1775))} and C = f(a,f(a,☐))