WORST_CASE(Omega(n^1),O(n^1))
proof of input_rOLbxGsaDj.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxTRS
(1) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms]
(2) CpxTRS
    (3) CpxTrsMatchBoundsTAProof [FINISHED, 32 ms]
    (4) BOUNDS(1, n^1)
(5) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CdtProblem
    (7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CpxRelTRS
    (9) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CpxRelTRS
    (11) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) typed CpxTrs
    (13) OrderProof [LOWER BOUND(ID), 13 ms]
    (14) typed CpxTrs
    (15) RewriteLemmaProof [LOWER BOUND(ID), 260 ms]
    (16) BEST
        (17) proven lower bound
            (18) LowerBoundPropagationProof [FINISHED, 0 ms]
            (19) BOUNDS(n^1, INF)
        (20) typed CpxTrs
            (21) RewriteLemmaProof [LOWER BOUND(ID), 19 ms]
            (22) typed CpxTrs
            (23) RewriteLemmaProof [LOWER BOUND(ID), 30 ms]
            (24) typed CpxTrs
            (25) RewriteLemmaProof [LOWER BOUND(ID), 49 ms]
            (26) BOUNDS(1, INF)


----------------------------------------

(0)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^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)

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) RelTrsToTrsProof (UPPER BOUND(ID))
transformed relative TRS to TRS
----------------------------------------

(2)
Obligation:
The Runtime Complexity (parallel-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)

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(3) CpxTrsMatchBoundsTAProof (FINISHED)
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

----------------------------------------

(4)
BOUNDS(1, n^1)

----------------------------------------

(5) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rev_l#2(z0, z1) -> Cons(z1, z0)
   step_x_f#1(rev_l, z0, step_x_f(z1, z2, z3), z4) -> step_x_f#1(z1, z2, z3, rev_l#2(z4, z0))
   step_x_f#1(rev_l, z0, fleft_op_e_xs_1, z1) -> rev_l#2(z1, z0)
   foldr#3(Nil) -> fleft_op_e_xs_1
   foldr#3(Cons(z0, z1)) -> step_x_f(rev_l, z0, foldr#3(z1))
   main(Nil) -> Nil
   main(Cons(z0, z1)) -> step_x_f#1(rev_l, z0, foldr#3(z1), Nil)
Tuples:
   REV_L#2(z0, z1) -> c
   STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) -> c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)), REV_L#2(z4, z0))
   STEP_X_F#1(rev_l, z0, fleft_op_e_xs_1, z1) -> c2(REV_L#2(z1, z0))
   FOLDR#3(Nil) -> c3
   FOLDR#3(Cons(z0, z1)) -> c4(FOLDR#3(z1))
   MAIN(Nil) -> c5
   MAIN(Cons(z0, z1)) -> c6(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil), FOLDR#3(z1))
S tuples:
   REV_L#2(z0, z1) -> c
   STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) -> c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)), REV_L#2(z4, z0))
   STEP_X_F#1(rev_l, z0, fleft_op_e_xs_1, z1) -> c2(REV_L#2(z1, z0))
   FOLDR#3(Nil) -> c3
   FOLDR#3(Cons(z0, z1)) -> c4(FOLDR#3(z1))
   MAIN(Nil) -> c5
   MAIN(Cons(z0, z1)) -> c6(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil), FOLDR#3(z1))
K tuples:none
Defined Rule Symbols:   rev_l#2_2, step_x_f#1_4, foldr#3_1, main_1

Defined Pair Symbols:   REV_L#2_2, STEP_X_F#1_4, FOLDR#3_1, MAIN_1

Compound Symbols:   c, c1_2, c2_1, c3, c4_1, c5, c6_2


----------------------------------------

(7) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

(8)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   REV_L#2(z0, z1) -> c
   STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) -> c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)), REV_L#2(z4, z0))
   STEP_X_F#1(rev_l, z0, fleft_op_e_xs_1, z1) -> c2(REV_L#2(z1, z0))
   FOLDR#3(Nil) -> c3
   FOLDR#3(Cons(z0, z1)) -> c4(FOLDR#3(z1))
   MAIN(Nil) -> c5
   MAIN(Cons(z0, z1)) -> c6(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil), FOLDR#3(z1))

The (relative) TRS S consists of the following rules:

   rev_l#2(z0, z1) -> Cons(z1, z0)
   step_x_f#1(rev_l, z0, step_x_f(z1, z2, z3), z4) -> step_x_f#1(z1, z2, z3, rev_l#2(z4, z0))
   step_x_f#1(rev_l, z0, fleft_op_e_xs_1, z1) -> rev_l#2(z1, z0)
   foldr#3(Nil) -> fleft_op_e_xs_1
   foldr#3(Cons(z0, z1)) -> step_x_f(rev_l, z0, foldr#3(z1))
   main(Nil) -> Nil
   main(Cons(z0, z1)) -> step_x_f#1(rev_l, z0, foldr#3(z1), Nil)

