* Step 1: Sum WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
cond_take_l_n_xs(ConsL(x16,x18),0()) -> Nil()
cond_take_l_n_xs(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> Cons(x7
,cond_take_l_n_xs(fibs_2#1(x4,x8,x12,bot[0]())
,x16))
cond_take_l_n_xs(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> Cons(x7
,cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x4
,x8
,x12
,bot[0]())
,x16))
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
cond_zipwith_l_f_xs_ys_1(ConsL(x4,x3),x2,x1) -> ConsL(plus#2(x2,x4),zipwith_l#3(x1,x3))
fibs_2#1(zipwith_l(),plus(),tail_l(),x3) -> ConsL(S(0())
,zipwith_l#3(fibs(),fibs_2(zipwith_l(),plus(),tail_l())))
main(x12) -> cond_take_l_n_xs(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12)
plus#2(0(),x12) -> x12
plus#2(S(x4),x2) -> S(plus#2(x4,x2))
zipwith_l#3(x8,x4) -> zipwith_l_f_xs_ys(plus(),x8,x4)
zipwith_l_f_xs_ys#1(plus(),fibs(),x5,x3) -> cond_zipwith_l_f_xs_ys(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5)
zipwith_l_f_xs_ys#1(plus(),fibs_2(x3,x4,x5),x2,x1) -> cond_zipwith_l_f_xs_ys(fibs_2#1(x3,x4,x5,bot[7]()),x2)
zipwith_l_f_xs_ys#1(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
- Signature:
{cond_take_l_n_xs/2,cond_zipwith_l_f_xs_ys/2,cond_zipwith_l_f_xs_ys_1/3,fibs_2#1/4,main/1,plus#2/2
,zipwith_l#3/2,zipwith_l_f_xs_ys#1/4} / {0/0,Cons/2,ConsL/2,Nil/0,S/1,bot[0]/0,bot[6]/0,bot[7]/0,fibs/0
,fibs_2/3,plus/0,tail_l/0,zipwith_l/0,zipwith_l_f_xs_ys/3}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_take_l_n_xs,cond_zipwith_l_f_xs_ys
,cond_zipwith_l_f_xs_ys_1,fibs_2#1,main,plus#2,zipwith_l#3,zipwith_l_f_xs_ys#1} and constructors {0,Cons
,ConsL,Nil,S,bot[0],bot[6],bot[7],fibs,fibs_2,plus,tail_l,zipwith_l,zipwith_l_f_xs_ys}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
cond_take_l_n_xs(ConsL(x16,x18),0()) -> Nil()
cond_take_l_n_xs(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> Cons(x7
,cond_take_l_n_xs(fibs_2#1(x4,x8,x12,bot[0]())
,x16))
cond_take_l_n_xs(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> Cons(x7
,cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x4
,x8
,x12
,bot[0]())
,x16))
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1
,x2
,x3
,bot[6]())
,x5
,x4)
cond_zipwith_l_f_xs_ys(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) ->
cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4)
cond_zipwith_l_f_xs_ys_1(ConsL(x4,x3),x2,x1) -> ConsL(plus#2(x2,x4),zipwith_l#3(x1,x3))
fibs_2#1(zipwith_l(),plus(),tail_l(),x3) -> ConsL(S(0())
,zipwith_l#3(fibs(),fibs_2(zipwith_l(),plus(),tail_l())))
main(x12) -> cond_take_l_n_xs(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12)
plus#2(0(),x12) -> x12
plus#2(S(x4),x2) -> S(plus#2(x4,x2))
zipwith_l#3(x8,x4) -> zipwith_l_f_xs_ys(plus(),x8,x4)
zipwith_l_f_xs_ys#1(plus(),fibs(),x5,x3) -> cond_zipwith_l_f_xs_ys(ConsL(0()
,fibs_2(zipwith_l()
,plus()
,tail_l()))
,x5)
zipwith_l_f_xs_ys#1(plus(),fibs_2(x3,x4,x5),x2,x1) -> cond_zipwith_l_f_xs_ys(fibs_2#1(x3,x4,x5,bot[7]()),x2)
zipwith_l_f_xs_ys#1(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) ->
cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2)
- Signature:
{cond_take_l_n_xs/2,cond_zipwith_l_f_xs_ys/2,cond_zipwith_l_f_xs_ys_1/3,fibs_2#1/4,main/1,plus#2/2
,zipwith_l#3/2,zipwith_l_f_xs_ys#1/4} / {0/0,Cons/2,ConsL/2,Nil/0,S/1,bot[0]/0,bot[6]/0,bot[7]/0,fibs/0
,fibs_2/3,plus/0,tail_l/0,zipwith_l/0,zipwith_l_f_xs_ys/3}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_take_l_n_xs,cond_zipwith_l_f_xs_ys
,cond_zipwith_l_f_xs_ys_1,fibs_2#1,main,plus#2,zipwith_l#3,zipwith_l_f_xs_ys#1} and constructors {0,Cons
,ConsL,Nil,S,bot[0],bot[6],bot[7],fibs,fibs_2,plus,tail_l,zipwith_l,zipwith_l_f_xs_ys}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
plus#2(x,y){x -> S(x)} =
plus#2(S(x),y) ->^+ S(plus#2(x,y))
= C[plus#2(x,y) = plus#2(x,y){}]
WORST_CASE(Omega(n^1),?)