MAYBE * Step 1: DependencyPairs MAYBE + 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: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1() cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4,x8,x12,bot[0]()) ,x16) ,fibs_2#1#(x4,x8,x12,bot[0]())) cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16),zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())) cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4) ,fibs_2#1#(x1,x2,x3,bot[6]())) cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())) cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3)) fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs(),fibs_2(zipwith_l(),plus(),tail_l()))) main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12)) plus#2#(0(),x12) -> c_9() plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)) zipwith_l#3#(x8,x4) -> c_11() zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(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) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2) ,fibs_2#1#(x3,x4,x5,bot[7]())) zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1() cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4,x8,x12,bot[0]()) ,x16) ,fibs_2#1#(x4,x8,x12,bot[0]())) cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16) ,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())) cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4) ,fibs_2#1#(x1,x2,x3,bot[6]())) cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())) cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3)) fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs(),fibs_2(zipwith_l(),plus(),tail_l()))) main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12)) plus#2#(0(),x12) -> c_9() plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)) zipwith_l#3#(x8,x4) -> c_11() zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(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) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2) ,fibs_2#1#(x3,x4,x5,bot[7]())) zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())) - Weak 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,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,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/2,c_7/1,c_8/1,c_9/0,c_10/1,c_11/0,c_12/1,c_13/2 ,c_14/2} - 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: UsableRules + Details: We replace rewrite rules by usable rules: 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()))) 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) cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1() cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4,x8,x12,bot[0]()) ,x16) ,fibs_2#1#(x4,x8,x12,bot[0]())) cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16),zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())) cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4) ,fibs_2#1#(x1,x2,x3,bot[6]())) cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())) cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3)) fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs(),fibs_2(zipwith_l(),plus(),tail_l()))) main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12)) plus#2#(0(),x12) -> c_9() plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)) zipwith_l#3#(x8,x4) -> c_11() zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(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) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2) ,fibs_2#1#(x3,x4,x5,bot[7]())) zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1() cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4,x8,x12,bot[0]()) ,x16) ,fibs_2#1#(x4,x8,x12,bot[0]())) cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16) ,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())) cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4) ,fibs_2#1#(x1,x2,x3,bot[6]())) cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())) cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3)) fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs(),fibs_2(zipwith_l(),plus(),tail_l()))) main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12)) plus#2#(0(),x12) -> c_9() plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)) zipwith_l#3#(x8,x4) -> c_11() zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(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) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2) ,fibs_2#1#(x3,x4,x5,bot[7]())) zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())) - Weak TRS: 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()))) 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,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,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/2,c_7/1,c_8/1,c_9/0,c_10/1,c_11/0,c_12/1,c_13/2 ,c_14/2} - 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: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,9,11} by application of Pre({1,9,11}) = {2,3,6,7,8,10}. Here rules are labelled as follows: 1: cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1() 2: cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4 ,x8 ,x12 ,bot[0]()) ,x16) ,fibs_2#1#(x4,x8,x12,bot[0]())) 3: cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16) ,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())) 4: cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4) ,fibs_2#1#(x1,x2,x3,bot[6]())) 5: cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())) 6: cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3)) 7: fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs() ,fibs_2(zipwith_l(),plus(),tail_l()))) 8: main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12)) 9: plus#2#(0(),x12) -> c_9() 10: plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)) 11: zipwith_l#3#(x8,x4) -> c_11() 12: zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0() ,fibs_2(zipwith_l() ,plus() ,tail_l())) ,x5)) 13: zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2) ,fibs_2#1#(x3,x4,x5,bot[7]())) 14: zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())) * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4,x8,x12,bot[0]()) ,x16) ,fibs_2#1#(x4,x8,x12,bot[0]())) cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16) ,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())) cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4) ,fibs_2#1#(x1,x2,x3,bot[6]())) cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())) cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3)) fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs(),fibs_2(zipwith_l(),plus(),tail_l()))) main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12)) plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)) zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(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) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2) ,fibs_2#1#(x3,x4,x5,bot[7]())) zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())) - Weak DPs: cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1() plus#2#(0(),x12) -> c_9() zipwith_l#3#(x8,x4) -> c_11() - Weak TRS: 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()))) 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,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,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/2,c_7/1,c_8/1,c_9/0,c_10/1,c_11/0,c_12/1,c_13/2 ,c_14/2} - 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: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {6} by application of Pre({6}) = {1,3,10}. Here rules are labelled as follows: 1: cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4 ,x8 ,x12 ,bot[0]()) ,x16) ,fibs_2#1#(x4,x8,x12,bot[0]())) 2: cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16) ,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())) 3: cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4) ,fibs_2#1#(x1,x2,x3,bot[6]())) 4: cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())) 5: cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3)) 6: fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs() ,fibs_2(zipwith_l(),plus(),tail_l()))) 7: main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12)) 8: plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)) 9: zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0() ,fibs_2(zipwith_l() ,plus() ,tail_l())) ,x5)) 10: zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2) ,fibs_2#1#(x3,x4,x5,bot[7]())) 11: zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())) 12: cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1() 13: plus#2#(0(),x12) -> c_9() 14: zipwith_l#3#(x8,x4) -> c_11() * Step 5: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4,x8,x12,bot[0]()) ,x16) ,fibs_2#1#(x4,x8,x12,bot[0]())) cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16) ,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())) cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4) ,fibs_2#1#(x1,x2,x3,bot[6]())) cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())) cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3)) main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12)) plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)) zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(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) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2) ,fibs_2#1#(x3,x4,x5,bot[7]())) zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())) - Weak DPs: cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1() fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs(),fibs_2(zipwith_l(),plus(),tail_l()))) plus#2#(0(),x12) -> c_9() zipwith_l#3#(x8,x4) -> c_11() - Weak TRS: 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()))) 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,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,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/2,c_7/1,c_8/1,c_9/0,c_10/1,c_11/0,c_12/1,c_13/2 ,c_14/2} - 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: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4 ,x8 ,x12 ,bot[0]()) ,x16) ,fibs_2#1#(x4,x8,x12,bot[0]())) -->_2 fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs() ,fibs_2(zipwith_l() ,plus() ,tail_l()))):12 -->_1 cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16) ,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())):2 -->_1 cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1():11 -->_1 cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4 ,x8 ,x12 ,bot[0]()) ,x16) ,fibs_2#1#(x4,x8,x12,bot[0]())):1 2:S:cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16) ,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())) -->_2 zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())):10 -->_2 zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2) ,fibs_2#1#(x3,x4,x5,bot[7]())):9 -->_2 zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0() ,fibs_2(zipwith_l() ,plus() ,tail_l())) ,x5)):8 -->_1 cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1():11 -->_1 cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16) ,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())):2 -->_1 cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4 ,x8 ,x12 ,bot[0]()) ,x16) ,fibs_2#1#(x4,x8,x12,bot[0]())):1 3:S:cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4) ,fibs_2#1#(x1,x2,x3,bot[6]())) -->_2 fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs() ,fibs_2(zipwith_l() ,plus() ,tail_l()))):12 -->_1 cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3)):5 4:S:cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())) -->_2 zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())):10 -->_2 zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2) ,fibs_2#1#(x3,x4,x5,bot[7]())):9 -->_2 zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0() ,fibs_2(zipwith_l() ,plus() ,tail_l())) ,x5)):8 -->_1 cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3)):5 5:S:cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3)) -->_1 plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)):7 -->_2 zipwith_l#3#(x8,x4) -> c_11():14 -->_1 plus#2#(0(),x12) -> c_9():13 6:S:main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12)) -->_1 cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1():11 -->_1 cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4 ,x8 ,x12 ,bot[0]()) ,x16) ,fibs_2#1#(x4,x8,x12,bot[0]())):1 7:S:plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)) -->_1 plus#2#(0(),x12) -> c_9():13 -->_1 plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)):7 8:S:zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0() ,fibs_2(zipwith_l() ,plus() ,tail_l())) ,x5)) -->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())):4 -->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4) ,fibs_2#1#(x1,x2,x3,bot[6]())):3 9:S:zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2) ,fibs_2#1#(x3,x4,x5,bot[7]())) -->_2 fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs() ,fibs_2(zipwith_l() ,plus() ,tail_l()))):12 -->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())):4 -->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4) ,fibs_2#1#(x1,x2,x3,bot[6]())):3 10:S:zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())) -->_2 zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())):10 -->_2 zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2) ,fibs_2#1#(x3,x4,x5,bot[7]())):9 -->_2 zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0() ,fibs_2(zipwith_l() ,plus() ,tail_l())) ,x5)):8 -->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())):4 -->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4) ,fibs_2#1#(x1,x2,x3,bot[6]())):3 11:W:cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1() 12:W:fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs() ,fibs_2(zipwith_l(),plus(),tail_l()))) -->_1 zipwith_l#3#(x8,x4) -> c_11():14 13:W:plus#2#(0(),x12) -> c_9() 14:W:zipwith_l#3#(x8,x4) -> c_11() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 11: cond_take_l_n_xs#(ConsL(x16,x18),0()) -> c_1() 13: plus#2#(0(),x12) -> c_9() 12: fibs_2#1#(zipwith_l(),plus(),tail_l(),x3) -> c_7(zipwith_l#3#(fibs() ,fibs_2(zipwith_l(),plus(),tail_l()))) 14: zipwith_l#3#(x8,x4) -> c_11() * Step 6: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4,x8,x12,bot[0]()) ,x16) ,fibs_2#1#(x4,x8,x12,bot[0]())) cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16) ,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())) cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4) ,fibs_2#1#(x1,x2,x3,bot[6]())) cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())) cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3)) main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12)) plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)) zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(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) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2) ,fibs_2#1#(x3,x4,x5,bot[7]())) zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())) - Weak TRS: 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()))) 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,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,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/2,c_7/1,c_8/1,c_9/0,c_10/1,c_11/0,c_12/1,c_13/2 ,c_14/2} - 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: SimplifyRHS + Details: Consider the dependency graph 1:S:cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4 ,x8 ,x12 ,bot[0]()) ,x16) ,fibs_2#1#(x4,x8,x12,bot[0]())) -->_1 cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16) ,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())):2 -->_1 cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4 ,x8 ,x12 ,bot[0]()) ,x16) ,fibs_2#1#(x4,x8,x12,bot[0]())):1 2:S:cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16) ,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())) -->_2 zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())):10 -->_2 zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2) ,fibs_2#1#(x3,x4,x5,bot[7]())):9 -->_2 zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0() ,fibs_2(zipwith_l() ,plus() ,tail_l())) ,x5)):8 -->_1 cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16) ,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())):2 -->_1 cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4 ,x8 ,x12 ,bot[0]()) ,x16) ,fibs_2#1#(x4,x8,x12,bot[0]())):1 3:S:cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4) ,fibs_2#1#(x1,x2,x3,bot[6]())) -->_1 cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3)):5 4:S:cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())) -->_2 zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())):10 -->_2 zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2) ,fibs_2#1#(x3,x4,x5,bot[7]())):9 -->_2 zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0() ,fibs_2(zipwith_l() ,plus() ,tail_l())) ,x5)):8 -->_1 cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3)):5 5:S:cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4),zipwith_l#3#(x1,x3)) -->_1 plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)):7 6:S:main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12)) -->_1 cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4 ,x8 ,x12 ,bot[0]()) ,x16) ,fibs_2#1#(x4,x8,x12,bot[0]())):1 7:S:plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)) -->_1 plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)):7 8:S:zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0() ,fibs_2(zipwith_l() ,plus() ,tail_l())) ,x5)) -->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())):4 -->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4) ,fibs_2#1#(x1,x2,x3,bot[6]())):3 9:S:zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2) ,fibs_2#1#(x3,x4,x5,bot[7]())) -->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())):4 -->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4) ,fibs_2#1#(x1,x2,x3,bot[6]())):3 10:S:zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())) -->_2 zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())):10 -->_2 zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2) ,fibs_2#1#(x3,x4,x5,bot[7]())):9 -->_2 zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0() ,fibs_2(zipwith_l() ,plus() ,tail_l())) ,x5)):8 -->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())):4 -->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4) ,fibs_2#1#(x1,x2,x3,bot[6]())):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4 ,x8 ,x12 ,bot[0]()) ,x16)) cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4)) cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4)) zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2)) * Step 7: RemoveHeads MAYBE + Considered Problem: - Strict DPs: cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(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)) -> c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16) ,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())) cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(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)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())) cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4)) main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12)) plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)) zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(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) -> c_13(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) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())) - Weak TRS: 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()))) 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,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,c_1/0,c_2/1,c_3/2,c_4/1,c_5/2,c_6/1,c_7/1,c_8/1,c_9/0,c_10/1,c_11/0,c_12/1,c_13/1 ,c_14/2} - 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: RemoveHeads + Details: Consider the dependency graph 1:S:cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4 ,x8 ,x12 ,bot[0]()) ,x16)) -->_1 cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16) ,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())):2 -->_1 cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4 ,x8 ,x12 ,bot[0]()) ,x16)):1 2:S:cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16) ,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())) -->_2 zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())):10 -->_2 zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2)):9 -->_2 zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0() ,fibs_2(zipwith_l() ,plus() ,tail_l())) ,x5)):8 -->_1 cond_take_l_n_xs#(ConsL(x7,zipwith_l_f_xs_ys(x4,x8,x12)),S(x16)) -> c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16) ,zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())):2 -->_1 cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4 ,x8 ,x12 ,bot[0]()) ,x16)):1 3:S:cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4)) -->_1 cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4)):5 4:S:cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())) -->_2 zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())):10 -->_2 zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2)):9 -->_2 zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0() ,fibs_2(zipwith_l() ,plus() ,tail_l())) ,x5)):8 -->_1 cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4)):5 5:S:cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4)) -->_1 plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)):7 6:S:main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12)) -->_1 cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(cond_take_l_n_xs#(fibs_2#1(x4 ,x8 ,x12 ,bot[0]()) ,x16)):1 7:S:plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)) -->_1 plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)):7 8:S:zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0() ,fibs_2(zipwith_l() ,plus() ,tail_l())) ,x5)) -->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())):4 -->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4)):3 9:S:zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2)) -->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())):4 -->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4)):3 10:S:zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())) -->_2 zipwith_l_f_xs_ys#1#(plus(),zipwith_l_f_xs_ys(x3,x4,x5),x2,x1) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())):10 -->_2 zipwith_l_f_xs_ys#1#(plus(),fibs_2(x3,x4,x5),x2,x1) -> c_13(cond_zipwith_l_f_xs_ys#(fibs_2#1(x3 ,x4 ,x5 ,bot[7]()) ,x2)):9 -->_2 zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(cond_zipwith_l_f_xs_ys#(ConsL(0() ,fibs_2(zipwith_l() ,plus() ,tail_l())) ,x5)):8 -->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),zipwith_l_f_xs_ys(x1,x2,x3)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())):4 -->_1 cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(cond_zipwith_l_f_xs_ys_1#(fibs_2#1(x1 ,x2 ,x3 ,bot[6]()) ,x5 ,x4)):3 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(6,main#(x12) -> c_8(cond_take_l_n_xs#(ConsL(0(),fibs_2(zipwith_l(),plus(),tail_l())),x12)))] * Step 8: Failure MAYBE + Considered Problem: - Strict DPs: cond_take_l_n_xs#(ConsL(x7,fibs_2(x4,x8,x12)),S(x16)) -> c_2(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)) -> c_3(cond_take_l_n_xs#(zipwith_l_f_xs_ys#1(x4,x8,x12,bot[0]()),x16),zipwith_l_f_xs_ys#1#(x4,x8,x12,bot[0]())) cond_zipwith_l_f_xs_ys#(ConsL(x5,x4),fibs_2(x1,x2,x3)) -> c_4(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)) -> c_5(cond_zipwith_l_f_xs_ys_1#(zipwith_l_f_xs_ys#1(x1,x2,x3,bot[6]()),x5,x4) ,zipwith_l_f_xs_ys#1#(x1,x2,x3,bot[6]())) cond_zipwith_l_f_xs_ys_1#(ConsL(x4,x3),x2,x1) -> c_6(plus#2#(x2,x4)) plus#2#(S(x4),x2) -> c_10(plus#2#(x4,x2)) zipwith_l_f_xs_ys#1#(plus(),fibs(),x5,x3) -> c_12(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) -> c_13(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) -> c_14(cond_zipwith_l_f_xs_ys#(zipwith_l_f_xs_ys#1(x3,x4,x5,bot[7]()),x2) ,zipwith_l_f_xs_ys#1#(x3,x4,x5,bot[7]())) - Weak TRS: 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()))) 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,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,c_1/0,c_2/1,c_3/2,c_4/1,c_5/2,c_6/1,c_7/1,c_8/1,c_9/0,c_10/1,c_11/0,c_12/1,c_13/1 ,c_14/2} - 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: EmptyProcessor + Details: The problem is still open. MAYBE