Certification Problem

Input (TPDB TRS_Relative/Mixed_relative_TRS/assoc)

The relative rewrite relation R/S is considered where R is the following TRS

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

and S is the following TRS.

f(x,f(y,z)) → f(f(x,y),z) (2)
f(f(x,y),z) → f(x,f(y,z)) (3)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Loop

The following loop proves that R/S is not relative terminating.

t0 = f(a,f(x',f(y',a)))
→S f(a,f(f(x',y'),a))
→R f(f(f(x',y'),a),f(b,f(f(x',y'),a)))
→S f(f(x',y'),f(a,f(b,f(f(x',y'),a))))
= t3
where t3 = C[t0σ] and σ = {x'/b, y'/f(x',y')} and C = f(f(x',y'),☐)