YES Problem: take_l_cond(ConsL(x13,x17),0()) -> Nil() take_l_cond(ConsL(0(),fibs_1()),S(x1)) -> Cons(0(),take_l_cond(fibs_1[1](bot[0]()),x1)) take_l_cond(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> Cons(x4,take_l_cond(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1)) zipwith_l_cond_1(ConsL(x9,x7),x5,x3) -> ConsL(rec[plus_0][2](x5,x9),rec[zipwith_l_0][3](x3,x7)) zipwith_l_cond(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_cond_1(zipwith_l_f_xs_ys[1](x2,x1,bot[1]()),x4,x3) zipwith_l_cond(ConsL(x5,x3),fibs_1()) -> zipwith_l_cond_1(fibs_1[1](bot[1]()),x5,x3) zipwith_l_f_xs_ys[1](rec[fibs_0](),x11,x7) -> zipwith_l_cond(ConsL(0(),fibs_1()),x11) zipwith_l_f_xs_ys[1](fibs_1(),x5,x3) -> zipwith_l_cond(fibs_1[1](bot[2]()),x5) zipwith_l_f_xs_ys[1](zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) rec[zipwith_l_0][3](x20,x12) -> zipwith_l_f_xs_ys(x20,x12) rec[plus_0][2](0(),x34) -> x34 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) fibs_1[1](x15) -> ConsL(S(0()),rec[zipwith_l_0][3](rec[fibs_0](),fibs_1())) main(x28) -> take_l_cond(ConsL(0(),fibs_1()),x28) Proof: Matrix Interpretation Processor: dim=1 interpretation: [main](x0) = x0 + 2, [bot[2]] = 0, [rec[fibs_0]] = 0, [bot[1]] = 0, [zipwith_l_cond](x0, x1) = 4x0 + x1, [rec[zipwith_l_0][3]](x0, x1) = 4x0 + x1, [rec[plus_0][2]](x0, x1) = x0 + x1, [zipwith_l_cond_1](x0, x1, x2) = x0 + x1 + 4x2, [zipwith_l_f_xs_ys[1]](x0, x1, x2) = 4x0 + x1 + 4x2, [zipwith_l_f_xs_ys](x0, x1) = 4x0 + x1, [Cons](x0, x1) = x0 + x1, [fibs_1[1]](x0) = x0, [bot[0]] = 0, [S](x0) = x0, [fibs_1] = 0, [Nil] = 0, [take_l_cond](x0, x1) = x0 + x1 + 2, [0] = 0, [ConsL](x0, x1) = x0 + x1 orientation: take_l_cond(ConsL(x13,x17),0()) = x13 + x17 + 2 >= 0 = Nil() take_l_cond(ConsL(0(),fibs_1()),S(x1)) = x1 + 2 >= x1 + 2 = Cons(0(),take_l_cond(fibs_1[1](bot[0]()),x1)) take_l_cond(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) = x1 + x2 + 4x3 + x4 + 2 >= x1 + x2 + 4x3 + x4 + 2 = Cons(x4,take_l_cond(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1)) zipwith_l_cond_1(ConsL(x9,x7),x5,x3) = 4x3 + x5 + x7 + x9 >= 4x3 + x5 + x7 + x9 = ConsL(rec[plus_0][2](x5,x9),rec[zipwith_l_0][3](x3,x7)) zipwith_l_cond(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) = x1 + 4x2 + 4x3 + 4x4 >= x1 + 4x2 + 4x3 + x4 = zipwith_l_cond_1(zipwith_l_f_xs_ys[1](x2,x1,bot[1]()),x4,x3) zipwith_l_cond(ConsL(x5,x3),fibs_1()) = 4x3 + 4x5 >= 4x3 + x5 = zipwith_l_cond_1(fibs_1[1](bot[1]()),x5,x3) zipwith_l_f_xs_ys[1](rec[fibs_0](),x11,x7) = x11 + 4x7 >= x11 = zipwith_l_cond(ConsL(0(),fibs_1()),x11) zipwith_l_f_xs_ys[1](fibs_1(),x5,x3) = 4x3 + x5 >= x5 = zipwith_l_cond(fibs_1[1](bot[2]()),x5) zipwith_l_f_xs_ys[1](zipwith_l_f_xs_ys(x4,x3),x2,x1) = 4x1 + x2 + 4x3 + 16x4 >= x2 + 4x3 + 16x4 = zipwith_l_cond(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) rec[zipwith_l_0][3](x20,x12) = x12 + 4x20 >= x12 + 4x20 = zipwith_l_f_xs_ys(x20,x12) rec[plus_0][2](0(),x34) = x34 >= x34 = x34 rec[plus_0][2](S(x10),x6) = x10 + x6 >= x10 + x6 = S(rec[plus_0][2](x10,x6)) fibs_1[1](x15) = x15 >= 0 = ConsL(S(0()),rec[zipwith_l_0][3](rec[fibs_0](),fibs_1())) main(x28) = x28 + 2 >= x28 + 2 = take_l_cond(ConsL(0(),fibs_1()),x28) problem: take_l_cond(ConsL(0(),fibs_1()),S(x1)) -> Cons(0(),take_l_cond(fibs_1[1](bot[0]()),x1)) take_l_cond(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> Cons(x4,take_l_cond(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1)) zipwith_l_cond_1(ConsL(x9,x7),x5,x3) -> ConsL(rec[plus_0][2](x5,x9),rec[zipwith_l_0][3](x3,x7)) zipwith_l_cond(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_cond_1(zipwith_l_f_xs_ys[1](x2,x1,bot[1]()),x4,x3) zipwith_l_cond(ConsL(x5,x3),fibs_1()) -> zipwith_l_cond_1(fibs_1[1](bot[1]()),x5,x3) zipwith_l_f_xs_ys[1](rec[fibs_0](),x11,x7) -> zipwith_l_cond(ConsL(0(),fibs_1()),x11) zipwith_l_f_xs_ys[1](fibs_1(),x5,x3) -> zipwith_l_cond(fibs_1[1](bot[2]()),x5) zipwith_l_f_xs_ys[1](zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) rec[zipwith_l_0][3](x20,x12) -> zipwith_l_f_xs_ys(x20,x12) rec[plus_0][2](0(),x34) -> x34 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) fibs_1[1](x15) -> ConsL(S(0()),rec[zipwith_l_0][3](rec[fibs_0](),fibs_1())) main(x28) -> take_l_cond(ConsL(0(),fibs_1()),x28) Matrix Interpretation Processor: dim=1 interpretation: [main](x0) = 4x0 + 4, [bot[2]] = 0, [rec[fibs_0]] = 0, [bot[1]] = 0, [zipwith_l_cond](x0, x1) = 2x0 + x1, [rec[zipwith_l_0][3]](x0, x1) = 2x0 + 2x1, [rec[plus_0][2]](x0, x1) = x0 + x1, [zipwith_l_cond_1](x0, x1, x2) = 2x0 + x1 + 4x2, [zipwith_l_f_xs_ys[1]](x0, x1, x2) = x0 + x1 + 2x2, [zipwith_l_f_xs_ys](x0, x1) = 2x0 + 2x1, [Cons](x0, x1) = 2x0 + x1, [fibs_1[1]](x0) = x0, [bot[0]] = 0, [S](x0) = x0, [fibs_1] = 0, [take_l_cond](x0, x1) = 4x0 + x1 + 2, [0] = 0, [ConsL](x0, x1) = x0 + 2x1 orientation: take_l_cond(ConsL(0(),fibs_1()),S(x1)) = x1 + 2 >= x1 + 2 = Cons(0(),take_l_cond(fibs_1[1](bot[0]()),x1)) take_l_cond(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) = x1 + 16x2 + 16x3 + 4x4 + 2 >= x1 + 4x2 + 4x3 + 2x4 + 2 = Cons(x4,take_l_cond(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1)) zipwith_l_cond_1(ConsL(x9,x7),x5,x3) = 4x3 + x5 + 4x7 + 2x9 >= 4x3 + x5 + 4x7 + x9 = ConsL(rec[plus_0][2](x5,x9),rec[zipwith_l_0][3](x3,x7)) zipwith_l_cond(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) = 2x1 + 2x2 + 4x3 + 2x4 >= 2x1 + 2x2 + 4x3 + x4 = zipwith_l_cond_1(zipwith_l_f_xs_ys[1](x2,x1,bot[1]()),x4,x3) zipwith_l_cond(ConsL(x5,x3),fibs_1()) = 4x3 + 2x5 >= 4x3 + x5 = zipwith_l_cond_1(fibs_1[1](bot[1]()),x5,x3) zipwith_l_f_xs_ys[1](rec[fibs_0](),x11,x7) = x11 + 2x7 >= x11 = zipwith_l_cond(ConsL(0(),fibs_1()),x11) zipwith_l_f_xs_ys[1](fibs_1(),x5,x3) = 2x3 + x5 >= x5 = zipwith_l_cond(fibs_1[1](bot[2]()),x5) zipwith_l_f_xs_ys[1](zipwith_l_f_xs_ys(x4,x3),x2,x1) = 2x1 + x2 + 2x3 + 2x4 >= x2 + 2x3 + 2x4 = zipwith_l_cond(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) rec[zipwith_l_0][3](x20,x12) = 2x12 + 2x20 >= 2x12 + 2x20 = zipwith_l_f_xs_ys(x20,x12) rec[plus_0][2](0(),x34) = x34 >= x34 = x34 rec[plus_0][2](S(x10),x6) = x10 + x6 >= x10 + x6 = S(rec[plus_0][2](x10,x6)) fibs_1[1](x15) = x15 >= 0 = ConsL(S(0()),rec[zipwith_l_0][3](rec[fibs_0](),fibs_1())) main(x28) = 4x28 + 4 >= x28 + 2 = take_l_cond(ConsL(0(),fibs_1()),x28) problem: take_l_cond(ConsL(0(),fibs_1()),S(x1)) -> Cons(0(),take_l_cond(fibs_1[1](bot[0]()),x1)) take_l_cond(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> Cons(x4,take_l_cond(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1)) zipwith_l_cond_1(ConsL(x9,x7),x5,x3) -> ConsL(rec[plus_0][2](x5,x9),rec[zipwith_l_0][3](x3,x7)) zipwith_l_cond(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_cond_1(zipwith_l_f_xs_ys[1](x2,x1,bot[1]()),x4,x3) zipwith_l_cond(ConsL(x5,x3),fibs_1()) -> zipwith_l_cond_1(fibs_1[1](bot[1]()),x5,x3) zipwith_l_f_xs_ys[1](rec[fibs_0](),x11,x7) -> zipwith_l_cond(ConsL(0(),fibs_1()),x11) zipwith_l_f_xs_ys[1](fibs_1(),x5,x3) -> zipwith_l_cond(fibs_1[1](bot[2]()),x5) zipwith_l_f_xs_ys[1](zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) rec[zipwith_l_0][3](x20,x12) -> zipwith_l_f_xs_ys(x20,x12) rec[plus_0][2](0(),x34) -> x34 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) fibs_1[1](x15) -> ConsL(S(0()),rec[zipwith_l_0][3](rec[fibs_0](),fibs_1())) DP Processor: DPs: take_l_cond#(ConsL(0(),fibs_1()),S(x1)) -> fibs_1[1]#(bot[0]()) take_l_cond#(ConsL(0(),fibs_1()),S(x1)) -> take_l_cond#(fibs_1[1](bot[0]()),x1) take_l_cond#(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> zipwith_l_f_xs_ys[1]#(x3,x2,bot[0]()) take_l_cond#(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> take_l_cond#(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1) zipwith_l_cond_1#(ConsL(x9,x7),x5,x3) -> rec[zipwith_l_0][3]#(x3,x7) zipwith_l_cond_1#(ConsL(x9,x7),x5,x3) -> rec[plus_0][2]#(x5,x9) zipwith_l_cond#(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_f_xs_ys[1]#(x2,x1,bot[1]()) zipwith_l_cond#(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_cond_1#(zipwith_l_f_xs_ys[1](x2,x1,bot[1]()),x4,x3) zipwith_l_cond#(ConsL(x5,x3),fibs_1()) -> fibs_1[1]#(bot[1]()) zipwith_l_cond#(ConsL(x5,x3),fibs_1()) -> zipwith_l_cond_1#(fibs_1[1](bot[1]()),x5,x3) zipwith_l_f_xs_ys[1]#(rec[fibs_0](),x11,x7) -> zipwith_l_cond#(ConsL(0(),fibs_1()),x11) zipwith_l_f_xs_ys[1]#(fibs_1(),x5,x3) -> fibs_1[1]#(bot[2]()) zipwith_l_f_xs_ys[1]#(fibs_1(),x5,x3) -> zipwith_l_cond#(fibs_1[1](bot[2]()),x5) zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_f_xs_ys[1]#(x4,x3,bot[2]()) zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond#(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) rec[plus_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x10,x6) fibs_1[1]#(x15) -> rec[zipwith_l_0][3]#(rec[fibs_0](),fibs_1()) TRS: take_l_cond(ConsL(0(),fibs_1()),S(x1)) -> Cons(0(),take_l_cond(fibs_1[1](bot[0]()),x1)) take_l_cond(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> Cons(x4,take_l_cond(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1)) zipwith_l_cond_1(ConsL(x9,x7),x5,x3) -> ConsL(rec[plus_0][2](x5,x9),rec[zipwith_l_0][3](x3,x7)) zipwith_l_cond(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_cond_1(zipwith_l_f_xs_ys[1](x2,x1,bot[1]()),x4,x3) zipwith_l_cond(ConsL(x5,x3),fibs_1()) -> zipwith_l_cond_1(fibs_1[1](bot[1]()),x5,x3) zipwith_l_f_xs_ys[1](rec[fibs_0](),x11,x7) -> zipwith_l_cond(ConsL(0(),fibs_1()),x11) zipwith_l_f_xs_ys[1](fibs_1(),x5,x3) -> zipwith_l_cond(fibs_1[1](bot[2]()),x5) zipwith_l_f_xs_ys[1](zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) rec[zipwith_l_0][3](x20,x12) -> zipwith_l_f_xs_ys(x20,x12) rec[plus_0][2](0(),x34) -> x34 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) fibs_1[1](x15) -> ConsL(S(0()),rec[zipwith_l_0][3](rec[fibs_0](),fibs_1())) TDG Processor: DPs: take_l_cond#(ConsL(0(),fibs_1()),S(x1)) -> fibs_1[1]#(bot[0]()) take_l_cond#(ConsL(0(),fibs_1()),S(x1)) -> take_l_cond#(fibs_1[1](bot[0]()),x1) take_l_cond#(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> zipwith_l_f_xs_ys[1]#(x3,x2,bot[0]()) take_l_cond#(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> take_l_cond#(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1) zipwith_l_cond_1#(ConsL(x9,x7),x5,x3) -> rec[zipwith_l_0][3]#(x3,x7) zipwith_l_cond_1#(ConsL(x9,x7),x5,x3) -> rec[plus_0][2]#(x5,x9) zipwith_l_cond#(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_f_xs_ys[1]#(x2,x1,bot[1]()) zipwith_l_cond#(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_cond_1#(zipwith_l_f_xs_ys[1](x2,x1,bot[1]()),x4,x3) zipwith_l_cond#(ConsL(x5,x3),fibs_1()) -> fibs_1[1]#(bot[1]()) zipwith_l_cond#(ConsL(x5,x3),fibs_1()) -> zipwith_l_cond_1#(fibs_1[1](bot[1]()),x5,x3) zipwith_l_f_xs_ys[1]#(rec[fibs_0](),x11,x7) -> zipwith_l_cond#(ConsL(0(),fibs_1()),x11) zipwith_l_f_xs_ys[1]#(fibs_1(),x5,x3) -> fibs_1[1]#(bot[2]()) zipwith_l_f_xs_ys[1]#(fibs_1(),x5,x3) -> zipwith_l_cond#(fibs_1[1](bot[2]()),x5) zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_f_xs_ys[1]#(x4,x3,bot[2]()) zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond#(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) rec[plus_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x10,x6) fibs_1[1]#(x15) -> rec[zipwith_l_0][3]#(rec[fibs_0](),fibs_1()) TRS: take_l_cond(ConsL(0(),fibs_1()),S(x1)) -> Cons(0(),take_l_cond(fibs_1[1](bot[0]()),x1)) take_l_cond(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> Cons(x4,take_l_cond(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1)) zipwith_l_cond_1(ConsL(x9,x7),x5,x3) -> ConsL(rec[plus_0][2](x5,x9),rec[zipwith_l_0][3](x3,x7)) zipwith_l_cond(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_cond_1(zipwith_l_f_xs_ys[1](x2,x1,bot[1]()),x4,x3) zipwith_l_cond(ConsL(x5,x3),fibs_1()) -> zipwith_l_cond_1(fibs_1[1](bot[1]()),x5,x3) zipwith_l_f_xs_ys[1](rec[fibs_0](),x11,x7) -> zipwith_l_cond(ConsL(0(),fibs_1()),x11) zipwith_l_f_xs_ys[1](fibs_1(),x5,x3) -> zipwith_l_cond(fibs_1[1](bot[2]()),x5) zipwith_l_f_xs_ys[1](zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) rec[zipwith_l_0][3](x20,x12) -> zipwith_l_f_xs_ys(x20,x12) rec[plus_0][2](0(),x34) -> x34 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) fibs_1[1](x15) -> ConsL(S(0()),rec[zipwith_l_0][3](rec[fibs_0](),fibs_1())) graph: zipwith_l_cond#(ConsL(x5,x3),fibs_1()) -> zipwith_l_cond_1#(fibs_1[1](bot[1]()),x5,x3) -> zipwith_l_cond_1#(ConsL(x9,x7),x5,x3) -> rec[plus_0][2]#(x5,x9) zipwith_l_cond#(ConsL(x5,x3),fibs_1()) -> zipwith_l_cond_1#(fibs_1[1](bot[1]()),x5,x3) -> zipwith_l_cond_1#(ConsL(x9,x7),x5,x3) -> rec[zipwith_l_0][3]#(x3,x7) zipwith_l_cond#(ConsL(x5,x3),fibs_1()) -> fibs_1[1]#(bot[1]()) -> fibs_1[1]#(x15) -> rec[zipwith_l_0][3]#(rec[fibs_0](),fibs_1()) zipwith_l_cond#(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_cond_1#(zipwith_l_f_xs_ys[1](x2,x1,bot[1]()),x4,x3) -> zipwith_l_cond_1#(ConsL(x9,x7),x5,x3) -> rec[plus_0][2]#(x5,x9) zipwith_l_cond#(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_cond_1#(zipwith_l_f_xs_ys[1](x2,x1,bot[1]()),x4,x3) -> zipwith_l_cond_1#(ConsL(x9,x7),x5,x3) -> rec[zipwith_l_0][3]#(x3,x7) zipwith_l_cond#(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_f_xs_ys[1]#(x2,x1,bot[1]()) -> zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond#(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) zipwith_l_cond#(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_f_xs_ys[1]#(x2,x1,bot[1]()) -> zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_f_xs_ys[1]#(x4,x3,bot[2]()) zipwith_l_cond#(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_f_xs_ys[1]#(x2,x1,bot[1]()) -> zipwith_l_f_xs_ys[1]#(fibs_1(),x5,x3) -> zipwith_l_cond#(fibs_1[1](bot[2]()),x5) zipwith_l_cond#(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_f_xs_ys[1]#(x2,x1,bot[1]()) -> zipwith_l_f_xs_ys[1]#(fibs_1(),x5,x3) -> fibs_1[1]#(bot[2]()) zipwith_l_cond#(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_f_xs_ys[1]#(x2,x1,bot[1]()) -> zipwith_l_f_xs_ys[1]#(rec[fibs_0](),x11,x7) -> zipwith_l_cond#(ConsL(0(),fibs_1()),x11) rec[plus_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x10,x6) -> rec[plus_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x10,x6) zipwith_l_cond_1#(ConsL(x9,x7),x5,x3) -> rec[plus_0][2]#(x5,x9) -> rec[plus_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x10,x6) zipwith_l_f_xs_ys[1]#(rec[fibs_0](),x11,x7) -> zipwith_l_cond#(ConsL(0(),fibs_1()),x11) -> zipwith_l_cond#(ConsL(x5,x3),fibs_1()) -> zipwith_l_cond_1#(fibs_1[1](bot[1]()),x5,x3) zipwith_l_f_xs_ys[1]#(rec[fibs_0](),x11,x7) -> zipwith_l_cond#(ConsL(0(),fibs_1()),x11) -> zipwith_l_cond#(ConsL(x5,x3),fibs_1()) -> fibs_1[1]#(bot[1]()) zipwith_l_f_xs_ys[1]#(rec[fibs_0](),x11,x7) -> zipwith_l_cond#(ConsL(0(),fibs_1()),x11) -> zipwith_l_cond#(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_cond_1#(zipwith_l_f_xs_ys[1](x2,x1,bot[1]()),x4,x3) zipwith_l_f_xs_ys[1]#(rec[fibs_0](),x11,x7) -> zipwith_l_cond#(ConsL(0(),fibs_1()),x11) -> zipwith_l_cond#(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_f_xs_ys[1]#(x2,x1,bot[1]()) zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond#(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) -> zipwith_l_cond#(ConsL(x5,x3),fibs_1()) -> zipwith_l_cond_1#(fibs_1[1](bot[1]()),x5,x3) zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond#(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) -> zipwith_l_cond#(ConsL(x5,x3),fibs_1()) -> fibs_1[1]#(bot[1]()) zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond#(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) -> zipwith_l_cond#(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_cond_1#(zipwith_l_f_xs_ys[1](x2,x1,bot[1]()),x4,x3) zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond#(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) -> zipwith_l_cond#(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_f_xs_ys[1]#(x2,x1,bot[1]()) zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_f_xs_ys[1]#(x4,x3,bot[2]()) -> zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond#(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_f_xs_ys[1]#(x4,x3,bot[2]()) -> zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_f_xs_ys[1]#(x4,x3,bot[2]()) zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_f_xs_ys[1]#(x4,x3,bot[2]()) -> zipwith_l_f_xs_ys[1]#(fibs_1(),x5,x3) -> zipwith_l_cond#(fibs_1[1](bot[2]()),x5) zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_f_xs_ys[1]#(x4,x3,bot[2]()) -> zipwith_l_f_xs_ys[1]#(fibs_1(),x5,x3) -> fibs_1[1]#(bot[2]()) zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_f_xs_ys[1]#(x4,x3,bot[2]()) -> zipwith_l_f_xs_ys[1]#(rec[fibs_0](),x11,x7) -> zipwith_l_cond#(ConsL(0(),fibs_1()),x11) zipwith_l_f_xs_ys[1]#(fibs_1(),x5,x3) -> zipwith_l_cond#(fibs_1[1](bot[2]()),x5) -> zipwith_l_cond#(ConsL(x5,x3),fibs_1()) -> zipwith_l_cond_1#(fibs_1[1](bot[1]()),x5,x3) zipwith_l_f_xs_ys[1]#(fibs_1(),x5,x3) -> zipwith_l_cond#(fibs_1[1](bot[2]()),x5) -> zipwith_l_cond#(ConsL(x5,x3),fibs_1()) -> fibs_1[1]#(bot[1]()) zipwith_l_f_xs_ys[1]#(fibs_1(),x5,x3) -> zipwith_l_cond#(fibs_1[1](bot[2]()),x5) -> zipwith_l_cond#(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_cond_1#(zipwith_l_f_xs_ys[1](x2,x1,bot[1]()),x4,x3) zipwith_l_f_xs_ys[1]#(fibs_1(),x5,x3) -> zipwith_l_cond#(fibs_1[1](bot[2]()),x5) -> zipwith_l_cond#(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_f_xs_ys[1]#(x2,x1,bot[1]()) zipwith_l_f_xs_ys[1]#(fibs_1(),x5,x3) -> fibs_1[1]#(bot[2]()) -> fibs_1[1]#(x15) -> rec[zipwith_l_0][3]#(rec[fibs_0](),fibs_1()) take_l_cond#(ConsL(0(),fibs_1()),S(x1)) -> fibs_1[1]#(bot[0]()) -> fibs_1[1]#(x15) -> rec[zipwith_l_0][3]#(rec[fibs_0](),fibs_1()) take_l_cond#(ConsL(0(),fibs_1()),S(x1)) -> take_l_cond#(fibs_1[1](bot[0]()),x1) -> take_l_cond#(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> take_l_cond#(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1) take_l_cond#(ConsL(0(),fibs_1()),S(x1)) -> take_l_cond#(fibs_1[1](bot[0]()),x1) -> take_l_cond#(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> zipwith_l_f_xs_ys[1]#(x3,x2,bot[0]()) take_l_cond#(ConsL(0(),fibs_1()),S(x1)) -> take_l_cond#(fibs_1[1](bot[0]()),x1) -> take_l_cond#(ConsL(0(),fibs_1()),S(x1)) -> take_l_cond#(fibs_1[1](bot[0]()),x1) take_l_cond#(ConsL(0(),fibs_1()),S(x1)) -> take_l_cond#(fibs_1[1](bot[0]()),x1) -> take_l_cond#(ConsL(0(),fibs_1()),S(x1)) -> fibs_1[1]#(bot[0]()) take_l_cond#(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> zipwith_l_f_xs_ys[1]#(x3,x2,bot[0]()) -> zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond#(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) take_l_cond#(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> zipwith_l_f_xs_ys[1]#(x3,x2,bot[0]()) -> zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_f_xs_ys[1]#(x4,x3,bot[2]()) take_l_cond#(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> zipwith_l_f_xs_ys[1]#(x3,x2,bot[0]()) -> zipwith_l_f_xs_ys[1]#(fibs_1(),x5,x3) -> zipwith_l_cond#(fibs_1[1](bot[2]()),x5) take_l_cond#(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> zipwith_l_f_xs_ys[1]#(x3,x2,bot[0]()) -> zipwith_l_f_xs_ys[1]#(fibs_1(),x5,x3) -> fibs_1[1]#(bot[2]()) take_l_cond#(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> zipwith_l_f_xs_ys[1]#(x3,x2,bot[0]()) -> zipwith_l_f_xs_ys[1]#(rec[fibs_0](),x11,x7) -> zipwith_l_cond#(ConsL(0(),fibs_1()),x11) take_l_cond#(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> take_l_cond#(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1) -> take_l_cond#(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> take_l_cond#(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1) take_l_cond#(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> take_l_cond#(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1) -> take_l_cond#(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> zipwith_l_f_xs_ys[1]#(x3,x2,bot[0]()) take_l_cond#(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> take_l_cond#(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1) -> take_l_cond#(ConsL(0(),fibs_1()),S(x1)) -> take_l_cond#(fibs_1[1](bot[0]()),x1) take_l_cond#(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> take_l_cond#(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1) -> take_l_cond#(ConsL(0(),fibs_1()),S(x1)) -> fibs_1[1]#(bot[0]()) SCC Processor: #sccs: 3 #rules: 8 #arcs: 44/289 DPs: take_l_cond#(ConsL(0(),fibs_1()),S(x1)) -> take_l_cond#(fibs_1[1](bot[0]()),x1) take_l_cond#(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> take_l_cond#(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1) TRS: take_l_cond(ConsL(0(),fibs_1()),S(x1)) -> Cons(0(),take_l_cond(fibs_1[1](bot[0]()),x1)) take_l_cond(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> Cons(x4,take_l_cond(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1)) zipwith_l_cond_1(ConsL(x9,x7),x5,x3) -> ConsL(rec[plus_0][2](x5,x9),rec[zipwith_l_0][3](x3,x7)) zipwith_l_cond(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_cond_1(zipwith_l_f_xs_ys[1](x2,x1,bot[1]()),x4,x3) zipwith_l_cond(ConsL(x5,x3),fibs_1()) -> zipwith_l_cond_1(fibs_1[1](bot[1]()),x5,x3) zipwith_l_f_xs_ys[1](rec[fibs_0](),x11,x7) -> zipwith_l_cond(ConsL(0(),fibs_1()),x11) zipwith_l_f_xs_ys[1](fibs_1(),x5,x3) -> zipwith_l_cond(fibs_1[1](bot[2]()),x5) zipwith_l_f_xs_ys[1](zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) rec[zipwith_l_0][3](x20,x12) -> zipwith_l_f_xs_ys(x20,x12) rec[plus_0][2](0(),x34) -> x34 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) fibs_1[1](x15) -> ConsL(S(0()),rec[zipwith_l_0][3](rec[fibs_0](),fibs_1())) Subterm Criterion Processor: simple projection: pi(take_l_cond#) = 1 problem: DPs: TRS: take_l_cond(ConsL(0(),fibs_1()),S(x1)) -> Cons(0(),take_l_cond(fibs_1[1](bot[0]()),x1)) take_l_cond(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> Cons(x4,take_l_cond(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1)) zipwith_l_cond_1(ConsL(x9,x7),x5,x3) -> ConsL(rec[plus_0][2](x5,x9),rec[zipwith_l_0][3](x3,x7)) zipwith_l_cond(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_cond_1(zipwith_l_f_xs_ys[1](x2,x1,bot[1]()),x4,x3) zipwith_l_cond(ConsL(x5,x3),fibs_1()) -> zipwith_l_cond_1(fibs_1[1](bot[1]()),x5,x3) zipwith_l_f_xs_ys[1](rec[fibs_0](),x11,x7) -> zipwith_l_cond(ConsL(0(),fibs_1()),x11) zipwith_l_f_xs_ys[1](fibs_1(),x5,x3) -> zipwith_l_cond(fibs_1[1](bot[2]()),x5) zipwith_l_f_xs_ys[1](zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) rec[zipwith_l_0][3](x20,x12) -> zipwith_l_f_xs_ys(x20,x12) rec[plus_0][2](0(),x34) -> x34 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) fibs_1[1](x15) -> ConsL(S(0()),rec[zipwith_l_0][3](rec[fibs_0](),fibs_1())) Qed DPs: zipwith_l_cond#(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_f_xs_ys[1]#(x2,x1,bot[1]()) zipwith_l_f_xs_ys[1]#(rec[fibs_0](),x11,x7) -> zipwith_l_cond#(ConsL(0(),fibs_1()),x11) zipwith_l_f_xs_ys[1]#(fibs_1(),x5,x3) -> zipwith_l_cond#(fibs_1[1](bot[2]()),x5) zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_f_xs_ys[1]#(x4,x3,bot[2]()) zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond#(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) TRS: take_l_cond(ConsL(0(),fibs_1()),S(x1)) -> Cons(0(),take_l_cond(fibs_1[1](bot[0]()),x1)) take_l_cond(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> Cons(x4,take_l_cond(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1)) zipwith_l_cond_1(ConsL(x9,x7),x5,x3) -> ConsL(rec[plus_0][2](x5,x9),rec[zipwith_l_0][3](x3,x7)) zipwith_l_cond(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_cond_1(zipwith_l_f_xs_ys[1](x2,x1,bot[1]()),x4,x3) zipwith_l_cond(ConsL(x5,x3),fibs_1()) -> zipwith_l_cond_1(fibs_1[1](bot[1]()),x5,x3) zipwith_l_f_xs_ys[1](rec[fibs_0](),x11,x7) -> zipwith_l_cond(ConsL(0(),fibs_1()),x11) zipwith_l_f_xs_ys[1](fibs_1(),x5,x3) -> zipwith_l_cond(fibs_1[1](bot[2]()),x5) zipwith_l_f_xs_ys[1](zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) rec[zipwith_l_0][3](x20,x12) -> zipwith_l_f_xs_ys(x20,x12) rec[plus_0][2](0(),x34) -> x34 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) fibs_1[1](x15) -> ConsL(S(0()),rec[zipwith_l_0][3](rec[fibs_0](),fibs_1())) Size-Change Termination Processor: DPs: TRS: take_l_cond(ConsL(0(),fibs_1()),S(x1)) -> Cons(0(),take_l_cond(fibs_1[1](bot[0]()),x1)) take_l_cond(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> Cons(x4,take_l_cond(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1)) zipwith_l_cond_1(ConsL(x9,x7),x5,x3) -> ConsL(rec[plus_0][2](x5,x9),rec[zipwith_l_0][3](x3,x7)) zipwith_l_cond(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_cond_1(zipwith_l_f_xs_ys[1](x2,x1,bot[1]()),x4,x3) zipwith_l_cond(ConsL(x5,x3),fibs_1()) -> zipwith_l_cond_1(fibs_1[1](bot[1]()),x5,x3) zipwith_l_f_xs_ys[1](rec[fibs_0](),x11,x7) -> zipwith_l_cond(ConsL(0(),fibs_1()),x11) zipwith_l_f_xs_ys[1](fibs_1(),x5,x3) -> zipwith_l_cond(fibs_1[1](bot[2]()),x5) zipwith_l_f_xs_ys[1](zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) rec[zipwith_l_0][3](x20,x12) -> zipwith_l_f_xs_ys(x20,x12) rec[plus_0][2](0(),x34) -> x34 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) fibs_1[1](x15) -> ConsL(S(0()),rec[zipwith_l_0][3](rec[fibs_0](),fibs_1())) The DP: zipwith_l_cond#(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_f_xs_ys[1]#(x2,x1,bot[1]()) has the edges: 1 > 1 1 > 0 The DP: zipwith_l_f_xs_ys[1]#(rec[fibs_0](),x11,x7) -> zipwith_l_cond#(ConsL(0(),fibs_1()),x11) has the edges: 1 >= 1 The DP: zipwith_l_f_xs_ys[1]#(fibs_1(),x5,x3) -> zipwith_l_cond#(fibs_1[1](bot[2]()),x5) has the edges: 1 >= 1 The DP: zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_f_xs_ys[1]#(x4,x3,bot[2]()) has the edges: 0 > 1 0 > 0 The DP: zipwith_l_f_xs_ys[1]#(zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond#(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) has the edges: 1 >= 1 Qed DPs: rec[plus_0][2]#(S(x10),x6) -> rec[plus_0][2]#(x10,x6) TRS: take_l_cond(ConsL(0(),fibs_1()),S(x1)) -> Cons(0(),take_l_cond(fibs_1[1](bot[0]()),x1)) take_l_cond(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> Cons(x4,take_l_cond(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1)) zipwith_l_cond_1(ConsL(x9,x7),x5,x3) -> ConsL(rec[plus_0][2](x5,x9),rec[zipwith_l_0][3](x3,x7)) zipwith_l_cond(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_cond_1(zipwith_l_f_xs_ys[1](x2,x1,bot[1]()),x4,x3) zipwith_l_cond(ConsL(x5,x3),fibs_1()) -> zipwith_l_cond_1(fibs_1[1](bot[1]()),x5,x3) zipwith_l_f_xs_ys[1](rec[fibs_0](),x11,x7) -> zipwith_l_cond(ConsL(0(),fibs_1()),x11) zipwith_l_f_xs_ys[1](fibs_1(),x5,x3) -> zipwith_l_cond(fibs_1[1](bot[2]()),x5) zipwith_l_f_xs_ys[1](zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) rec[zipwith_l_0][3](x20,x12) -> zipwith_l_f_xs_ys(x20,x12) rec[plus_0][2](0(),x34) -> x34 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) fibs_1[1](x15) -> ConsL(S(0()),rec[zipwith_l_0][3](rec[fibs_0](),fibs_1())) Subterm Criterion Processor: simple projection: pi(rec[plus_0][2]#) = 0 problem: DPs: TRS: take_l_cond(ConsL(0(),fibs_1()),S(x1)) -> Cons(0(),take_l_cond(fibs_1[1](bot[0]()),x1)) take_l_cond(ConsL(x4,zipwith_l_f_xs_ys(x3,x2)),S(x1)) -> Cons(x4,take_l_cond(zipwith_l_f_xs_ys[1](x3,x2,bot[0]()),x1)) zipwith_l_cond_1(ConsL(x9,x7),x5,x3) -> ConsL(rec[plus_0][2](x5,x9),rec[zipwith_l_0][3](x3,x7)) zipwith_l_cond(ConsL(x4,x3),zipwith_l_f_xs_ys(x2,x1)) -> zipwith_l_cond_1(zipwith_l_f_xs_ys[1](x2,x1,bot[1]()),x4,x3) zipwith_l_cond(ConsL(x5,x3),fibs_1()) -> zipwith_l_cond_1(fibs_1[1](bot[1]()),x5,x3) zipwith_l_f_xs_ys[1](rec[fibs_0](),x11,x7) -> zipwith_l_cond(ConsL(0(),fibs_1()),x11) zipwith_l_f_xs_ys[1](fibs_1(),x5,x3) -> zipwith_l_cond(fibs_1[1](bot[2]()),x5) zipwith_l_f_xs_ys[1](zipwith_l_f_xs_ys(x4,x3),x2,x1) -> zipwith_l_cond(zipwith_l_f_xs_ys[1](x4,x3,bot[2]()),x2) rec[zipwith_l_0][3](x20,x12) -> zipwith_l_f_xs_ys(x20,x12) rec[plus_0][2](0(),x34) -> x34 rec[plus_0][2](S(x10),x6) -> S(rec[plus_0][2](x10,x6)) fibs_1[1](x15) -> ConsL(S(0()),rec[zipwith_l_0][3](rec[fibs_0](),fibs_1())) Qed