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)

Prove or disprove termination.

No.

The following loop proves nontermination.

t₀	=	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)))))))
	=	t₆

where t₆ = C[t₀σ] 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,☐))