Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/SK90/4.30)

The rewrite relation of the following TRS is considered.

f(nil) → nil (1)
f(.(nil,y)) → .(nil,f(y)) (2)
f(.(.(x,y),z)) → f(.(x,.(y,z))) (3)
g(nil) → nil (4)
g(.(x,nil)) → .(g(x),nil) (5)
g(.(x,.(y,z))) → g(.(.(x,y),z)) (6)
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.