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)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Innermost Lhss Increase

We add the following left hand sides to the innermost strategy.

f(h(x0),x1)

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

f^#(h(x),y)	→	f^#(y,f(x,h(a)))	(2)
f^#(h(x),y)	→	f^#(x,h(a))	(3)

It remains to prove infiniteness of the resulting DP problem.

1.1.1 Instantiation Processor

The pairs are instantiated to the following pairs.

f^#(h(x),y)	→	f^#(y,f(x,h(a)))	(2)
f^#(h(h(y_0)),x1)	→	f^#(h(y_0),h(a))	(4)

1.1.1.1 Full Strategy Switch Processor

We have a locally confluent overlay TRS, no overlaps between P and R, and the strategy is less than innermost. Hence, it suffices to prove non-termination for the full rewrite relation.

Local Confluence Proof

All critical pairs are joinable within 0 step(s). 0

1.1.1.1.1 Loop

The following loop proves infiniteness of the DP problem.

t₀	=	f^#(f(f(h(x),y''),h(x'')),f(f(h(x'),y'''),h(x''')))
	→_R	f^#(f(h(f(y'',f(x,h(a)))),h(x'')),f(f(h(x'),y'''),h(x''')))
	→_R	f^#(h(f(h(x''),f(f(y'',f(x,h(a))),h(a)))),f(f(h(x'),y'''),h(x''')))
	→_P	f^#(f(f(h(x'),y'''),h(x''')),f(f(h(x''),f(f(y'',f(x,h(a))),h(a))),h(a)))
	=	t₃

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