Rewrite Strategy: INNERMOST
----------------------------------------

(9) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

(10)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   REV_L#2(z0, z1) -> c
   STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) -> c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)), REV_L#2(z4, z0))
   STEP_X_F#1(rev_l, z0, fleft_op_e_xs_1, z1) -> c2(REV_L#2(z1, z0))
   FOLDR#3(Nil) -> c3
   FOLDR#3(Cons(z0, z1)) -> c4(FOLDR#3(z1))
   MAIN(Nil) -> c5
   MAIN(Cons(z0, z1)) -> c6(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil), FOLDR#3(z1))

The (relative) TRS S consists of the following rules:

   rev_l#2(z0, z1) -> Cons(z1, z0)
   step_x_f#1(rev_l, z0, step_x_f(z1, z2, z3), z4) -> step_x_f#1(z1, z2, z3, rev_l#2(z4, z0))
   step_x_f#1(rev_l, z0, fleft_op_e_xs_1, z1) -> rev_l#2(z1, z0)
   foldr#3(Nil) -> fleft_op_e_xs_1
   foldr#3(Cons(z0, z1)) -> step_x_f(rev_l, z0, foldr#3(z1))
   main(Nil) -> Nil
   main(Cons(z0, z1)) -> step_x_f#1(rev_l, z0, foldr#3(z1), Nil)

Rewrite Strategy: INNERMOST
----------------------------------------

(11) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(12)
Obligation:
Innermost TRS:
Rules:
REV_L#2(z0, z1) -> c
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) -> c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)), REV_L#2(z4, z0))
STEP_X_F#1(rev_l, z0, fleft_op_e_xs_1, z1) -> c2(REV_L#2(z1, z0))
FOLDR#3(Nil) -> c3
FOLDR#3(Cons(z0, z1)) -> c4(FOLDR#3(z1))
MAIN(Nil) -> c5
MAIN(Cons(z0, z1)) -> c6(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil), FOLDR#3(z1))
rev_l#2(z0, z1) -> Cons(z1, z0)
step_x_f#1(rev_l, z0, step_x_f(z1, z2, z3), z4) -> step_x_f#1(z1, z2, z3, rev_l#2(z4, z0))
step_x_f#1(rev_l, z0, fleft_op_e_xs_1, z1) -> rev_l#2(z1, z0)
foldr#3(Nil) -> fleft_op_e_xs_1
foldr#3(Cons(z0, z1)) -> step_x_f(rev_l, z0, foldr#3(z1))
main(Nil) -> Nil
main(Cons(z0, z1)) -> step_x_f#1(rev_l, z0, foldr#3(z1), Nil)

Types:
REV_L#2 :: Nil:Cons -> a -> c
c :: c
STEP_X_F#1 :: rev_l -> a -> step_x_f:fleft_op_e_xs_1 -> Nil:Cons -> c1:c2
rev_l :: rev_l
step_x_f :: rev_l -> a -> step_x_f:fleft_op_e_xs_1 -> step_x_f:fleft_op_e_xs_1
c1 :: c1:c2 -> c -> c1:c2
rev_l#2 :: Nil:Cons -> a -> Nil:Cons
fleft_op_e_xs_1 :: step_x_f:fleft_op_e_xs_1
c2 :: c -> c1:c2
FOLDR#3 :: Nil:Cons -> c3:c4
Nil :: Nil:Cons
c3 :: c3:c4
Cons :: a -> Nil:Cons -> Nil:Cons
c4 :: c3:c4 -> c3:c4
MAIN :: Nil:Cons -> c5:c6
c5 :: c5:c6
c6 :: c1:c2 -> c3:c4 -> c5:c6
foldr#3 :: Nil:Cons -> step_x_f:fleft_op_e_xs_1
step_x_f#1 :: rev_l -> a -> step_x_f:fleft_op_e_xs_1 -> Nil:Cons -> Nil:Cons
main :: Nil:Cons -> Nil:Cons
hole_c1_7 :: c
hole_Nil:Cons2_7 :: Nil:Cons
hole_a3_7 :: a
hole_c1:c24_7 :: c1:c2
hole_rev_l5_7 :: rev_l
hole_step_x_f:fleft_op_e_xs_16_7 :: step_x_f:fleft_op_e_xs_1
hole_c3:c47_7 :: c3:c4
hole_c5:c68_7 :: c5:c6
gen_Nil:Cons9_7 :: Nat -> Nil:Cons
gen_c1:c210_7 :: Nat -> c1:c2
gen_step_x_f:fleft_op_e_xs_111_7 :: Nat -> step_x_f:fleft_op_e_xs_1
gen_c3:c412_7 :: Nat -> c3:c4

