Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/hoca/sum)

The rewrite relation of the following TRS is considered.

plus#2(0,x12) → x12 (1)
plus#2(S(x4),x2) → S(plus#2(x4,x2)) (2)
fold#3(Nil) → 0 (3)
fold#3(Cons(x4,x2)) → plus#2(x4,fold#3(x2)) (4)
main(x1) → fold#3(x1) (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 1. This is shown by the following automaton.