Certification Problem

Input (TPDB TRS_Standard/Waldmann_06/jwno1)

The rewrite relation of the following TRS is considered.

f(h(x),y)

→

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

(1)

Prove or disprove termination.

No.

The following loop proves nontermination.

t₀	=	f(h(h(x1062)),h(h(x1398)))
	→	h(f(h(h(x1398)),f(h(x1062),h(f(a,a)))))
	→	h(h(f(f(h(x1062),h(f(a,a))),f(h(x1398),h(f(a,a))))))
	→	h(h(f(h(f(h(f(a,a)),f(x1062,h(f(a,a))))),f(h(x1398),h(f(a,a))))))
	→	h(h(f(h(h(f(f(x1062,h(f(a,a))),f(f(a,a),h(f(a,a)))))),f(h(x1398),h(f(a,a))))))
	→	h(h(f(h(h(f(f(x1062,h(f(a,a))),f(f(a,a),h(f(a,a)))))),h(f(h(f(a,a)),f(x1398,h(f(a,a))))))))
	→	h(h(f(h(h(f(f(x1062,h(f(a,a))),f(f(a,a),h(f(a,a)))))),h(h(f(f(x1398,h(f(a,a))),f(f(a,a),h(f(a,a)))))))))
	=	t₆

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