----------------------------------------

(13) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
STEP_X_F#1, FOLDR#3, foldr#3, step_x_f#1
----------------------------------------

(14)
Obligation:
Innermost TRS:
Rules:
REV_L#2(z0, z1) -> c
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) -> c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)), REV_L#2(z4, z0))
STEP_X_F#1(rev_l, z0, fleft_op_e_xs_1, z1) -> c2(REV_L#2(z1, z0))
FOLDR#3(Nil) -> c3
FOLDR#3(Cons(z0, z1)) -> c4(FOLDR#3(z1))
MAIN(Nil) -> c5
MAIN(Cons(z0, z1)) -> c6(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil), FOLDR#3(z1))
rev_l#2(z0, z1) -> Cons(z1, z0)
step_x_f#1(rev_l, z0, step_x_f(z1, z2, z3), z4) -> step_x_f#1(z1, z2, z3, rev_l#2(z4, z0))
step_x_f#1(rev_l, z0, fleft_op_e_xs_1, z1) -> rev_l#2(z1, z0)
foldr#3(Nil) -> fleft_op_e_xs_1
foldr#3(Cons(z0, z1)) -> step_x_f(rev_l, z0, foldr#3(z1))
main(Nil) -> Nil
main(Cons(z0, z1)) -> step_x_f#1(rev_l, z0, foldr#3(z1), Nil)

Types:
REV_L#2 :: Nil:Cons -> a -> c
c :: c
STEP_X_F#1 :: rev_l -> a -> step_x_f:fleft_op_e_xs_1 -> Nil:Cons -> c1:c2
rev_l :: rev_l
step_x_f :: rev_l -> a -> step_x_f:fleft_op_e_xs_1 -> step_x_f:fleft_op_e_xs_1
c1 :: c1:c2 -> c -> c1:c2
rev_l#2 :: Nil:Cons -> a -> Nil:Cons
fleft_op_e_xs_1 :: step_x_f:fleft_op_e_xs_1
c2 :: c -> c1:c2
FOLDR#3 :: Nil:Cons -> c3:c4
Nil :: Nil:Cons
c3 :: c3:c4
Cons :: a -> Nil:Cons -> Nil:Cons
c4 :: c3:c4 -> c3:c4
MAIN :: Nil:Cons -> c5:c6
c5 :: c5:c6
c6 :: c1:c2 -> c3:c4 -> c5:c6
foldr#3 :: Nil:Cons -> step_x_f:fleft_op_e_xs_1
step_x_f#1 :: rev_l -> a -> step_x_f:fleft_op_e_xs_1 -> Nil:Cons -> Nil:Cons
main :: Nil:Cons -> Nil:Cons
hole_c1_7 :: c
hole_Nil:Cons2_7 :: Nil:Cons
hole_a3_7 :: a
hole_c1:c24_7 :: c1:c2
hole_rev_l5_7 :: rev_l
hole_step_x_f:fleft_op_e_xs_16_7 :: step_x_f:fleft_op_e_xs_1
hole_c3:c47_7 :: c3:c4
hole_c5:c68_7 :: c5:c6
gen_Nil:Cons9_7 :: Nat -> Nil:Cons
gen_c1:c210_7 :: Nat -> c1:c2
gen_step_x_f:fleft_op_e_xs_111_7 :: Nat -> step_x_f:fleft_op_e_xs_1
gen_c3:c412_7 :: Nat -> c3:c4


Generator Equations:
gen_Nil:Cons9_7(0) <=> Nil
gen_Nil:Cons9_7(+(x, 1)) <=> Cons(hole_a3_7, gen_Nil:Cons9_7(x))
gen_c1:c210_7(0) <=> c2(c)
gen_c1:c210_7(+(x, 1)) <=> c1(gen_c1:c210_7(x), c)
gen_step_x_f:fleft_op_e_xs_111_7(0) <=> fleft_op_e_xs_1
gen_step_x_f:fleft_op_e_xs_111_7(+(x, 1)) <=> step_x_f(rev_l, hole_a3_7, gen_step_x_f:fleft_op_e_xs_111_7(x))
gen_c3:c412_7(0) <=> c3
gen_c3:c412_7(+(x, 1)) <=> c4(gen_c3:c412_7(x))


