Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/raML/rationalPotential.raml)

The rewrite relation of the following TRS is considered.

group3(@l) → group3#1(@l) (1)
group3#1(::(@x,@xs)) → group3#2(@xs,@x) (2)
group3#1(nil) → nil (3)
group3#2(::(@y,@ys),@x) → group3#3(@ys,@x,@y) (4)
group3#2(nil,@x) → nil (5)
group3#3(::(@z,@zs),@x,@y) → ::(tuple#3(@x,@y,@z),group3(@zs)) (6)
group3#3(nil,@x,@y) → nil (7)
zip3(@l1,@l2,@l3) → zip3#1(@l1,@l2,@l3) (8)
zip3#1(::(@x,@xs),@l2,@l3) → zip3#2(@l2,@l3,@x,@xs) (9)
zip3#1(nil,@l2,@l3) → nil (10)
zip3#2(::(@y,@ys),@l3,@x,@xs) → zip3#3(@l3,@x,@xs,@y,@ys) (11)
zip3#2(nil,@l3,@x,@xs) → nil (12)
zip3#3(::(@z,@zs),@x,@xs,@y,@ys) → ::(tuple#3(@x,@y,@z),zip3(@xs,@ys,@zs)) (13)
zip3#3(nil,@x,@xs,@y,@ys) → nil (14)
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.