WORST_CASE(Omega(n^1),?)
proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 1052 ms]
(2) CpxRelTRS
(3) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
(4) TRS for Loop Detection
(5) DecreasingLoopProof [LOWER BOUND(ID), 0 ms]
(6) BEST
    (7) proven lower bound
        (8) LowerBoundPropagationProof [FINISHED, 0 ms]
        (9) BOUNDS(n^1, INF)
    (10) TRS for Loop Detection


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

(0)
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:

   FIBS_2#1(zipwith_l, plus, tail_l, z0) -> c(ZIPWITH_L#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
   COND_TAKE_L_N_XS(ConsL(z0, z1), 0) -> c1
   COND_TAKE_L_N_XS(ConsL(z0, fibs_2(z1, z2, z3)), S(z4)) -> c2(COND_TAKE_L_N_XS(fibs_2#1(z1, z2, z3, bot[0]), z4), FIBS_2#1(z1, z2, z3, bot[0]))
   COND_TAKE_L_N_XS(ConsL(z0, zipwith_l_f_xs_ys(z1, z2, z3)), S(z4)) -> c3(COND_TAKE_L_N_XS(zipwith_l_f_xs_ys#1(z1, z2, z3, bot[0]), z4), ZIPWITH_L_F_XS_YS#1(z1, z2, z3, bot[0]))
   PLUS#2(0, z0) -> c4
   PLUS#2(S(z0), z1) -> c5(PLUS#2(z0, z1))
   COND_ZIPWITH_L_F_XS_YS_1(ConsL(z0, z1), z2, z3) -> c6(PLUS#2(z2, z0))
   COND_ZIPWITH_L_F_XS_YS_1(ConsL(z0, z1), z2, z3) -> c7(ZIPWITH_L#3(z3, z1))
   COND_ZIPWITH_L_F_XS_YS(ConsL(z0, z1), zipwith_l_f_xs_ys(z2, z3, z4)) -> c8(COND_ZIPWITH_L_F_XS_YS_1(zipwith_l_f_xs_ys#1(z2, z3, z4, bot[6]), z0, z1), ZIPWITH_L_F_XS_YS#1(z2, z3, z4, bot[6]))
   COND_ZIPWITH_L_F_XS_YS(ConsL(z0, z1), fibs_2(z2, z3, z4)) -> c9(COND_ZIPWITH_L_F_XS_YS_1(fibs_2#1(z2, z3, z4, bot[6]), z0, z1), FIBS_2#1(z2, z3, z4, bot[6]))
   ZIPWITH_L_F_XS_YS#1(plus, fibs, z0, z1) -> c10(COND_ZIPWITH_L_F_XS_YS(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), z0))
   ZIPWITH_L_F_XS_YS#1(plus, fibs_2(z0, z1, z2), z3, z4) -> c11(COND_ZIPWITH_L_F_XS_YS(fibs_2#1(z0, z1, z2, bot[7]), z3), FIBS_2#1(z0, z1, z2, bot[7]))
   ZIPWITH_L_F_XS_YS#1(plus, zipwith_l_f_xs_ys(z0, z1, z2), z3, z4) -> c12(COND_ZIPWITH_L_F_XS_YS(zipwith_l_f_xs_ys#1(z0, z1, z2, bot[7]), z3), ZIPWITH_L_F_XS_YS#1(z0, z1, z2, bot[7]))
   ZIPWITH_L#3(z0, z1) -> c13
   MAIN(z0) -> c14(COND_TAKE_L_N_XS(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), z0))

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

   fibs_2#1(zipwith_l, plus, tail_l, z0) -> ConsL(S(0), zipwith_l#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
   cond_take_l_n_xs(ConsL(z0, z1), 0) -> Nil
   cond_take_l_n_xs(ConsL(z0, fibs_2(z1, z2, z3)), S(z4)) -> Cons(z0, cond_take_l_n_xs(fibs_2#1(z1, z2, z3, bot[0]), z4))
   cond_take_l_n_xs(ConsL(z0, zipwith_l_f_xs_ys(z1, z2, z3)), S(z4)) -> Cons(z0, cond_take_l_n_xs(zipwith_l_f_xs_ys#1(z1, z2, z3, bot[0]), z4))
   plus#2(0, z0) -> z0
   plus#2(S(z0), z1) -> S(plus#2(z0, z1))
   cond_zipwith_l_f_xs_ys_1(ConsL(z0, z1), z2, z3) -> ConsL(plus#2(z2, z0), zipwith_l#3(z3, z1))
   cond_zipwith_l_f_xs_ys(ConsL(z0, z1), zipwith_l_f_xs_ys(z2, z3, z4)) -> cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(z2, z3, z4, bot[6]), z0, z1)
   cond_zipwith_l_f_xs_ys(ConsL(z0, z1), fibs_2(z2, z3, z4)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(z2, z3, z4, bot[6]), z0, z1)
   zipwith_l_f_xs_ys#1(plus, fibs, z0, z1) -> cond_zipwith_l_f_xs_ys(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), z0)
   zipwith_l_f_xs_ys#1(plus, fibs_2(z0, z1, z2), z3, z4) -> cond_zipwith_l_f_xs_ys(fibs_2#1(z0, z1, z2, bot[7]), z3)
   zipwith_l_f_xs_ys#1(plus, zipwith_l_f_xs_ys(z0, z1, z2), z3, z4) -> cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(z0, z1, z2, bot[7]), z3)
   zipwith_l#3(z0, z1) -> zipwith_l_f_xs_ys(plus, z0, z1)
   main(z0) -> cond_take_l_n_xs(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), z0)

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

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

(2)
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:

   FIBS_2#1(zipwith_l, plus, tail_l, z0) -> c(ZIPWITH_L#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
   COND_TAKE_L_N_XS(ConsL(z0, z1), 0) -> c1
   COND_TAKE_L_N_XS(ConsL(z0, fibs_2(z1, z2, z3)), S(z4)) -> c2(COND_TAKE_L_N_XS(fibs_2#1(z1, z2, z3, bot[0]), z4), FIBS_2#1(z1, z2, z3, bot[0]))
   COND_TAKE_L_N_XS(ConsL(z0, zipwith_l_f_xs_ys(z1, z2, z3)), S(z4)) -> c3(COND_TAKE_L_N_XS(zipwith_l_f_xs_ys#1(z1, z2, z3, bot[0]), z4), ZIPWITH_L_F_XS_YS#1(z1, z2, z3, bot[0]))
   PLUS#2(0, z0) -> c4
   PLUS#2(S(z0), z1) -> c5(PLUS#2(z0, z1))
   COND_ZIPWITH_L_F_XS_YS_1(ConsL(z0, z1), z2, z3) -> c6(PLUS#2(z2, z0))
   COND_ZIPWITH_L_F_XS_YS_1(ConsL(z0, z1), z2, z3) -> c7(ZIPWITH_L#3(z3, z1))
   COND_ZIPWITH_L_F_XS_YS(ConsL(z0, z1), zipwith_l_f_xs_ys(z2, z3, z4)) -> c8(COND_ZIPWITH_L_F_XS_YS_1(zipwith_l_f_xs_ys#1(z2, z3, z4, bot[6]), z0, z1), ZIPWITH_L_F_XS_YS#1(z2, z3, z4, bot[6]))
   COND_ZIPWITH_L_F_XS_YS(ConsL(z0, z1), fibs_2(z2, z3, z4)) -> c9(COND_ZIPWITH_L_F_XS_YS_1(fibs_2#1(z2, z3, z4, bot[6]), z0, z1), FIBS_2#1(z2, z3, z4, bot[6]))
   ZIPWITH_L_F_XS_YS#1(plus, fibs, z0, z1) -> c10(COND_ZIPWITH_L_F_XS_YS(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), z0))
   ZIPWITH_L_F_XS_YS#1(plus, fibs_2(z0, z1, z2), z3, z4) -> c11(COND_ZIPWITH_L_F_XS_YS(fibs_2#1(z0, z1, z2, bot[7]), z3), FIBS_2#1(z0, z1, z2, bot[7]))
   ZIPWITH_L_F_XS_YS#1(plus, zipwith_l_f_xs_ys(z0, z1, z2), z3, z4) -> c12(COND_ZIPWITH_L_F_XS_YS(zipwith_l_f_xs_ys#1(z0, z1, z2, bot[7]), z3), ZIPWITH_L_F_XS_YS#1(z0, z1, z2, bot[7]))
   ZIPWITH_L#3(z0, z1) -> c13
   MAIN(z0) -> c14(COND_TAKE_L_N_XS(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), z0))

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

   fibs_2#1(zipwith_l, plus, tail_l, z0) -> ConsL(S(0), zipwith_l#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
   cond_take_l_n_xs(ConsL(z0, z1), 0) -> Nil
   cond_take_l_n_xs(ConsL(z0, fibs_2(z1, z2, z3)), S(z4)) -> Cons(z0, cond_take_l_n_xs(fibs_2#1(z1, z2, z3, bot[0]), z4))
   cond_take_l_n_xs(ConsL(z0, zipwith_l_f_xs_ys(z1, z2, z3)), S(z4)) -> Cons(z0, cond_take_l_n_xs(zipwith_l_f_xs_ys#1(z1, z2, z3, bot[0]), z4))
   plus#2(0, z0) -> z0
   plus#2(S(z0), z1) -> S(plus#2(z0, z1))
   cond_zipwith_l_f_xs_ys_1(ConsL(z0, z1), z2, z3) -> ConsL(plus#2(z2, z0), zipwith_l#3(z3, z1))
   cond_zipwith_l_f_xs_ys(ConsL(z0, z1), zipwith_l_f_xs_ys(z2, z3, z4)) -> cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(z2, z3, z4, bot[6]), z0, z1)
   cond_zipwith_l_f_xs_ys(ConsL(z0, z1), fibs_2(z2, z3, z4)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(z2, z3, z4, bot[6]), z0, z1)
   zipwith_l_f_xs_ys#1(plus, fibs, z0, z1) -> cond_zipwith_l_f_xs_ys(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), z0)
   zipwith_l_f_xs_ys#1(plus, fibs_2(z0, z1, z2), z3, z4) -> cond_zipwith_l_f_xs_ys(fibs_2#1(z0, z1, z2, bot[7]), z3)
   zipwith_l_f_xs_ys#1(plus, zipwith_l_f_xs_ys(z0, z1, z2), z3, z4) -> cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(z0, z1, z2, bot[7]), z3)
   zipwith_l#3(z0, z1) -> zipwith_l_f_xs_ys(plus, z0, z1)
   main(z0) -> cond_take_l_n_xs(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), z0)

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

(3) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID))
Transformed a relative TRS into a decreasing-loop problem.
----------------------------------------

(4)
Obligation:
Analyzing the following TRS for decreasing loops:

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:

   FIBS_2#1(zipwith_l, plus, tail_l, z0) -> c(ZIPWITH_L#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
   COND_TAKE_L_N_XS(ConsL(z0, z1), 0) -> c1
   COND_TAKE_L_N_XS(ConsL(z0, fibs_2(z1, z2, z3)), S(z4)) -> c2(COND_TAKE_L_N_XS(fibs_2#1(z1, z2, z3, bot[0]), z4), FIBS_2#1(z1, z2, z3, bot[0]))
   COND_TAKE_L_N_XS(ConsL(z0, zipwith_l_f_xs_ys(z1, z2, z3)), S(z4)) -> c3(COND_TAKE_L_N_XS(zipwith_l_f_xs_ys#1(z1, z2, z3, bot[0]), z4), ZIPWITH_L_F_XS_YS#1(z1, z2, z3, bot[0]))
   PLUS#2(0, z0) -> c4
   PLUS#2(S(z0), z1) -> c5(PLUS#2(z0, z1))
   COND_ZIPWITH_L_F_XS_YS_1(ConsL(z0, z1), z2, z3) -> c6(PLUS#2(z2, z0))
   COND_ZIPWITH_L_F_XS_YS_1(ConsL(z0, z1), z2, z3) -> c7(ZIPWITH_L#3(z3, z1))
   COND_ZIPWITH_L_F_XS_YS(ConsL(z0, z1), zipwith_l_f_xs_ys(z2, z3, z4)) -> c8(COND_ZIPWITH_L_F_XS_YS_1(zipwith_l_f_xs_ys#1(z2, z3, z4, bot[6]), z0, z1), ZIPWITH_L_F_XS_YS#1(z2, z3, z4, bot[6]))
   COND_ZIPWITH_L_F_XS_YS(ConsL(z0, z1), fibs_2(z2, z3, z4)) -> c9(COND_ZIPWITH_L_F_XS_YS_1(fibs_2#1(z2, z3, z4, bot[6]), z0, z1), FIBS_2#1(z2, z3, z4, bot[6]))
   ZIPWITH_L_F_XS_YS#1(plus, fibs, z0, z1) -> c10(COND_ZIPWITH_L_F_XS_YS(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), z0))
   ZIPWITH_L_F_XS_YS#1(plus, fibs_2(z0, z1, z2), z3, z4) -> c11(COND_ZIPWITH_L_F_XS_YS(fibs_2#1(z0, z1, z2, bot[7]), z3), FIBS_2#1(z0, z1, z2, bot[7]))
   ZIPWITH_L_F_XS_YS#1(plus, zipwith_l_f_xs_ys(z0, z1, z2), z3, z4) -> c12(COND_ZIPWITH_L_F_XS_YS(zipwith_l_f_xs_ys#1(z0, z1, z2, bot[7]), z3), ZIPWITH_L_F_XS_YS#1(z0, z1, z2, bot[7]))
   ZIPWITH_L#3(z0, z1) -> c13
   MAIN(z0) -> c14(COND_TAKE_L_N_XS(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), z0))

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

   fibs_2#1(zipwith_l, plus, tail_l, z0) -> ConsL(S(0), zipwith_l#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
   cond_take_l_n_xs(ConsL(z0, z1), 0) -> Nil
   cond_take_l_n_xs(ConsL(z0, fibs_2(z1, z2, z3)), S(z4)) -> Cons(z0, cond_take_l_n_xs(fibs_2#1(z1, z2, z3, bot[0]), z4))
   cond_take_l_n_xs(ConsL(z0, zipwith_l_f_xs_ys(z1, z2, z3)), S(z4)) -> Cons(z0, cond_take_l_n_xs(zipwith_l_f_xs_ys#1(z1, z2, z3, bot[0]), z4))
   plus#2(0, z0) -> z0
   plus#2(S(z0), z1) -> S(plus#2(z0, z1))
   cond_zipwith_l_f_xs_ys_1(ConsL(z0, z1), z2, z3) -> ConsL(plus#2(z2, z0), zipwith_l#3(z3, z1))
   cond_zipwith_l_f_xs_ys(ConsL(z0, z1), zipwith_l_f_xs_ys(z2, z3, z4)) -> cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(z2, z3, z4, bot[6]), z0, z1)
   cond_zipwith_l_f_xs_ys(ConsL(z0, z1), fibs_2(z2, z3, z4)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(z2, z3, z4, bot[6]), z0, z1)
   zipwith_l_f_xs_ys#1(plus, fibs, z0, z1) -> cond_zipwith_l_f_xs_ys(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), z0)
   zipwith_l_f_xs_ys#1(plus, fibs_2(z0, z1, z2), z3, z4) -> cond_zipwith_l_f_xs_ys(fibs_2#1(z0, z1, z2, bot[7]), z3)
   zipwith_l_f_xs_ys#1(plus, zipwith_l_f_xs_ys(z0, z1, z2), z3, z4) -> cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(z0, z1, z2, bot[7]), z3)
   zipwith_l#3(z0, z1) -> zipwith_l_f_xs_ys(plus, z0, z1)
   main(z0) -> cond_take_l_n_xs(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), z0)

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

(5) DecreasingLoopProof (LOWER BOUND(ID))
The following loop(s) give(s) rise to the lower bound Omega(n^1):

The rewrite sequence

PLUS#2(S(z0), z1) ->^+ c5(PLUS#2(z0, z1))

gives rise to a decreasing loop by considering the right hand sides subterm at position [0].

The pumping substitution is [z0 / S(z0)].

The result substitution is [ ].




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

(6)
Complex Obligation (BEST)

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

(7)
Obligation:
Proved the lower bound n^1 for the following 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:

   FIBS_2#1(zipwith_l, plus, tail_l, z0) -> c(ZIPWITH_L#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
   COND_TAKE_L_N_XS(ConsL(z0, z1), 0) -> c1
   COND_TAKE_L_N_XS(ConsL(z0, fibs_2(z1, z2, z3)), S(z4)) -> c2(COND_TAKE_L_N_XS(fibs_2#1(z1, z2, z3, bot[0]), z4), FIBS_2#1(z1, z2, z3, bot[0]))
   COND_TAKE_L_N_XS(ConsL(z0, zipwith_l_f_xs_ys(z1, z2, z3)), S(z4)) -> c3(COND_TAKE_L_N_XS(zipwith_l_f_xs_ys#1(z1, z2, z3, bot[0]), z4), ZIPWITH_L_F_XS_YS#1(z1, z2, z3, bot[0]))
   PLUS#2(0, z0) -> c4
   PLUS#2(S(z0), z1) -> c5(PLUS#2(z0, z1))
   COND_ZIPWITH_L_F_XS_YS_1(ConsL(z0, z1), z2, z3) -> c6(PLUS#2(z2, z0))
   COND_ZIPWITH_L_F_XS_YS_1(ConsL(z0, z1), z2, z3) -> c7(ZIPWITH_L#3(z3, z1))
   COND_ZIPWITH_L_F_XS_YS(ConsL(z0, z1), zipwith_l_f_xs_ys(z2, z3, z4)) -> c8(COND_ZIPWITH_L_F_XS_YS_1(zipwith_l_f_xs_ys#1(z2, z3, z4, bot[6]), z0, z1), ZIPWITH_L_F_XS_YS#1(z2, z3, z4, bot[6]))
   COND_ZIPWITH_L_F_XS_YS(ConsL(z0, z1), fibs_2(z2, z3, z4)) -> c9(COND_ZIPWITH_L_F_XS_YS_1(fibs_2#1(z2, z3, z4, bot[6]), z0, z1), FIBS_2#1(z2, z3, z4, bot[6]))
   ZIPWITH_L_F_XS_YS#1(plus, fibs, z0, z1) -> c10(COND_ZIPWITH_L_F_XS_YS(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), z0))
   ZIPWITH_L_F_XS_YS#1(plus, fibs_2(z0, z1, z2), z3, z4) -> c11(COND_ZIPWITH_L_F_XS_YS(fibs_2#1(z0, z1, z2, bot[7]), z3), FIBS_2#1(z0, z1, z2, bot[7]))
   ZIPWITH_L_F_XS_YS#1(plus, zipwith_l_f_xs_ys(z0, z1, z2), z3, z4) -> c12(COND_ZIPWITH_L_F_XS_YS(zipwith_l_f_xs_ys#1(z0, z1, z2, bot[7]), z3), ZIPWITH_L_F_XS_YS#1(z0, z1, z2, bot[7]))
   ZIPWITH_L#3(z0, z1) -> c13
   MAIN(z0) -> c14(COND_TAKE_L_N_XS(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), z0))

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

   fibs_2#1(zipwith_l, plus, tail_l, z0) -> ConsL(S(0), zipwith_l#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
   cond_take_l_n_xs(ConsL(z0, z1), 0) -> Nil
   cond_take_l_n_xs(ConsL(z0, fibs_2(z1, z2, z3)), S(z4)) -> Cons(z0, cond_take_l_n_xs(fibs_2#1(z1, z2, z3, bot[0]), z4))
   cond_take_l_n_xs(ConsL(z0, zipwith_l_f_xs_ys(z1, z2, z3)), S(z4)) -> Cons(z0, cond_take_l_n_xs(zipwith_l_f_xs_ys#1(z1, z2, z3, bot[0]), z4))
   plus#2(0, z0) -> z0
   plus#2(S(z0), z1) -> S(plus#2(z0, z1))
   cond_zipwith_l_f_xs_ys_1(ConsL(z0, z1), z2, z3) -> ConsL(plus#2(z2, z0), zipwith_l#3(z3, z1))
   cond_zipwith_l_f_xs_ys(ConsL(z0, z1), zipwith_l_f_xs_ys(z2, z3, z4)) -> cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(z2, z3, z4, bot[6]), z0, z1)
   cond_zipwith_l_f_xs_ys(ConsL(z0, z1), fibs_2(z2, z3, z4)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(z2, z3, z4, bot[6]), z0, z1)
   zipwith_l_f_xs_ys#1(plus, fibs, z0, z1) -> cond_zipwith_l_f_xs_ys(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), z0)
   zipwith_l_f_xs_ys#1(plus, fibs_2(z0, z1, z2), z3, z4) -> cond_zipwith_l_f_xs_ys(fibs_2#1(z0, z1, z2, bot[7]), z3)
   zipwith_l_f_xs_ys#1(plus, zipwith_l_f_xs_ys(z0, z1, z2), z3, z4) -> cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(z0, z1, z2, bot[7]), z3)
   zipwith_l#3(z0, z1) -> zipwith_l_f_xs_ys(plus, z0, z1)
   main(z0) -> cond_take_l_n_xs(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), z0)

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

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

(9)
BOUNDS(n^1, INF)

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

(10)
Obligation:
Analyzing the following TRS for decreasing loops:

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:

   FIBS_2#1(zipwith_l, plus, tail_l, z0) -> c(ZIPWITH_L#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
   COND_TAKE_L_N_XS(ConsL(z0, z1), 0) -> c1
   COND_TAKE_L_N_XS(ConsL(z0, fibs_2(z1, z2, z3)), S(z4)) -> c2(COND_TAKE_L_N_XS(fibs_2#1(z1, z2, z3, bot[0]), z4), FIBS_2#1(z1, z2, z3, bot[0]))
   COND_TAKE_L_N_XS(ConsL(z0, zipwith_l_f_xs_ys(z1, z2, z3)), S(z4)) -> c3(COND_TAKE_L_N_XS(zipwith_l_f_xs_ys#1(z1, z2, z3, bot[0]), z4), ZIPWITH_L_F_XS_YS#1(z1, z2, z3, bot[0]))
   PLUS#2(0, z0) -> c4
   PLUS#2(S(z0), z1) -> c5(PLUS#2(z0, z1))
   COND_ZIPWITH_L_F_XS_YS_1(ConsL(z0, z1), z2, z3) -> c6(PLUS#2(z2, z0))
   COND_ZIPWITH_L_F_XS_YS_1(ConsL(z0, z1), z2, z3) -> c7(ZIPWITH_L#3(z3, z1))
   COND_ZIPWITH_L_F_XS_YS(ConsL(z0, z1), zipwith_l_f_xs_ys(z2, z3, z4)) -> c8(COND_ZIPWITH_L_F_XS_YS_1(zipwith_l_f_xs_ys#1(z2, z3, z4, bot[6]), z0, z1), ZIPWITH_L_F_XS_YS#1(z2, z3, z4, bot[6]))
   COND_ZIPWITH_L_F_XS_YS(ConsL(z0, z1), fibs_2(z2, z3, z4)) -> c9(COND_ZIPWITH_L_F_XS_YS_1(fibs_2#1(z2, z3, z4, bot[6]), z0, z1), FIBS_2#1(z2, z3, z4, bot[6]))
   ZIPWITH_L_F_XS_YS#1(plus, fibs, z0, z1) -> c10(COND_ZIPWITH_L_F_XS_YS(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), z0))
   ZIPWITH_L_F_XS_YS#1(plus, fibs_2(z0, z1, z2), z3, z4) -> c11(COND_ZIPWITH_L_F_XS_YS(fibs_2#1(z0, z1, z2, bot[7]), z3), FIBS_2#1(z0, z1, z2, bot[7]))
   ZIPWITH_L_F_XS_YS#1(plus, zipwith_l_f_xs_ys(z0, z1, z2), z3, z4) -> c12(COND_ZIPWITH_L_F_XS_YS(zipwith_l_f_xs_ys#1(z0, z1, z2, bot[7]), z3), ZIPWITH_L_F_XS_YS#1(z0, z1, z2, bot[7]))
   ZIPWITH_L#3(z0, z1) -> c13
   MAIN(z0) -> c14(COND_TAKE_L_N_XS(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), z0))

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

   fibs_2#1(zipwith_l, plus, tail_l, z0) -> ConsL(S(0), zipwith_l#3(fibs, fibs_2(zipwith_l, plus, tail_l)))
   cond_take_l_n_xs(ConsL(z0, z1), 0) -> Nil
   cond_take_l_n_xs(ConsL(z0, fibs_2(z1, z2, z3)), S(z4)) -> Cons(z0, cond_take_l_n_xs(fibs_2#1(z1, z2, z3, bot[0]), z4))
   cond_take_l_n_xs(ConsL(z0, zipwith_l_f_xs_ys(z1, z2, z3)), S(z4)) -> Cons(z0, cond_take_l_n_xs(zipwith_l_f_xs_ys#1(z1, z2, z3, bot[0]), z4))
   plus#2(0, z0) -> z0
   plus#2(S(z0), z1) -> S(plus#2(z0, z1))
   cond_zipwith_l_f_xs_ys_1(ConsL(z0, z1), z2, z3) -> ConsL(plus#2(z2, z0), zipwith_l#3(z3, z1))
   cond_zipwith_l_f_xs_ys(ConsL(z0, z1), zipwith_l_f_xs_ys(z2, z3, z4)) -> cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(z2, z3, z4, bot[6]), z0, z1)
   cond_zipwith_l_f_xs_ys(ConsL(z0, z1), fibs_2(z2, z3, z4)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(z2, z3, z4, bot[6]), z0, z1)
   zipwith_l_f_xs_ys#1(plus, fibs, z0, z1) -> cond_zipwith_l_f_xs_ys(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), z0)
   zipwith_l_f_xs_ys#1(plus, fibs_2(z0, z1, z2), z3, z4) -> cond_zipwith_l_f_xs_ys(fibs_2#1(z0, z1, z2, bot[7]), z3)
   zipwith_l_f_xs_ys#1(plus, zipwith_l_f_xs_ys(z0, z1, z2), z3, z4) -> cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(z0, z1, z2, bot[7]), z3)
   zipwith_l#3(z0, z1) -> zipwith_l_f_xs_ys(plus, z0, z1)
   main(z0) -> cond_take_l_n_xs(ConsL(0, fibs_2(zipwith_l, plus, tail_l)), z0)

Rewrite Strategy: INNERMOST