Certification Problem

Input (TPDB TRS_Standard/Waldmann_06/jwno6)

The rewrite relation of the following TRS is considered.

f(x,h(y))

→

h(f(f(h(a),y),x))

(1)

Prove or disprove termination.

No.

The following loop proves nontermination.

t₀	=	f(h(h(x799)),h(h(x877)))
	→	h(f(f(h(a),h(x877)),h(h(x799))))
	→	h(h(f(f(h(a),h(x799)),f(h(a),h(x877)))))
	→	h(h(f(h(f(f(h(a),x799),h(a))),f(h(a),h(x877)))))
	→	h(h(f(h(h(f(f(h(a),a),f(h(a),x799)))),f(h(a),h(x877)))))
	→	h(h(f(h(h(f(f(h(a),a),f(h(a),x799)))),h(f(f(h(a),x877),h(a))))))
	→	h(h(f(h(h(f(f(h(a),a),f(h(a),x799)))),h(h(f(f(h(a),a),f(h(a),x877)))))))
	=	t₆

where t₆ = C[t₀σ] and σ = {x877/f(f(h(a),a),f(h(a),x877)), x799/f(f(h(a),a),f(h(a),x799))} and C = h(h(☐))