Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex24_GM04_Z)

The rewrite relation of the following TRS is considered.

f(X,n__g(X),Y) → f(activate(Y),activate(Y),activate(Y)) (1)
g(b) → c (2)
b → c (3)
g(X) → n__g(X) (4)
activate(n__g(X)) → g(X) (5)
activate(X) → X (6)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by ttt2 @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t0 = f(X,n__g(X),n__g(b))
→ f(activate(n__g(b)),activate(n__g(b)),activate(n__g(b)))
→ f(g(b),activate(n__g(b)),activate(n__g(b)))
→ f(c,activate(n__g(b)),activate(n__g(b)))
→ f(c,n__g(b),activate(n__g(b)))
→ f(c,n__g(c),activate(n__g(b)))
→ f(c,n__g(c),n__g(b))
= t6
where t6 = t0σ and σ = {X/c}