The following defined symbols remain to be analysed:
STEP_X_F#1, FOLDR#3, foldr#3, step_x_f#1
----------------------------------------

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
STEP_X_F#1(rev_l, hole_a3_7, gen_step_x_f:fleft_op_e_xs_111_7(n14_7), gen_Nil:Cons9_7(b)) -> gen_c1:c210_7(n14_7), rt in Omega(1 + n14_7)

Induction Base:
STEP_X_F#1(rev_l, hole_a3_7, gen_step_x_f:fleft_op_e_xs_111_7(0), gen_Nil:Cons9_7(b)) ->_R^Omega(1)
c2(REV_L#2(gen_Nil:Cons9_7(b), hole_a3_7)) ->_R^Omega(1)
c2(c)

Induction Step:
STEP_X_F#1(rev_l, hole_a3_7, gen_step_x_f:fleft_op_e_xs_111_7(+(n14_7, 1)), gen_Nil:Cons9_7(b)) ->_R^Omega(1)
c1(STEP_X_F#1(rev_l, hole_a3_7, gen_step_x_f:fleft_op_e_xs_111_7(n14_7), rev_l#2(gen_Nil:Cons9_7(b), hole_a3_7)), REV_L#2(gen_Nil:Cons9_7(b), hole_a3_7)) ->_R^Omega(0)
c1(STEP_X_F#1(rev_l, hole_a3_7, gen_step_x_f:fleft_op_e_xs_111_7(n14_7), Cons(hole_a3_7, gen_Nil:Cons9_7(b))), REV_L#2(gen_Nil:Cons9_7(b), hole_a3_7)) ->_IH
c1(gen_c1:c210_7(c15_7), REV_L#2(gen_Nil:Cons9_7(+(b, 1)), hole_a3_7)) ->_R^Omega(1)
c1(gen_c1:c210_7(n14_7), c)

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(16)
Complex Obligation (BEST)

----------------------------------------

(17)
Obligation:
Proved the lower bound n^1 for the following obligation:

Innermost TRS:
Rules:
REV_L#2(z0, z1) -> c
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) -> c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)), REV_L#2(z4, z0))
STEP_X_F#1(rev_l, z0, fleft_op_e_xs_1, z1) -> c2(REV_L#2(z1, z0))
FOLDR#3(Nil) -> c3
FOLDR#3(Cons(z0, z1)) -> c4(FOLDR#3(z1))
MAIN(Nil) -> c5
MAIN(Cons(z0, z1)) -> c6(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil), FOLDR#3(z1))
rev_l#2(z0, z1) -> Cons(z1, z0)
step_x_f#1(rev_l, z0, step_x_f(z1, z2, z3), z4) -> step_x_f#1(z1, z2, z3, rev_l#2(z4, z0))
step_x_f#1(rev_l, z0, fleft_op_e_xs_1, z1) -> rev_l#2(z1, z0)
foldr#3(Nil) -> fleft_op_e_xs_1
foldr#3(Cons(z0, z1)) -> step_x_f(rev_l, z0, foldr#3(z1))
main(Nil) -> Nil
main(Cons(z0, z1)) -> step_x_f#1(rev_l, z0, foldr#3(z1), Nil)

Types:
REV_L#2 :: Nil:Cons -> a -> c
c :: c
STEP_X_F#1 :: rev_l -> a -> step_x_f:fleft_op_e_xs_1 -> Nil:Cons -> c1:c2
rev_l :: rev_l
step_x_f :: rev_l -> a -> step_x_f:fleft_op_e_xs_1 -> step_x_f:fleft_op_e_xs_1
c1 :: c1:c2 -> c -> c1:c2
rev_l#2 :: Nil:Cons -> a -> Nil:Cons
fleft_op_e_xs_1 :: step_x_f:fleft_op_e_xs_1
c2 :: c -> c1:c2
FOLDR#3 :: Nil:Cons -> c3:c4
Nil :: Nil:Cons
c3 :: c3:c4
Cons :: a -> Nil:Cons -> Nil:Cons
c4 :: c3:c4 -> c3:c4
MAIN :: Nil:Cons -> c5:c6
c5 :: c5:c6
c6 :: c1:c2 -> c3:c4 -> c5:c6
foldr#3 :: Nil:Cons -> step_x_f:fleft_op_e_xs_1
step_x_f#1 :: rev_l -> a -> step_x_f:fleft_op_e_xs_1 -> Nil:Cons -> Nil:Cons
main :: Nil:Cons -> Nil:Cons
hole_c1_7 :: c
hole_Nil:Cons2_7 :: Nil:Cons
hole_a3_7 :: a
hole_c1:c24_7 :: c1:c2
hole_rev_l5_7 :: rev_l
hole_step_x_f:fleft_op_e_xs_16_7 :: step_x_f:fleft_op_e_xs_1
hole_c3:c47_7 :: c3:c4
hole_c5:c68_7 :: c5:c6
gen_Nil:Cons9_7 :: Nat -> Nil:Cons
gen_c1:c210_7 :: Nat -> c1:c2
gen_step_x_f:fleft_op_e_xs_111_7 :: Nat -> step_x_f:fleft_op_e_xs_1
gen_c3:c412_7 :: Nat -> c3:c4


Generator Equations:
gen_Nil:Cons9_7(0) <=> Nil
gen_Nil:Cons9_7(+(x, 1)) <=> Cons(hole_a3_7, gen_Nil:Cons9_7(x))
gen_c1:c210_7(0) <=> c2(c)
gen_c1:c210_7(+(x, 1)) <=> c1(gen_c1:c210_7(x), c)
gen_step_x_f:fleft_op_e_xs_111_7(0) <=> fleft_op_e_xs_1
gen_step_x_f:fleft_op_e_xs_111_7(+(x, 1)) <=> step_x_f(rev_l, hole_a3_7, gen_step_x_f:fleft_op_e_xs_111_7(x))
gen_c3:c412_7(0) <=> c3
gen_c3:c412_7(+(x, 1)) <=> c4(gen_c3:c412_7(x))


The following defined symbols remain to be analysed:
STEP_X_F#1, FOLDR#3, foldr#3, step_x_f#1
----------------------------------------

(18) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(19)
BOUNDS(n^1, INF)

----------------------------------------

(20)
Obligation:
Innermost TRS:
Rules:
REV_L#2(z0, z1) -> c
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) -> c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)), REV_L#2(z4, z0))
STEP_X_F#1(rev_l, z0, fleft_op_e_xs_1, z1) -> c2(REV_L#2(z1, z0))
FOLDR#3(Nil) -> c3
FOLDR#3(Cons(z0, z1)) -> c4(FOLDR#3(z1))
MAIN(Nil) -> c5
MAIN(Cons(z0, z1)) -> c6(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil), FOLDR#3(z1))
rev_l#2(z0, z1) -> Cons(z1, z0)
step_x_f#1(rev_l, z0, step_x_f(z1, z2, z3), z4) -> step_x_f#1(z1, z2, z3, rev_l#2(z4, z0))
step_x_f#1(rev_l, z0, fleft_op_e_xs_1, z1) -> rev_l#2(z1, z0)
foldr#3(Nil) -> fleft_op_e_xs_1
foldr#3(Cons(z0, z1)) -> step_x_f(rev_l, z0, foldr#3(z1))
main(Nil) -> Nil
main(Cons(z0, z1)) -> step_x_f#1(rev_l, z0, foldr#3(z1), Nil)

