Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/jwno1)

The rewrite relation of the following TRS is considered.

f(h(x),y)

→

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

(1)

The evaluation strategy is outermost

Prove or disprove termination.

No.

The following loop proves nontermination.

t₀	=	f(f(f(h(x),y''),h(x'')),f(f(h(x'),y'''),h(x''')))
	→	f(f(h(f(y'',f(x,h(f(a,a))))),h(x'')),f(f(h(x'),y'''),h(x''')))
	→	f(h(f(h(x''),f(f(y'',f(x,h(f(a,a)))),h(f(a,a))))),f(f(h(x'),y'''),h(x''')))
	→	h(f(f(f(h(x'),y'''),h(x''')),f(f(h(x''),f(f(y'',f(x,h(f(a,a)))),h(f(a,a)))),h(f(a,a)))))
	=	t₃

where t₃ = C[t₀σ] and σ = {y''/y''', x/x', x'/x'', x''/x''', y'''/f(f(y'',f(x,h(f(a,a)))),h(f(a,a))), x'''/f(a,a)} and C = h(☐)