Certification Problem

Input (TPDB TRS_Standard/SK90/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)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by ttt2 @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t0 = f(f(f(a,f(a,x75)),c),f(f(a,f(a,x75)),c))
→ f(f(f(a,x75),f(f(a,f(a,x75)),c)),f(c,f(f(a,f(a,x75)),c)))
→ f(f(x75,f(c,f(f(a,f(a,x75)),c))),f(f(f(a,f(a,x75)),c),f(c,f(f(a,f(a,x75)),c))))
→ f(f(x75,f(c,f(f(a,f(a,x75)),c))),f(f(f(a,f(a,x75)),c),f(f(a,f(a,x75)),c)))
= t3
where t3 = C[t0σ] and σ = {x75/x75} and C = f(f(x75,f(c,f(f(a,f(a,x75)),c))),☐)