Types:
REV_L#2 :: Nil:Cons -> a -> c
c :: c
STEP_X_F#1 :: rev_l -> a -> step_x_f:fleft_op_e_xs_1 -> Nil:Cons -> c1:c2
rev_l :: rev_l
step_x_f :: rev_l -> a -> step_x_f:fleft_op_e_xs_1 -> step_x_f:fleft_op_e_xs_1
c1 :: c1:c2 -> c -> c1:c2
rev_l#2 :: Nil:Cons -> a -> Nil:Cons
fleft_op_e_xs_1 :: step_x_f:fleft_op_e_xs_1
c2 :: c -> c1:c2
FOLDR#3 :: Nil:Cons -> c3:c4
Nil :: Nil:Cons
c3 :: c3:c4
Cons :: a -> Nil:Cons -> Nil:Cons
c4 :: c3:c4 -> c3:c4
MAIN :: Nil:Cons -> c5:c6
c5 :: c5:c6
c6 :: c1:c2 -> c3:c4 -> c5:c6
foldr#3 :: Nil:Cons -> step_x_f:fleft_op_e_xs_1
step_x_f#1 :: rev_l -> a -> step_x_f:fleft_op_e_xs_1 -> Nil:Cons -> Nil:Cons
main :: Nil:Cons -> Nil:Cons
hole_c1_7 :: c
hole_Nil:Cons2_7 :: Nil:Cons
hole_a3_7 :: a
hole_c1:c24_7 :: c1:c2
hole_rev_l5_7 :: rev_l
hole_step_x_f:fleft_op_e_xs_16_7 :: step_x_f:fleft_op_e_xs_1
hole_c3:c47_7 :: c3:c4
hole_c5:c68_7 :: c5:c6
gen_Nil:Cons9_7 :: Nat -> Nil:Cons
gen_c1:c210_7 :: Nat -> c1:c2
gen_step_x_f:fleft_op_e_xs_111_7 :: Nat -> step_x_f:fleft_op_e_xs_1
gen_c3:c412_7 :: Nat -> c3:c4


