Certification Problem

Input (TPDB TRS_Standard/Waldmann_06/jwno4)

The rewrite relation of the following TRS is considered.

f(h(x),y)

→

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

(1)

Prove or disprove termination.

No.

The following loop proves nontermination.

t₀	=	f(h(h(x758)),h(h(x986)))
	→	h(f(h(h(x986)),f(h(x758),h(a))))
	→	h(h(f(f(h(x758),h(a)),f(h(x986),h(a)))))
	→	h(h(f(h(f(h(a),f(x758,h(a)))),f(h(x986),h(a)))))
	→	h(h(f(h(h(f(f(x758,h(a)),f(a,h(a))))),f(h(x986),h(a)))))
	→	h(h(f(h(h(f(f(x758,h(a)),f(a,h(a))))),h(f(h(a),f(x986,h(a)))))))
	→	h(h(f(h(h(f(f(x758,h(a)),f(a,h(a))))),h(h(f(f(x986,h(a)),f(a,h(a))))))))
	=	t₆

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