Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/SK90/2.41)

The rewrite relation of the following TRS is considered.

norm(nil) → 0 (1)
norm(g(x,y)) → s(norm(x)) (2)
f(x,nil) → g(nil,x) (3)
f(x,g(y,z)) → g(f(x,y),z) (4)
rem(nil,y) → nil (5)
rem(g(x,y),0) → g(x,y) (6)
rem(g(x,y),s(z)) → rem(x,z) (7)
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 1. This is shown by the following automaton.