Lemmas:
STEP_X_F#1(rev_l, hole_a3_7, gen_step_x_f:fleft_op_e_xs_111_7(n14_7), gen_Nil:Cons9_7(b)) -> gen_c1:c210_7(n14_7), rt in Omega(1 + n14_7)


Generator Equations:
gen_Nil:Cons9_7(0) <=> Nil
gen_Nil:Cons9_7(+(x, 1)) <=> Cons(hole_a3_7, gen_Nil:Cons9_7(x))
gen_c1:c210_7(0) <=> c2(c)
gen_c1:c210_7(+(x, 1)) <=> c1(gen_c1:c210_7(x), c)
gen_step_x_f:fleft_op_e_xs_111_7(0) <=> fleft_op_e_xs_1
gen_step_x_f:fleft_op_e_xs_111_7(+(x, 1)) <=> step_x_f(rev_l, hole_a3_7, gen_step_x_f:fleft_op_e_xs_111_7(x))
gen_c3:c412_7(0) <=> c3
gen_c3:c412_7(+(x, 1)) <=> c4(gen_c3:c412_7(x))


The following defined symbols remain to be analysed:
FOLDR#3, foldr#3, step_x_f#1
----------------------------------------

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
FOLDR#3(gen_Nil:Cons9_7(n690_7)) -> gen_c3:c412_7(n690_7), rt in Omega(1 + n690_7)

Induction Base:
FOLDR#3(gen_Nil:Cons9_7(0)) ->_R^Omega(1)
c3

Induction Step:
FOLDR#3(gen_Nil:Cons9_7(+(n690_7, 1))) ->_R^Omega(1)
c4(FOLDR#3(gen_Nil:Cons9_7(n690_7))) ->_IH
c4(gen_c3:c412_7(c691_7))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(22)
Obligation:
Innermost TRS:
Rules:
REV_L#2(z0, z1) -> c
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) -> c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)), REV_L#2(z4, z0))
STEP_X_F#1(rev_l, z0, fleft_op_e_xs_1, z1) -> c2(REV_L#2(z1, z0))
FOLDR#3(Nil) -> c3
FOLDR#3(Cons(z0, z1)) -> c4(FOLDR#3(z1))
MAIN(Nil) -> c5
MAIN(Cons(z0, z1)) -> c6(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil), FOLDR#3(z1))
rev_l#2(z0, z1) -> Cons(z1, z0)
step_x_f#1(rev_l, z0, step_x_f(z1, z2, z3), z4) -> step_x_f#1(z1, z2, z3, rev_l#2(z4, z0))
step_x_f#1(rev_l, z0, fleft_op_e_xs_1, z1) -> rev_l#2(z1, z0)
foldr#3(Nil) -> fleft_op_e_xs_1
foldr#3(Cons(z0, z1)) -> step_x_f(rev_l, z0, foldr#3(z1))
main(Nil) -> Nil
main(Cons(z0, z1)) -> step_x_f#1(rev_l, z0, foldr#3(z1), Nil)

Types:
REV_L#2 :: Nil:Cons -> a -> c
c :: c
STEP_X_F#1 :: rev_l -> a -> step_x_f:fleft_op_e_xs_1 -> Nil:Cons -> c1:c2
rev_l :: rev_l
step_x_f :: rev_l -> a -> step_x_f:fleft_op_e_xs_1 -> step_x_f:fleft_op_e_xs_1
c1 :: c1:c2 -> c -> c1:c2
rev_l#2 :: Nil:Cons -> a -> Nil:Cons
fleft_op_e_xs_1 :: step_x_f:fleft_op_e_xs_1
c2 :: c -> c1:c2
FOLDR#3 :: Nil:Cons -> c3:c4
Nil :: Nil:Cons
c3 :: c3:c4
Cons :: a -> Nil:Cons -> Nil:Cons
c4 :: c3:c4 -> c3:c4
MAIN :: Nil:Cons -> c5:c6
c5 :: c5:c6
c6 :: c1:c2 -> c3:c4 -> c5:c6
foldr#3 :: Nil:Cons -> step_x_f:fleft_op_e_xs_1
step_x_f#1 :: rev_l -> a -> step_x_f:fleft_op_e_xs_1 -> Nil:Cons -> Nil:Cons
main :: Nil:Cons -> Nil:Cons
hole_c1_7 :: c
hole_Nil:Cons2_7 :: Nil:Cons
hole_a3_7 :: a
hole_c1:c24_7 :: c1:c2
hole_rev_l5_7 :: rev_l
hole_step_x_f:fleft_op_e_xs_16_7 :: step_x_f:fleft_op_e_xs_1
hole_c3:c47_7 :: c3:c4
hole_c5:c68_7 :: c5:c6
gen_Nil:Cons9_7 :: Nat -> Nil:Cons
gen_c1:c210_7 :: Nat -> c1:c2
gen_step_x_f:fleft_op_e_xs_111_7 :: Nat -> step_x_f:fleft_op_e_xs_1
gen_c3:c412_7 :: Nat -> c3:c4


