Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Transformed_CSR_04/Ex18_Luc06_GM)

The rewrite relation of the following TRS is considered.

a__f(f(a)) → a__f(g(f(a))) (1)
mark(f(X)) → a__f(mark(X)) (2)
mark(a) → a (3)
mark(g(X)) → g(X) (4)
a__f(X) → f(X) (5)
The evaluation strategy is innermost.

Property / Task

Determine bounds on the runtime complexity.

Answer / Result

An upperbound for the complexity is O(n).

Proof (by AProVE @ termCOMP 2023)

1 Bounds

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