Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Endrullis_06/direct)

The rewrite relation of the following TRS is considered.

h(x,c(y,z)) h(c(s(y),x),z) (1)
h(c(s(x),c(s(0),y)),z) h(y,c(s(0),c(x,z))) (2)
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 2. This is shown by the following automaton.