Lemmas:
STEP_X_F#1(rev_l, hole_a3_7, gen_step_x_f:fleft_op_e_xs_111_7(n14_7), gen_Nil:Cons9_7(b)) -> gen_c1:c210_7(n14_7), rt in Omega(1 + n14_7)
FOLDR#3(gen_Nil:Cons9_7(n690_7)) -> gen_c3:c412_7(n690_7), rt in Omega(1 + n690_7)


Generator Equations:
gen_Nil:Cons9_7(0) <=> Nil
gen_Nil:Cons9_7(+(x, 1)) <=> Cons(hole_a3_7, gen_Nil:Cons9_7(x))
gen_c1:c210_7(0) <=> c2(c)
gen_c1:c210_7(+(x, 1)) <=> c1(gen_c1:c210_7(x), c)
gen_step_x_f:fleft_op_e_xs_111_7(0) <=> fleft_op_e_xs_1
gen_step_x_f:fleft_op_e_xs_111_7(+(x, 1)) <=> step_x_f(rev_l, hole_a3_7, gen_step_x_f:fleft_op_e_xs_111_7(x))
gen_c3:c412_7(0) <=> c3
gen_c3:c412_7(+(x, 1)) <=> c4(gen_c3:c412_7(x))


The following defined symbols remain to be analysed:
foldr#3, step_x_f#1
----------------------------------------

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
foldr#3(gen_Nil:Cons9_7(n1057_7)) -> gen_step_x_f:fleft_op_e_xs_111_7(n1057_7), rt in Omega(0)

Induction Base:
foldr#3(gen_Nil:Cons9_7(0)) ->_R^Omega(0)
fleft_op_e_xs_1

