(GOAL COMPLEXITY) (STARTTERM CONSTRUCTOR-BASED) (STRATEGY INNERMOST) (STRATEGY INNERMOST) (VAR x1 x12 x16 x18 x2 x3 x4 x5 x7 x8) (DATATYPES A = µX.< zipwith_l, plus, tail_l, ConsL(X, X), S(X), 0, fibs, fibs_2(X, X, X), Nil, Cons(X, X), bot[0], zipwith_l_f_xs_ys(X, X, X), bot[6], bot[7] >) (SIGNATURES fibs_2#1 :: [A x A x A x A] -> A cond_take_l_n_xs :: [A x A] -> A plus#2 :: [A x A] -> A cond_zipwith_l_f_xs_ys_1 :: [A x A x A] -> A cond_zipwith_l_f_xs_ys :: [A x A] -> A zipwith_l_f_xs_ys#1 :: [A x A x A x A] -> A zipwith_l#3 :: [A x A] -> A main :: [A] -> A) (RULES fibs_2#1(zipwith_l() ,plus() ,tail_l() ,x3) -> ConsL(S(0()) ,zipwith_l#3(fibs() ,fibs_2(zipwith_l() ,plus() ,tail_l()))) 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)) plus#2(0(),x12) -> x12 plus#2(S(x4),x2) -> S(plus#2(x4 ,x2)) cond_zipwith_l_f_xs_ys_1(ConsL(x4 ,x3) ,x2 ,x1) -> ConsL(plus#2(x2,x4) ,zipwith_l#3(x1,x3)) 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(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) 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) zipwith_l#3(x8,x4) -> zipwith_l_f_xs_ys(plus(),x8,x4) main(x12) -> cond_take_l_n_xs(ConsL(0() ,fibs_2(zipwith_l() ,plus() ,tail_l())) ,x12))