The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

rev_l#2(x8, x10) → Cons(x10, x8)
step_x_f#1(rev_l, x5, step_x_f(x2, x3, x4), x1) → step_x_f#1(x2, x3, x4, rev_l#2(x1, x5))
step_x_f#1(rev_l, x5, fleft_op_e_xs_1, x3) → rev_l#2(x3, x5)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(x16, x6)) → step_x_f(rev_l, x16, foldr#3(x6))
main(Nil) → Nil
main(Cons(x8, x9)) → step_x_f#1(rev_l, x8, foldr#3(x9), Nil)

Rewrite Strategy: INNERMOST

(1) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 3.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 4]
transitions:
Cons0(0, 0) → 0
rev_l0() → 0
step_x_f0(0, 0, 0) → 0
fleft_op_e_xs_10() → 0
Nil0() → 0
rev_l#20(0, 0) → 1
step_x_f#10(0, 0, 0, 0) → 2
foldr#30(0) → 3
main0(0) → 4
Cons1(0, 0) → 1
rev_l#21(0, 0) → 5
step_x_f#11(0, 0, 0, 5) → 2
rev_l#21(0, 0) → 2
fleft_op_e_xs_11() → 3
rev_l1() → 6
foldr#31(0) → 7
step_x_f1(6, 0, 7) → 3
Nil1() → 4
rev_l1() → 8
foldr#31(0) → 9
Nil1() → 10
step_x_f#11(8, 0, 9, 10) → 4
Cons2(0, 0) → 2
Cons2(0, 0) → 5
rev_l#21(5, 0) → 5
rev_l#21(5, 0) → 2
fleft_op_e_xs_11() → 7
fleft_op_e_xs_11() → 9
step_x_f1(6, 0, 7) → 7
step_x_f1(6, 0, 7) → 9
Cons2(0, 5) → 2
Cons2(0, 5) → 5
rev_l#22(10, 0) → 11
step_x_f#12(6, 0, 7, 11) → 4
rev_l#22(10, 0) → 4
Cons3(0, 10) → 4
Cons3(0, 10) → 11
rev_l#22(11, 0) → 11
rev_l#22(11, 0) → 4
Cons3(0, 11) → 4
Cons3(0, 11) → 11

(2) BOUNDS(1, n^1)