Induction Step:
foldr#3(gen_Nil:Cons9_7(+(n1057_7, 1))) ->_R^Omega(0)
step_x_f(rev_l, hole_a3_7, foldr#3(gen_Nil:Cons9_7(n1057_7))) ->_IH
step_x_f(rev_l, hole_a3_7, gen_step_x_f:fleft_op_e_xs_111_7(c1058_7))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(24)
Obligation:
Innermost TRS:
Rules:
REV_L#2(z0, z1) -> c
STEP_X_F#1(rev_l, z0, step_x_f(z1, z2, z3), z4) -> c1(STEP_X_F#1(z1, z2, z3, rev_l#2(z4, z0)), REV_L#2(z4, z0))
STEP_X_F#1(rev_l, z0, fleft_op_e_xs_1, z1) -> c2(REV_L#2(z1, z0))
FOLDR#3(Nil) -> c3
FOLDR#3(Cons(z0, z1)) -> c4(FOLDR#3(z1))
MAIN(Nil) -> c5
MAIN(Cons(z0, z1)) -> c6(STEP_X_F#1(rev_l, z0, foldr#3(z1), Nil), FOLDR#3(z1))
rev_l#2(z0, z1) -> Cons(z1, z0)
step_x_f#1(rev_l, z0, step_x_f(z1, z2, z3), z4) -> step_x_f#1(z1, z2, z3, rev_l#2(z4, z0))
step_x_f#1(rev_l, z0, fleft_op_e_xs_1, z1) -> rev_l#2(z1, z0)
foldr#3(Nil) -> fleft_op_e_xs_1
foldr#3(Cons(z0, z1)) -> step_x_f(rev_l, z0, foldr#3(z1))
main(Nil) -> Nil
main(Cons(z0, z1)) -> step_x_f#1(rev_l, z0, foldr#3(z1), Nil)

Types:
REV_L#2 :: Nil:Cons -> a -> c
c :: c
STEP_X_F#1 :: rev_l -> a -> step_x_f:fleft_op_e_xs_1 -> Nil:Cons -> c1:c2
rev_l :: rev_l
step_x_f :: rev_l -> a -> step_x_f:fleft_op_e_xs_1 -> step_x_f:fleft_op_e_xs_1
c1 :: c1:c2 -> c -> c1:c2
rev_l#2 :: Nil:Cons -> a -> Nil:Cons
fleft_op_e_xs_1 :: step_x_f:fleft_op_e_xs_1
c2 :: c -> c1:c2
FOLDR#3 :: Nil:Cons -> c3:c4
Nil :: Nil:Cons
c3 :: c3:c4
Cons :: a -> Nil:Cons -> Nil:Cons
c4 :: c3:c4 -> c3:c4
MAIN :: Nil:Cons -> c5:c6
c5 :: c5:c6
c6 :: c1:c2 -> c3:c4 -> c5:c6
foldr#3 :: Nil:Cons -> step_x_f:fleft_op_e_xs_1
step_x_f#1 :: rev_l -> a -> step_x_f:fleft_op_e_xs_1 -> Nil:Cons -> Nil:Cons
main :: Nil:Cons -> Nil:Cons
hole_c1_7 :: c
hole_Nil:Cons2_7 :: Nil:Cons
hole_a3_7 :: a
hole_c1:c24_7 :: c1:c2
hole_rev_l5_7 :: rev_l
hole_step_x_f:fleft_op_e_xs_16_7 :: step_x_f:fleft_op_e_xs_1
hole_c3:c47_7 :: c3:c4
hole_c5:c68_7 :: c5:c6
gen_Nil:Cons9_7 :: Nat -> Nil:Cons
gen_c1:c210_7 :: Nat -> c1:c2
gen_step_x_f:fleft_op_e_xs_111_7 :: Nat -> step_x_f:fleft_op_e_xs_1
gen_c3:c412_7 :: Nat -> c3:c4


Lemmas:
STEP_X_F#1(rev_l, hole_a3_7, gen_step_x_f:fleft_op_e_xs_111_7(n14_7), gen_Nil:Cons9_7(b)) -> gen_c1:c210_7(n14_7), rt in Omega(1 + n14_7)
FOLDR#3(gen_Nil:Cons9_7(n690_7)) -> gen_c3:c412_7(n690_7), rt in Omega(1 + n690_7)
foldr#3(gen_Nil:Cons9_7(n1057_7)) -> gen_step_x_f:fleft_op_e_xs_111_7(n1057_7), rt in Omega(0)


Generator Equations:
gen_Nil:Cons9_7(0) <=> Nil
gen_Nil:Cons9_7(+(x, 1)) <=> Cons(hole_a3_7, gen_Nil:Cons9_7(x))
gen_c1:c210_7(0) <=> c2(c)
gen_c1:c210_7(+(x, 1)) <=> c1(gen_c1:c210_7(x), c)
gen_step_x_f:fleft_op_e_xs_111_7(0) <=> fleft_op_e_xs_1
gen_step_x_f:fleft_op_e_xs_111_7(+(x, 1)) <=> step_x_f(rev_l, hole_a3_7, gen_step_x_f:fleft_op_e_xs_111_7(x))
gen_c3:c412_7(0) <=> c3
gen_c3:c412_7(+(x, 1)) <=> c4(gen_c3:c412_7(x))


The following defined symbols remain to be analysed:
step_x_f#1
----------------------------------------

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
step_x_f#1(rev_l, hole_a3_7, gen_step_x_f:fleft_op_e_xs_111_7(n1394_7), gen_Nil:Cons9_7(b)) -> gen_Nil:Cons9_7(+(+(1, n1394_7), b)), rt in Omega(0)

Induction Base:
step_x_f#1(rev_l, hole_a3_7, gen_step_x_f:fleft_op_e_xs_111_7(0), gen_Nil:Cons9_7(b)) ->_R^Omega(0)
rev_l#2(gen_Nil:Cons9_7(b), hole_a3_7) ->_R^Omega(0)
Cons(hole_a3_7, gen_Nil:Cons9_7(b))

Induction Step:
step_x_f#1(rev_l, hole_a3_7, gen_step_x_f:fleft_op_e_xs_111_7(+(n1394_7, 1)), gen_Nil:Cons9_7(b)) ->_R^Omega(0)
step_x_f#1(rev_l, hole_a3_7, gen_step_x_f:fleft_op_e_xs_111_7(n1394_7), rev_l#2(gen_Nil:Cons9_7(b), hole_a3_7)) ->_R^Omega(0)
step_x_f#1(rev_l, hole_a3_7, gen_step_x_f:fleft_op_e_xs_111_7(n1394_7), Cons(hole_a3_7, gen_Nil:Cons9_7(b))) ->_IH
gen_Nil:Cons9_7(+(+(1, +(b, 1)), c1395_7))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(26)
BOUNDS(1, INF)