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)

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(x0,h(x1))

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

f^#(x,h(y))	→	f^#(f(h(a),y),x)	(2)
f^#(x,h(y))	→	f^#(h(a),y)	(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^#(x,h(y))	→	f^#(f(h(a),y),x)	(2)
f^#(x0,h(h(y_1)))	→	f^#(h(a),h(y_1))	(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(h(y'''),f(x''',h(y'))),f(h(y''),f(x'',h(y))))
	→_R	f^#(f(h(y'''),f(x''',h(y'))),f(h(y''),h(f(f(h(a),y),x''))))
	→_R	f^#(f(h(y'''),f(x''',h(y'))),h(f(f(h(a),f(f(h(a),y),x'')),h(y''))))
	→_P	f^#(f(h(a),f(f(h(a),f(f(h(a),y),x'')),h(y''))),f(h(y'''),f(x''',h(y'))))
	=	t₃

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