WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: 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]())) 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]())) 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_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)) FIBS_2#1(zipwith_l(),plus(),tail_l(),z0) -> c(ZIPWITH_L#3(fibs(),fibs_2(zipwith_l(),plus(),tail_l()))) MAIN(z0) -> c14(COND_TAKE_L_N_XS(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),z0)) PLUS#2(0(),z0) -> c4() PLUS#2(S(z0),z1) -> c5(PLUS#2(z0,z1)) ZIPWITH_L#3(z0,z1) -> c13() 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]())) - Weak TRS: 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)) 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) 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_1(ConsL(z0,z1),z2,z3) -> ConsL(plus#2(z2,z0),zipwith_l#3(z3,z1)) fibs_2#1(zipwith_l(),plus(),tail_l(),z0) -> ConsL(S(0()) ,zipwith_l#3(fibs(),fibs_2(zipwith_l(),plus(),tail_l()))) main(z0) -> cond_take_l_n_xs(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),z0) plus#2(0(),z0) -> z0 plus#2(S(z0),z1) -> S(plus#2(z0,z1)) zipwith_l#3(z0,z1) -> zipwith_l_f_xs_ys(plus(),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) - 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,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,c/1,c1/0,c10/1,c11/2,c12/2,c13/0,c14/1,c2/2,c3/2,c4/0,c5/1,c6/1,c7/1,c8/2,c9/2,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,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],c,c1,c10,c11,c12,c13,c14,c2 ,c3,c4,c5,c6,c7,c8,c9,fibs,fibs_2,plus,tail_l,zipwith_l,zipwith_l_f_xs_ys} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: 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]())) 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]())) 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_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)) FIBS_2#1(zipwith_l(),plus(),tail_l(),z0) -> c(ZIPWITH_L#3(fibs(),fibs_2(zipwith_l(),plus(),tail_l()))) MAIN(z0) -> c14(COND_TAKE_L_N_XS(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),z0)) PLUS#2(0(),z0) -> c4() PLUS#2(S(z0),z1) -> c5(PLUS#2(z0,z1)) ZIPWITH_L#3(z0,z1) -> c13() 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]())) - Weak TRS: 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)) 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) 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_1(ConsL(z0,z1),z2,z3) -> ConsL(plus#2(z2,z0),zipwith_l#3(z3,z1)) fibs_2#1(zipwith_l(),plus(),tail_l(),z0) -> ConsL(S(0()) ,zipwith_l#3(fibs(),fibs_2(zipwith_l(),plus(),tail_l()))) main(z0) -> cond_take_l_n_xs(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),z0) plus#2(0(),z0) -> z0 plus#2(S(z0),z1) -> S(plus#2(z0,z1)) zipwith_l#3(z0,z1) -> zipwith_l_f_xs_ys(plus(),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) - 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,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,c/1,c1/0,c10/1,c11/2,c12/2,c13/0,c14/1,c2/2,c3/2,c4/0,c5/1,c6/1,c7/1,c8/2,c9/2,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,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],c,c1,c10,c11,c12,c13,c14,c2 ,c3,c4,c5,c6,c7,c8,c9,fibs,fibs_2,plus,tail_l,zipwith_l,zipwith_l_f_xs_ys} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: 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]())) 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]())) 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_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)) FIBS_2#1(zipwith_l(),plus(),tail_l(),z0) -> c(ZIPWITH_L#3(fibs(),fibs_2(zipwith_l(),plus(),tail_l()))) MAIN(z0) -> c14(COND_TAKE_L_N_XS(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),z0)) PLUS#2(0(),z0) -> c4() PLUS#2(S(z0),z1) -> c5(PLUS#2(z0,z1)) ZIPWITH_L#3(z0,z1) -> c13() 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]())) - Weak TRS: 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)) 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) 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_1(ConsL(z0,z1),z2,z3) -> ConsL(plus#2(z2,z0),zipwith_l#3(z3,z1)) fibs_2#1(zipwith_l(),plus(),tail_l(),z0) -> ConsL(S(0()) ,zipwith_l#3(fibs(),fibs_2(zipwith_l(),plus(),tail_l()))) main(z0) -> cond_take_l_n_xs(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),z0) plus#2(0(),z0) -> z0 plus#2(S(z0),z1) -> S(plus#2(z0,z1)) zipwith_l#3(z0,z1) -> zipwith_l_f_xs_ys(plus(),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) - 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,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,c/1,c1/0,c10/1,c11/2,c12/2,c13/0,c14/1,c2/2,c3/2,c4/0,c5/1,c6/1,c7/1,c8/2,c9/2,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,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],c,c1,c10,c11,c12,c13,c14,c2 ,c3,c4,c5,c6,c7,c8,c9,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) ->^+ c5(PLUS#2(x,y)) = C[PLUS#2(x,y) = PLUS#2(x,y){}] WORST_CASE(Omega(n^1),?)