Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/hoca/foldsum)

The rewrite relation of the following TRS is considered.

comp_f_g#1(plus_x(x3),comp_f_g(x1,x2),0) → plus_x#1(x3,comp_f_g#1(x1,x2,0)) (1)
comp_f_g#1(plus_x(x3),id,0) → plus_x#1(x3,0) (2)
map#2(Nil) → Nil (3)
map#2(Cons(x16,x6)) → Cons(plus_x(x16),map#2(x6)) (4)
plus_x#1(0,x6) → x6 (5)
plus_x#1(S(x8),x10) → S(plus_x#1(x8,x10)) (6)
foldr_f#3(Nil,0) → 0 (7)
foldr_f#3(Cons(x16,x5),x24) → comp_f_g#1(x16,foldr#3(x5),x24) (8)
foldr#3(Nil) → id (9)
foldr#3(Cons(x32,x6)) → comp_f_g(x32,foldr#3(x6)) (10)
main(x3) → foldr_f#3(map#2(x3),0) (11)
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.