Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Rubio_04/test4)

The rewrite relation of the following TRS is considered.

f(a,a) → f(a,b) (1)
f(a,b) → f(s(a),c) (2)
f(s(X),c) → f(X,c) (3)
f(c,c) → f(a,a) (4)
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 4. This is shown by the following automaton.