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 ttt2 @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t0 = activate(n__f(g(g(X)),x59))
→ f(g(g(X)),x59)
→ f(g(X),n__f(g(g(X)),activate(x59)))
→ f(X,n__f(g(X),activate(n__f(g(g(X)),activate(x59)))))
= t3
where t3 = C[t0σ] and σ = {x59/activate(x59), X/X} and C = f(X,n__f(g(X),☐))