Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex4_4_Luc96b_Z)

The rewrite relation of the following TRS is considered.

f(g(X),Y) → f(X,n__f(g(X),activate(Y))) (1)
f(X1,X2) → n__f(X1,X2) (2)
activate(n__f(X1,X2)) → f(X1,X2) (3)
activate(X) → X (4)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
f#(g(X),Y) → f#(X,n__f(g(X),activate(Y))) (5)
f#(g(X),Y) → activate#(Y) (6)
activate#(n__f(X1,X2)) → f#(X1,X2) (7)
It remains to prove infiniteness of the resulting DP problem.

1.1 Loop

The following loop proves infiniteness of the DP problem.

t0 = f#(g(X'),n__f(g(g(X'')),X2))
→P activate#(n__f(g(g(X'')),X2))
→P f#(g(g(X'')),X2)
→P f#(g(X''),n__f(g(g(X'')),activate(X2)))
= t3
where t3 = t0σ and σ = {X'/X'', X2/activate(X2)}