Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex15_Luc06_Z)

The rewrite relation of the following TRS is considered.

f(n__f(n__a)) f(n__g(f(n__a))) (1)
f(X) n__f(X) (2)
a n__a (3)
g(X) n__g(X) (4)
activate(n__f(X)) f(X) (5)
activate(n__a) a (6)
activate(n__g(X)) g(X) (7)
activate(X) X (8)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Bounds

The given TRS is match-(raise)-bounded by 3. This is shown by the following automaton.