MAYBE * Step 1: Desugar MAYBE + Considered Problem: type Unit = Unit;; type 'a llist = NilL | ConsL of 'a * (Unit -> 'a llist) ;; type nat = 0 | S of nat ;; type 'a list = Nil | Cons of 'a * 'a list ;; let rec zipwith_l f xs ys = lazy (match force xs with | NilL -> NilL | ConsL(x,xs') -> match force ys with | NilL -> NilL | ConsL(y,ys') -> ConsL(f x y, zipwith_l f xs' ys')) ;; let rec plus x y = match x with | 0 -> y | S(x') -> S(plus x' y) ;; let tail_l xs = match force xs with | NilL -> error | ConsL(x,xs') -> xs' ;; let rec nth_l n xs = match force xs with | NilL -> error | ConsL(x,xs') -> match n with | 0 -> x | S(n') -> nth_l n' xs' ;; let fix f = let rec x = lazy (force (f x)) in x ;; let rec take_l n xs = match force xs with | NilL -> Nil | ConsL(x,xs') -> match n with | 0 -> Nil | S(n') -> Cons(x,take_l n' xs') ;; let rec fibs = lazy ConsL(0, lazy ConsL(S(0), zipwith_l plus fibs (tail_l fibs))) ;; let fib n = take_l n fibs ;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization MAYBE + Considered Problem: λn : nat. (λzipwith_l : (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist. (λplus : nat -> nat -> nat. (λtail_l : (Unit -> nat llist) -> Unit -> nat llist. (λtake_l : nat -> (Unit -> nat llist) -> nat list. (λfibs : Unit -> nat llist. (λfib : nat -> nat list. fib n) (λn : nat. take_l n fibs)) (μfibs : Unit -> nat llist. λ0 : Unit. ConsL(0,λ0 : Unit. ConsL(S(0),zipwith_l plus fibs (tail_l fibs))))) (μtake_l : nat -> (Unit -> nat llist) -> nat list. λn : nat. λxs : Unit -> nat llist. case xs ⟘  of | NilL -> Nil | ConsL -> λx : nat. λxs' : Unit -> nat llist. case n of | 0 -> Nil | S -> λn' : nat. Cons(x,take_l n' xs'))) (λxs : Unit -> nat llist. case xs ⟘  of | NilL -> ⟘  | ConsL -> λx : nat. λxs' : Unit -> nat llist. xs')) (μplus : nat -> nat -> nat. λx : nat. λy : nat. case x of | 0 -> y | S -> λx' : nat. S(plus x' y))) (μzipwith_l : (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist. λf : nat -> nat -> nat. λxs : Unit -> nat llist. λys : Unit -> nat llist. λ0 : Unit. case xs ⟘  of | NilL -> NilL | ConsL -> λx : nat. λxs' : Unit -> nat llist. case ys ⟘  of | NilL -> NilL | ConsL -> λy : nat. λys' : Unit -> nat llist. ConsL(f x y,zipwith_l f xs' ys')) : nat -> nat list where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a llist) -> 'a llist Nil :: 'a list NilL :: 'a llist S :: nat -> nat Unit :: Unit + Applied Processor: Defunctionalization + Details: none * Step 3: Inline MAYBE + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: fib(x4, x5) x6 -> x4 x6 x5 3: main_5(x0, x4) x5 -> main_6(x0) fib(x4, x5) 4: fibs_2(x1, x2, x3) x6 -> ConsL(S(0()), x1 x2 fibs(x1, x2, x3) (x3 fibs(x1, x2, x3))) 5: fibs_1(x1, x2, x3) x5 -> ConsL(0(), fibs_2(x1, x2, x3)) 6: fibs(x1, x2, x3) x4 -> fibs_1(x1, x2, x3) x4 7: main_4(x0, x1, x2, x3) x4 -> main_5(x0, x4) fibs(x1, x2, x3) 8: cond_take_l_n_xs_1(0(), x6, x7) -> Nil() 9: cond_take_l_n_xs_1(S(x8), x6, x7) -> Cons(x6, take_l() x8 x7) 10: cond_take_l_n_xs(NilL(), x4) -> Nil() 11: cond_take_l_n_xs(ConsL(x6, x7), x4) -> cond_take_l_n_xs_1(x4, x6, x7) 12: take_l_n(x4) x5 -> cond_take_l_n_xs(x5 bot[0](), x4) 13: take_l_1() x4 -> take_l_n(x4) 14: take_l() x0 -> take_l_1() x0 15: main_3(x0, x1, x2) x3 -> main_4(x0, x1, x2, x3) take_l() 16: cond_tail_l_xs(NilL()) -> bot[1]() 17: cond_tail_l_xs(ConsL(x4, x5)) -> x5 18: tail_l() x3 -> cond_tail_l_xs(x3 bot[2]()) 19: main_2(x0, x1) x2 -> main_3(x0, x1, x2) tail_l() 20: cond_plus_x_y(0(), x3) -> x3 21: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 22: plus_x(x2) x3 -> cond_plus_x_y(x2, x3) 23: plus_1() x2 -> plus_x(x2) 24: plus() x0 -> plus_1() x0 25: main_1(x0) x1 -> main_2(x0, x1) plus() 26: cond_zipwith_l_f_xs_ys_1(NilL(), x1, x5, x6) -> NilL() 27: cond_zipwith_l_f_xs_ys_1(ConsL(x7, x8), x1, x5, x6) -> ConsL(x1 x5 x7, zipwith_l() x1 x6 x8) 28: cond_zipwith_l_f_xs_ys(NilL(), x1, x3) -> NilL() 29: cond_zipwith_l_f_xs_ys(ConsL(x5, x6), x1, x3) -> cond_zipwith_l_f_xs_ys_1(x3 bot[3](), x1, x5, x6) 30: zipwith_l_f_xs_ys(x1, x2, x3) x4 -> cond_zipwith_l_f_xs_ys(x2 bot[4](), x1, x3) 31: zipwith_l_f_xs(x1, x2) x3 -> zipwith_l_f_xs_ys(x1, x2, x3) 32: zipwith_l_f(x1) x2 -> zipwith_l_f_xs(x1, x2) 33: zipwith_l_1() x1 -> zipwith_l_f(x1) 34: zipwith_l() x0 -> zipwith_l_1() x0 35: main(x0) -> main_1(x0) zipwith_l() where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a llist) -> 'a llist Nil :: 'a list NilL :: 'a llist S :: nat -> nat zipwith_l_f :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fib :: (nat -> (Unit -> nat llist) -> nat list) -> (Unit -> nat llist) -> nat -> nat list take_l_n :: nat -> (Unit -> nat llist) -> nat list tail_l :: (Unit -> nat llist) -> Unit -> nat llist plus_x :: nat -> nat -> nat zipwith_l_f_xs :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fibs_1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main_1 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> nat list plus_1 :: nat -> nat -> nat take_l_1 :: nat -> (Unit -> nat llist) -> nat list zipwith_l_1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fibs_2 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main_2 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> nat list main_3 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> nat list main_4 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> (nat -> (Unit -> nat llist) -> nat list) -> nat list main_5 :: nat -> (nat -> (Unit -> nat llist) -> nat list) -> (Unit -> nat llist) -> nat list main_6 :: nat -> (nat -> nat list) -> nat list bot[0] :: Unit bot[1] :: Unit -> nat llist bot[2] :: Unit bot[3] :: Unit bot[4] :: Unit cond_take_l_n_xs :: nat llist -> nat -> nat list cond_tail_l_xs :: nat llist -> Unit -> nat llist cond_plus_x_y :: nat -> nat -> nat cond_zipwith_l_f_xs_ys :: nat llist -> (nat -> nat -> nat) -> (Unit -> nat llist) -> nat llist cond_take_l_n_xs_1 :: nat -> nat -> (Unit -> nat llist) -> nat list cond_zipwith_l_f_xs_ys_1 :: nat llist -> (nat -> nat -> nat) -> nat -> (Unit -> nat llist) -> nat llist fibs :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist plus :: nat -> nat -> nat take_l :: nat -> (Unit -> nat llist) -> nat list zipwith_l :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist main :: nat -> nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline MAYBE + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: fib(x4, x5) x6 -> x4 x6 x5 3: main_5(x0, x9) x11 -> fib(x9, x11) x0 4: fibs_2(x1, x2, x3) x6 -> ConsL(S(0()), x1 x2 fibs(x1, x2, x3) (x3 fibs(x1, x2, x3))) 5: fibs_1(x1, x2, x3) x5 -> ConsL(0(), fibs_2(x1, x2, x3)) 6: fibs(x2, x4, x6) x10 -> ConsL(0(), fibs_2(x2, x4, x6)) 7: main_4(x0, x3, x5, x7) x8 -> main_6(x0) fib(x8, fibs(x3, x5, x7)) 8: cond_take_l_n_xs_1(0(), x6, x7) -> Nil() 9: cond_take_l_n_xs_1(S(x8), x6, x7) -> Cons(x6, take_l() x8 x7) 10: cond_take_l_n_xs(NilL(), x4) -> Nil() 11: cond_take_l_n_xs(ConsL(x6, x7), x4) -> cond_take_l_n_xs_1(x4, x6, x7) 12: take_l_n(x4) x5 -> cond_take_l_n_xs(x5 bot[0](), x4) 13: take_l_1() x4 -> take_l_n(x4) 14: take_l() x8 -> take_l_n(x8) 15: main_3(x0, x2, x4) x6 -> main_5(x0, take_l()) fibs(x2, x4, x6) 16: cond_tail_l_xs(NilL()) -> bot[1]() 17: cond_tail_l_xs(ConsL(x4, x5)) -> x5 18: tail_l() x3 -> cond_tail_l_xs(x3 bot[2]()) 19: main_2(x0, x2) x4 -> main_4(x0, x2, x4, tail_l()) take_l() 20: cond_plus_x_y(0(), x3) -> x3 21: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 22: plus_x(x2) x3 -> cond_plus_x_y(x2, x3) 23: plus_1() x2 -> plus_x(x2) 24: plus() x4 -> plus_x(x4) 25: main_1(x0) x2 -> main_3(x0, x2, plus()) tail_l() 26: cond_zipwith_l_f_xs_ys_1(NilL(), x1, x5, x6) -> NilL() 27: cond_zipwith_l_f_xs_ys_1(ConsL(x7, x8), x1, x5, x6) -> ConsL(x1 x5 x7, zipwith_l() x1 x6 x8) 28: cond_zipwith_l_f_xs_ys(NilL(), x1, x3) -> NilL() 29: cond_zipwith_l_f_xs_ys(ConsL(x5, x6), x1, x3) -> cond_zipwith_l_f_xs_ys_1(x3 bot[3](), x1, x5, x6) 30: zipwith_l_f_xs_ys(x1, x2, x3) x4 -> cond_zipwith_l_f_xs_ys(x2 bot[4](), x1, x3) 31: zipwith_l_f_xs(x1, x2) x3 -> zipwith_l_f_xs_ys(x1, x2, x3) 32: zipwith_l_f(x1) x2 -> zipwith_l_f_xs(x1, x2) 33: zipwith_l_1() x1 -> zipwith_l_f(x1) 34: zipwith_l() x2 -> zipwith_l_f(x2) 35: main(x0) -> main_2(x0, zipwith_l()) plus() where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a llist) -> 'a llist Nil :: 'a list NilL :: 'a llist S :: nat -> nat zipwith_l_f :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fib :: (nat -> (Unit -> nat llist) -> nat list) -> (Unit -> nat llist) -> nat -> nat list take_l_n :: nat -> (Unit -> nat llist) -> nat list tail_l :: (Unit -> nat llist) -> Unit -> nat llist plus_x :: nat -> nat -> nat zipwith_l_f_xs :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fibs_1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main_1 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> nat list plus_1 :: nat -> nat -> nat take_l_1 :: nat -> (Unit -> nat llist) -> nat list zipwith_l_1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fibs_2 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main_2 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> nat list main_3 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> nat list main_4 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> (nat -> (Unit -> nat llist) -> nat list) -> nat list main_5 :: nat -> (nat -> (Unit -> nat llist) -> nat list) -> (Unit -> nat llist) -> nat list main_6 :: nat -> (nat -> nat list) -> nat list bot[0] :: Unit bot[1] :: Unit -> nat llist bot[2] :: Unit bot[3] :: Unit bot[4] :: Unit cond_take_l_n_xs :: nat llist -> nat -> nat list cond_tail_l_xs :: nat llist -> Unit -> nat llist cond_plus_x_y :: nat -> nat -> nat cond_zipwith_l_f_xs_ys :: nat llist -> (nat -> nat -> nat) -> (Unit -> nat llist) -> nat llist cond_take_l_n_xs_1 :: nat -> nat -> (Unit -> nat llist) -> nat list cond_zipwith_l_f_xs_ys_1 :: nat llist -> (nat -> nat -> nat) -> nat -> (Unit -> nat llist) -> nat llist fibs :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist plus :: nat -> nat -> nat take_l :: nat -> (Unit -> nat llist) -> nat list zipwith_l :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist main :: nat -> nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 5: Inline MAYBE + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: fib(x4, x5) x6 -> x4 x6 x5 3: main_5(x12, x8) x10 -> x8 x12 x10 4: fibs_2(x1, x2, x3) x6 -> ConsL(S(0()), x1 x2 fibs(x1, x2, x3) (x3 fibs(x1, x2, x3))) 5: fibs_1(x1, x2, x3) x5 -> ConsL(0(), fibs_2(x1, x2, x3)) 6: fibs(x2, x4, x6) x10 -> ConsL(0(), fibs_2(x2, x4, x6)) 7: main_4(x0, x7, x11, x15) x17 -> fib(x17, fibs(x7, x11, x15)) x0 8: cond_take_l_n_xs_1(0(), x6, x7) -> Nil() 9: cond_take_l_n_xs_1(S(x8), x6, x7) -> Cons(x6, take_l() x8 x7) 10: cond_take_l_n_xs(NilL(), x4) -> Nil() 11: cond_take_l_n_xs(ConsL(x6, x7), x4) -> cond_take_l_n_xs_1(x4, x6, x7) 12: take_l_n(x4) x5 -> cond_take_l_n_xs(x5 bot[0](), x4) 13: take_l_1() x4 -> take_l_n(x4) 14: take_l() x8 -> take_l_n(x8) 15: main_3(x0, x5, x9) x13 -> fib(take_l(), fibs(x5, x9, x13)) x0 16: cond_tail_l_xs(NilL()) -> bot[1]() 17: cond_tail_l_xs(ConsL(x4, x5)) -> x5 18: tail_l() x3 -> cond_tail_l_xs(x3 bot[2]()) 19: main_2(x0, x6) x10 -> main_6(x0) fib(take_l(), fibs(x6, x10, tail_l())) 20: cond_plus_x_y(0(), x3) -> x3 21: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 22: plus_x(x2) x3 -> cond_plus_x_y(x2, x3) 23: plus_1() x2 -> plus_x(x2) 24: plus() x4 -> plus_x(x4) 25: main_1(x0) x4 -> main_5(x0, take_l()) fibs(x4, plus(), tail_l()) 26: cond_zipwith_l_f_xs_ys_1(NilL(), x1, x5, x6) -> NilL() 27: cond_zipwith_l_f_xs_ys_1(ConsL(x7, x8), x1, x5, x6) -> ConsL(x1 x5 x7, zipwith_l() x1 x6 x8) 28: cond_zipwith_l_f_xs_ys(NilL(), x1, x3) -> NilL() 29: cond_zipwith_l_f_xs_ys(ConsL(x5, x6), x1, x3) -> cond_zipwith_l_f_xs_ys_1(x3 bot[3](), x1, x5, x6) 30: zipwith_l_f_xs_ys(x1, x2, x3) x4 -> cond_zipwith_l_f_xs_ys(x2 bot[4](), x1, x3) 31: zipwith_l_f_xs(x1, x2) x3 -> zipwith_l_f_xs_ys(x1, x2, x3) 32: zipwith_l_f(x1) x2 -> zipwith_l_f_xs(x1, x2) 33: zipwith_l_1() x1 -> zipwith_l_f(x1) 34: zipwith_l() x2 -> zipwith_l_f(x2) 35: main(x0) -> main_4(x0, zipwith_l(), plus(), tail_l()) take_l() where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a llist) -> 'a llist Nil :: 'a list NilL :: 'a llist S :: nat -> nat zipwith_l_f :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fib :: (nat -> (Unit -> nat llist) -> nat list) -> (Unit -> nat llist) -> nat -> nat list take_l_n :: nat -> (Unit -> nat llist) -> nat list tail_l :: (Unit -> nat llist) -> Unit -> nat llist plus_x :: nat -> nat -> nat zipwith_l_f_xs :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fibs_1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main_1 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> nat list plus_1 :: nat -> nat -> nat take_l_1 :: nat -> (Unit -> nat llist) -> nat list zipwith_l_1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fibs_2 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main_2 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> nat list main_3 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> nat list main_4 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> (nat -> (Unit -> nat llist) -> nat list) -> nat list main_5 :: nat -> (nat -> (Unit -> nat llist) -> nat list) -> (Unit -> nat llist) -> nat list main_6 :: nat -> (nat -> nat list) -> nat list bot[0] :: Unit bot[1] :: Unit -> nat llist bot[2] :: Unit bot[3] :: Unit bot[4] :: Unit cond_take_l_n_xs :: nat llist -> nat -> nat list cond_tail_l_xs :: nat llist -> Unit -> nat llist cond_plus_x_y :: nat -> nat -> nat cond_zipwith_l_f_xs_ys :: nat llist -> (nat -> nat -> nat) -> (Unit -> nat llist) -> nat llist cond_take_l_n_xs_1 :: nat -> nat -> (Unit -> nat llist) -> nat list cond_zipwith_l_f_xs_ys_1 :: nat llist -> (nat -> nat -> nat) -> nat -> (Unit -> nat llist) -> nat llist fibs :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist plus :: nat -> nat -> nat take_l :: nat -> (Unit -> nat llist) -> nat list zipwith_l :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist main :: nat -> nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 6: Inline MAYBE + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: fib(x4, x5) x6 -> x4 x6 x5 3: main_5(x12, x8) x10 -> x8 x12 x10 4: fibs_2(x1, x2, x3) x6 -> ConsL(S(0()), x1 x2 fibs(x1, x2, x3) (x3 fibs(x1, x2, x3))) 5: fibs_1(x1, x2, x3) x5 -> ConsL(0(), fibs_2(x1, x2, x3)) 6: fibs(x2, x4, x6) x10 -> ConsL(0(), fibs_2(x2, x4, x6)) 7: main_4(x12, x15, x23, x31) x8 -> x8 x12 fibs(x15, x23, x31) 8: cond_take_l_n_xs_1(0(), x6, x7) -> Nil() 9: cond_take_l_n_xs_1(S(x8), x6, x7) -> Cons(x6, take_l() x8 x7) 10: cond_take_l_n_xs(NilL(), x4) -> Nil() 11: cond_take_l_n_xs(ConsL(x6, x7), x4) -> cond_take_l_n_xs_1(x4, x6, x7) 12: take_l_n(x4) x5 -> cond_take_l_n_xs(x5 bot[0](), x4) 13: take_l_1() x4 -> take_l_n(x4) 14: take_l() x8 -> take_l_n(x8) 15: main_3(x12, x11, x19) x27 -> take_l() x12 fibs(x11, x19, x27) 16: cond_tail_l_xs(NilL()) -> bot[1]() 17: cond_tail_l_xs(ConsL(x4, x5)) -> x5 18: tail_l() x3 -> cond_tail_l_xs(x3 bot[2]()) 19: main_2(x0, x13) x21 -> fib(take_l(), fibs(x13, x21, tail_l())) x0 20: cond_plus_x_y(0(), x3) -> x3 21: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 22: plus_x(x2) x3 -> cond_plus_x_y(x2, x3) 23: plus_1() x2 -> plus_x(x2) 24: plus() x4 -> plus_x(x4) 25: main_1(x24) x9 -> take_l() x24 fibs(x9, plus(), tail_l()) 26: cond_zipwith_l_f_xs_ys_1(NilL(), x1, x5, x6) -> NilL() 27: cond_zipwith_l_f_xs_ys_1(ConsL(x7, x8), x1, x5, x6) -> ConsL(x1 x5 x7, zipwith_l() x1 x6 x8) 28: cond_zipwith_l_f_xs_ys(NilL(), x1, x3) -> NilL() 29: cond_zipwith_l_f_xs_ys(ConsL(x5, x6), x1, x3) -> cond_zipwith_l_f_xs_ys_1(x3 bot[3](), x1, x5, x6) 30: zipwith_l_f_xs_ys(x1, x2, x3) x4 -> cond_zipwith_l_f_xs_ys(x2 bot[4](), x1, x3) 31: zipwith_l_f_xs(x1, x2) x3 -> zipwith_l_f_xs_ys(x1, x2, x3) 32: zipwith_l_f(x1) x2 -> zipwith_l_f_xs(x1, x2) 33: zipwith_l_1() x1 -> zipwith_l_f(x1) 34: zipwith_l() x2 -> zipwith_l_f(x2) 35: main(x0) -> fib(take_l(), fibs(zipwith_l(), plus(), tail_l())) x0 where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a llist) -> 'a llist Nil :: 'a list NilL :: 'a llist S :: nat -> nat zipwith_l_f :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fib :: (nat -> (Unit -> nat llist) -> nat list) -> (Unit -> nat llist) -> nat -> nat list take_l_n :: nat -> (Unit -> nat llist) -> nat list tail_l :: (Unit -> nat llist) -> Unit -> nat llist plus_x :: nat -> nat -> nat zipwith_l_f_xs :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fibs_1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main_1 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> nat list plus_1 :: nat -> nat -> nat take_l_1 :: nat -> (Unit -> nat llist) -> nat list zipwith_l_1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fibs_2 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main_2 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> nat list main_3 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> nat list main_4 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> (nat -> (Unit -> nat llist) -> nat list) -> nat list main_5 :: nat -> (nat -> (Unit -> nat llist) -> nat list) -> (Unit -> nat llist) -> nat list main_6 :: nat -> (nat -> nat list) -> nat list bot[0] :: Unit bot[1] :: Unit -> nat llist bot[2] :: Unit bot[3] :: Unit bot[4] :: Unit cond_take_l_n_xs :: nat llist -> nat -> nat list cond_tail_l_xs :: nat llist -> Unit -> nat llist cond_plus_x_y :: nat -> nat -> nat cond_zipwith_l_f_xs_ys :: nat llist -> (nat -> nat -> nat) -> (Unit -> nat llist) -> nat llist cond_take_l_n_xs_1 :: nat -> nat -> (Unit -> nat llist) -> nat list cond_zipwith_l_f_xs_ys_1 :: nat llist -> (nat -> nat -> nat) -> nat -> (Unit -> nat llist) -> nat llist fibs :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist plus :: nat -> nat -> nat take_l :: nat -> (Unit -> nat llist) -> nat list zipwith_l :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist main :: nat -> nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 7: Inline MAYBE + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: fib(x4, x5) x6 -> x4 x6 x5 3: main_5(x12, x8) x10 -> x8 x12 x10 4: fibs_2(x1, x2, x3) x6 -> ConsL(S(0()), x1 x2 fibs(x1, x2, x3) (x3 fibs(x1, x2, x3))) 5: fibs_1(x1, x2, x3) x5 -> ConsL(0(), fibs_2(x1, x2, x3)) 6: fibs(x2, x4, x6) x10 -> ConsL(0(), fibs_2(x2, x4, x6)) 7: main_4(x12, x15, x23, x31) x8 -> x8 x12 fibs(x15, x23, x31) 8: cond_take_l_n_xs_1(0(), x6, x7) -> Nil() 9: cond_take_l_n_xs_1(S(x8), x6, x7) -> Cons(x6, take_l() x8 x7) 10: cond_take_l_n_xs(NilL(), x4) -> Nil() 11: cond_take_l_n_xs(ConsL(x6, x7), x4) -> cond_take_l_n_xs_1(x4, x6, x7) 12: take_l_n(x4) x5 -> cond_take_l_n_xs(x5 bot[0](), x4) 13: take_l_1() x4 -> take_l_n(x4) 14: take_l() x8 -> take_l_n(x8) 15: main_3(x12, x11, x19) x27 -> take_l() x12 fibs(x11, x19, x27) 16: cond_tail_l_xs(NilL()) -> bot[1]() 17: cond_tail_l_xs(ConsL(x4, x5)) -> x5 18: tail_l() x3 -> cond_tail_l_xs(x3 bot[2]()) 19: main_2(x12, x27) x43 -> take_l() x12 fibs(x27, x43, tail_l()) 20: cond_plus_x_y(0(), x3) -> x3 21: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 22: plus_x(x2) x3 -> cond_plus_x_y(x2, x3) 23: plus_1() x2 -> plus_x(x2) 24: plus() x4 -> plus_x(x4) 25: main_1(x24) x9 -> take_l() x24 fibs(x9, plus(), tail_l()) 26: cond_zipwith_l_f_xs_ys_1(NilL(), x1, x5, x6) -> NilL() 27: cond_zipwith_l_f_xs_ys_1(ConsL(x7, x8), x1, x5, x6) -> ConsL(x1 x5 x7, zipwith_l() x1 x6 x8) 28: cond_zipwith_l_f_xs_ys(NilL(), x1, x3) -> NilL() 29: cond_zipwith_l_f_xs_ys(ConsL(x5, x6), x1, x3) -> cond_zipwith_l_f_xs_ys_1(x3 bot[3](), x1, x5, x6) 30: zipwith_l_f_xs_ys(x1, x2, x3) x4 -> cond_zipwith_l_f_xs_ys(x2 bot[4](), x1, x3) 31: zipwith_l_f_xs(x1, x2) x3 -> zipwith_l_f_xs_ys(x1, x2, x3) 32: zipwith_l_f(x1) x2 -> zipwith_l_f_xs(x1, x2) 33: zipwith_l_1() x1 -> zipwith_l_f(x1) 34: zipwith_l() x2 -> zipwith_l_f(x2) 35: main(x12) -> take_l() x12 fibs(zipwith_l(), plus(), tail_l()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a llist) -> 'a llist Nil :: 'a list NilL :: 'a llist S :: nat -> nat zipwith_l_f :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fib :: (nat -> (Unit -> nat llist) -> nat list) -> (Unit -> nat llist) -> nat -> nat list take_l_n :: nat -> (Unit -> nat llist) -> nat list tail_l :: (Unit -> nat llist) -> Unit -> nat llist plus_x :: nat -> nat -> nat zipwith_l_f_xs :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fibs_1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main_1 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> nat list plus_1 :: nat -> nat -> nat take_l_1 :: nat -> (Unit -> nat llist) -> nat list zipwith_l_1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fibs_2 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main_2 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> nat list main_3 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> nat list main_4 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> (nat -> (Unit -> nat llist) -> nat list) -> nat list main_5 :: nat -> (nat -> (Unit -> nat llist) -> nat list) -> (Unit -> nat llist) -> nat list main_6 :: nat -> (nat -> nat list) -> nat list bot[0] :: Unit bot[1] :: Unit -> nat llist bot[2] :: Unit bot[3] :: Unit bot[4] :: Unit cond_take_l_n_xs :: nat llist -> nat -> nat list cond_tail_l_xs :: nat llist -> Unit -> nat llist cond_plus_x_y :: nat -> nat -> nat cond_zipwith_l_f_xs_ys :: nat llist -> (nat -> nat -> nat) -> (Unit -> nat llist) -> nat llist cond_take_l_n_xs_1 :: nat -> nat -> (Unit -> nat llist) -> nat list cond_zipwith_l_f_xs_ys_1 :: nat llist -> (nat -> nat -> nat) -> nat -> (Unit -> nat llist) -> nat llist fibs :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist plus :: nat -> nat -> nat take_l :: nat -> (Unit -> nat llist) -> nat list zipwith_l :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist main :: nat -> nat list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 8: UsableRules MAYBE + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: fib(x4, x5) x6 -> x4 x6 x5 3: main_5(x12, x8) x10 -> x8 x12 x10 4: fibs_2(x1, x2, x3) x6 -> ConsL(S(0()), x1 x2 fibs(x1, x2, x3) (x3 fibs(x1, x2, x3))) 5: fibs_1(x1, x2, x3) x5 -> ConsL(0(), fibs_2(x1, x2, x3)) 6: fibs(x2, x4, x6) x10 -> ConsL(0(), fibs_2(x2, x4, x6)) 7: main_4(x12, x15, x23, x31) x8 -> x8 x12 fibs(x15, x23, x31) 8: cond_take_l_n_xs_1(0(), x6, x7) -> Nil() 9: cond_take_l_n_xs_1(S(x8), x6, x7) -> Cons(x6, take_l() x8 x7) 10: cond_take_l_n_xs(NilL(), x4) -> Nil() 11: cond_take_l_n_xs(ConsL(x12, x14), 0()) -> Nil() 12: cond_take_l_n_xs(ConsL(x12, x14), S(x16)) -> Cons(x12, take_l() x16 x14) 13: take_l_n(x4) x5 -> cond_take_l_n_xs(x5 bot[0](), x4) 14: take_l_1() x4 -> take_l_n(x4) 15: take_l() x8 -> take_l_n(x8) 16: main_3(x12, x11, x19) x27 -> take_l() x12 fibs(x11, x19, x27) 17: cond_tail_l_xs(NilL()) -> bot[1]() 18: cond_tail_l_xs(ConsL(x4, x5)) -> x5 19: tail_l() x3 -> cond_tail_l_xs(x3 bot[2]()) 20: main_2(x12, x27) x43 -> take_l() x12 fibs(x27, x43, tail_l()) 21: cond_plus_x_y(0(), x3) -> x3 22: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 23: plus_x(0()) x6 -> x6 24: plus_x(S(x8)) x6 -> S(plus() x8 x6) 25: plus_1() x2 -> plus_x(x2) 26: plus() x4 -> plus_x(x4) 27: main_1(x24) x9 -> take_l() x24 fibs(x9, plus(), tail_l()) 28: cond_zipwith_l_f_xs_ys_1(NilL(), x1, x5, x6) -> NilL() 29: cond_zipwith_l_f_xs_ys_1(ConsL(x7, x8), x1, x5, x6) -> ConsL(x1 x5 x7, zipwith_l() x1 x6 x8) 30: cond_zipwith_l_f_xs_ys(NilL(), x1, x3) -> NilL() 31: cond_zipwith_l_f_xs_ys(ConsL(x5, x6), x1, x3) -> cond_zipwith_l_f_xs_ys_1(x3 bot[3](), x1, x5, x6) 32: zipwith_l_f_xs_ys(x1, x2, x3) x4 -> cond_zipwith_l_f_xs_ys(x2 bot[4](), x1, x3) 33: zipwith_l_f_xs(x1, x2) x3 -> zipwith_l_f_xs_ys(x1, x2, x3) 34: zipwith_l_f(x1) x2 -> zipwith_l_f_xs(x1, x2) 35: zipwith_l_1() x1 -> zipwith_l_f(x1) 36: zipwith_l() x2 -> zipwith_l_f(x2) 37: main(x12) -> take_l() x12 fibs(zipwith_l(), plus(), tail_l()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a llist) -> 'a llist Nil :: 'a list NilL :: 'a llist S :: nat -> nat zipwith_l_f :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fib :: (nat -> (Unit -> nat llist) -> nat list) -> (Unit -> nat llist) -> nat -> nat list take_l_n :: nat -> (Unit -> nat llist) -> nat list tail_l :: (Unit -> nat llist) -> Unit -> nat llist plus_x :: nat -> nat -> nat zipwith_l_f_xs :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fibs_1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main_1 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> nat list plus_1 :: nat -> nat -> nat take_l_1 :: nat -> (Unit -> nat llist) -> nat list zipwith_l_1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fibs_2 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main_2 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> nat list main_3 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> nat list main_4 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> (nat -> (Unit -> nat llist) -> nat list) -> nat list main_5 :: nat -> (nat -> (Unit -> nat llist) -> nat list) -> (Unit -> nat llist) -> nat list main_6 :: nat -> (nat -> nat list) -> nat list bot[0] :: Unit bot[1] :: Unit -> nat llist bot[2] :: Unit bot[3] :: Unit bot[4] :: Unit cond_take_l_n_xs :: nat llist -> nat -> nat list cond_tail_l_xs :: nat llist -> Unit -> nat llist cond_plus_x_y :: nat -> nat -> nat cond_zipwith_l_f_xs_ys :: nat llist -> (nat -> nat -> nat) -> (Unit -> nat llist) -> nat llist cond_take_l_n_xs_1 :: nat -> nat -> (Unit -> nat llist) -> nat list cond_zipwith_l_f_xs_ys_1 :: nat llist -> (nat -> nat -> nat) -> nat -> (Unit -> nat llist) -> nat llist fibs :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist plus :: nat -> nat -> nat take_l :: nat -> (Unit -> nat llist) -> nat list zipwith_l :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist main :: nat -> nat list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 9: NeededRules MAYBE + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: fib(x4, x5) x6 -> x4 x6 x5 3: main_5(x12, x8) x10 -> x8 x12 x10 4: fibs_2(x1, x2, x3) x6 -> ConsL(S(0()), x1 x2 fibs(x1, x2, x3) (x3 fibs(x1, x2, x3))) 5: fibs_1(x1, x2, x3) x5 -> ConsL(0(), fibs_2(x1, x2, x3)) 6: fibs(x2, x4, x6) x10 -> ConsL(0(), fibs_2(x2, x4, x6)) 7: main_4(x12, x15, x23, x31) x8 -> x8 x12 fibs(x15, x23, x31) 10: cond_take_l_n_xs(NilL(), x4) -> Nil() 11: cond_take_l_n_xs(ConsL(x12, x14), 0()) -> Nil() 12: cond_take_l_n_xs(ConsL(x12, x14), S(x16)) -> Cons(x12, take_l() x16 x14) 13: take_l_n(x4) x5 -> cond_take_l_n_xs(x5 bot[0](), x4) 14: take_l_1() x4 -> take_l_n(x4) 15: take_l() x8 -> take_l_n(x8) 16: main_3(x12, x11, x19) x27 -> take_l() x12 fibs(x11, x19, x27) 17: cond_tail_l_xs(NilL()) -> bot[1]() 18: cond_tail_l_xs(ConsL(x4, x5)) -> x5 19: tail_l() x3 -> cond_tail_l_xs(x3 bot[2]()) 20: main_2(x12, x27) x43 -> take_l() x12 fibs(x27, x43, tail_l()) 23: plus_x(0()) x6 -> x6 24: plus_x(S(x8)) x6 -> S(plus() x8 x6) 25: plus_1() x2 -> plus_x(x2) 26: plus() x4 -> plus_x(x4) 27: main_1(x24) x9 -> take_l() x24 fibs(x9, plus(), tail_l()) 28: cond_zipwith_l_f_xs_ys_1(NilL(), x1, x5, x6) -> NilL() 29: cond_zipwith_l_f_xs_ys_1(ConsL(x7, x8), x1, x5, x6) -> ConsL(x1 x5 x7, zipwith_l() x1 x6 x8) 30: cond_zipwith_l_f_xs_ys(NilL(), x1, x3) -> NilL() 31: cond_zipwith_l_f_xs_ys(ConsL(x5, x6), x1, x3) -> cond_zipwith_l_f_xs_ys_1(x3 bot[3](), x1, x5, x6) 32: zipwith_l_f_xs_ys(x1, x2, x3) x4 -> cond_zipwith_l_f_xs_ys(x2 bot[4](), x1, x3) 33: zipwith_l_f_xs(x1, x2) x3 -> zipwith_l_f_xs_ys(x1, x2, x3) 34: zipwith_l_f(x1) x2 -> zipwith_l_f_xs(x1, x2) 35: zipwith_l_1() x1 -> zipwith_l_f(x1) 36: zipwith_l() x2 -> zipwith_l_f(x2) 37: main(x12) -> take_l() x12 fibs(zipwith_l(), plus(), tail_l()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a llist) -> 'a llist Nil :: 'a list NilL :: 'a llist S :: nat -> nat zipwith_l_f :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fib :: (nat -> (Unit -> nat llist) -> nat list) -> (Unit -> nat llist) -> nat -> nat list take_l_n :: nat -> (Unit -> nat llist) -> nat list tail_l :: (Unit -> nat llist) -> Unit -> nat llist plus_x :: nat -> nat -> nat zipwith_l_f_xs :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fibs_1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main_1 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> nat list plus_1 :: nat -> nat -> nat take_l_1 :: nat -> (Unit -> nat llist) -> nat list zipwith_l_1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fibs_2 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main_2 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> nat list main_3 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> nat list main_4 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> (nat -> (Unit -> nat llist) -> nat list) -> nat list main_5 :: nat -> (nat -> (Unit -> nat llist) -> nat list) -> (Unit -> nat llist) -> nat list main_6 :: nat -> (nat -> nat list) -> nat list bot[0] :: Unit bot[1] :: Unit -> nat llist bot[2] :: Unit bot[3] :: Unit bot[4] :: Unit cond_take_l_n_xs :: nat llist -> nat -> nat list cond_tail_l_xs :: nat llist -> Unit -> nat llist cond_zipwith_l_f_xs_ys :: nat llist -> (nat -> nat -> nat) -> (Unit -> nat llist) -> nat llist cond_zipwith_l_f_xs_ys_1 :: nat llist -> (nat -> nat -> nat) -> nat -> (Unit -> nat llist) -> nat llist fibs :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist plus :: nat -> nat -> nat take_l :: nat -> (Unit -> nat llist) -> nat list zipwith_l :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist main :: nat -> nat list + Applied Processor: NeededRules + Details: none * Step 10: CFA MAYBE + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: fib(x4, x5) x6 -> x4 x6 x5 3: main_5(x12, x8) x10 -> x8 x12 x10 4: fibs_2(x1, x2, x3) x6 -> ConsL(S(0()), x1 x2 fibs(x1, x2, x3) (x3 fibs(x1, x2, x3))) 5: fibs_1(x1, x2, x3) x5 -> ConsL(0(), fibs_2(x1, x2, x3)) 6: fibs(x2, x4, x6) x10 -> ConsL(0(), fibs_2(x2, x4, x6)) 7: main_4(x12, x15, x23, x31) x8 -> x8 x12 fibs(x15, x23, x31) 8: cond_take_l_n_xs(NilL(), x4) -> Nil() 9: cond_take_l_n_xs(ConsL(x12, x14), 0()) -> Nil() 10: cond_take_l_n_xs(ConsL(x12, x14), S(x16)) -> Cons(x12, take_l() x16 x14) 11: take_l_n(x4) x5 -> cond_take_l_n_xs(x5 bot[0](), x4) 12: take_l_1() x4 -> take_l_n(x4) 13: take_l() x8 -> take_l_n(x8) 14: main_3(x12, x11, x19) x27 -> take_l() x12 fibs(x11, x19, x27) 15: cond_tail_l_xs(NilL()) -> bot[1]() 16: cond_tail_l_xs(ConsL(x4, x5)) -> x5 17: tail_l() x3 -> cond_tail_l_xs(x3 bot[2]()) 18: main_2(x12, x27) x43 -> take_l() x12 fibs(x27, x43, tail_l()) 19: plus_x(0()) x6 -> x6 20: plus_x(S(x8)) x6 -> S(plus() x8 x6) 21: plus_1() x2 -> plus_x(x2) 22: plus() x4 -> plus_x(x4) 23: main_1(x24) x9 -> take_l() x24 fibs(x9, plus(), tail_l()) 24: cond_zipwith_l_f_xs_ys_1(NilL(), x1, x5, x6) -> NilL() 25: cond_zipwith_l_f_xs_ys_1(ConsL(x7, x8), x1, x5, x6) -> ConsL(x1 x5 x7, zipwith_l() x1 x6 x8) 26: cond_zipwith_l_f_xs_ys(NilL(), x1, x3) -> NilL() 27: cond_zipwith_l_f_xs_ys(ConsL(x5, x6), x1, x3) -> cond_zipwith_l_f_xs_ys_1(x3 bot[3](), x1, x5, x6) 28: zipwith_l_f_xs_ys(x1, x2, x3) x4 -> cond_zipwith_l_f_xs_ys(x2 bot[4](), x1, x3) 29: zipwith_l_f_xs(x1, x2) x3 -> zipwith_l_f_xs_ys(x1, x2, x3) 30: zipwith_l_f(x1) x2 -> zipwith_l_f_xs(x1, x2) 31: zipwith_l_1() x1 -> zipwith_l_f(x1) 32: zipwith_l() x2 -> zipwith_l_f(x2) 33: main(x12) -> take_l() x12 fibs(zipwith_l(), plus(), tail_l()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a llist) -> 'a llist Nil :: 'a list NilL :: 'a llist S :: nat -> nat zipwith_l_f :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fib :: (nat -> (Unit -> nat llist) -> nat list) -> (Unit -> nat llist) -> nat -> nat list take_l_n :: nat -> (Unit -> nat llist) -> nat list tail_l :: (Unit -> nat llist) -> Unit -> nat llist plus_x :: nat -> nat -> nat zipwith_l_f_xs :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fibs_1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main_1 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> nat list plus_1 :: nat -> nat -> nat take_l_1 :: nat -> (Unit -> nat llist) -> nat list zipwith_l_1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fibs_2 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main_2 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> nat list main_3 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> nat list main_4 :: nat -> ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> (nat -> (Unit -> nat llist) -> nat list) -> nat list main_5 :: nat -> (nat -> (Unit -> nat llist) -> nat list) -> (Unit -> nat llist) -> nat list main_6 :: nat -> (nat -> nat list) -> nat list bot[0] :: Unit bot[1] :: Unit -> nat llist bot[2] :: Unit bot[3] :: Unit bot[4] :: Unit cond_take_l_n_xs :: nat llist -> nat -> nat list cond_tail_l_xs :: nat llist -> Unit -> nat llist cond_zipwith_l_f_xs_ys :: nat llist -> (nat -> nat -> nat) -> (Unit -> nat llist) -> nat llist cond_zipwith_l_f_xs_ys_1 :: nat llist -> (nat -> nat -> nat) -> nat -> (Unit -> nat llist) -> nat llist fibs :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist plus :: nat -> nat -> nat take_l :: nat -> (Unit -> nat llist) -> nat list zipwith_l :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist main :: nat -> nat list + Applied Processor: CFA {cfaRefinement = } + Details: {X{*} -> ConsL(X{*},X{*}) | NilL() | NilL() | ConsL(X{*},X{*}) | ConsL(X{*},X{*}) | NilL() | NilL() | S(X{*}) | S(X{*}) | 0() | ConsL(X{*},X{*}) | NilL() | Cons(X{*},X{*}) | S(X{*}) | ConsL(X{*},X{*}) | Nil() | 0() | ConsL(X{*},X{*}) | Nil() | NilL() | 0() | ConsL(X{*},X{*}) | 0() | ConsL(X{*},X{*}) | 0() | S(X{*}) | ConsL(X{*},X{*}) ,V{x1_4} -> V{x2_6} ,V{x1_25} -> V{x1_27} ,V{x1_27} -> V{x1_28} ,V{x1_28} -> V{x1_29} ,V{x1_29} -> V{x1_30} ,V{x1_30} -> V{x2_32} ,V{x2_4} -> V{x4_6} ,V{x2_6} -> V{x1_4} | zipwith_l() ,V{x2_28} -> V{x2_29} ,V{x2_29} -> V{x2_30} ,V{x2_30} -> V{x6_25} | fibs(V{x1_4},V{x2_4},V{x3_4}) ,V{x2_32} -> V{x1_25} | V{x2_4} ,V{x3_4} -> V{x6_6} ,V{x3_17} -> fibs(V{x1_4},V{x2_4},V{x3_4}) ,V{x3_27} -> V{x3_28} ,V{x3_28} -> V{x3_29} ,V{x3_29} -> V{x8_25} | R{17} ,V{x4_6} -> V{x2_4} | plus() ,V{x4_11} -> V{x8_13} ,V{x4_16} -> 0() ,V{x4_22} -> V{x8_20} | V{x5_25} ,V{x4_28} -> bot[4]() | bot[3]() | bot[0]() ,V{x5_11} -> V{x14_10} | fibs(zipwith_l(),plus(),tail_l()) ,V{x5_16} -> fibs_2(V{x2_6},V{x4_6},V{x6_6}) ,V{x5_25} -> V{x5_27} ,V{x5_27} -> @(@(V{x1_25},V{x5_25}),V{x7_25}) | @(R{22},V{x7_25}) | R{19} | R{20} | S(0()) | 0() ,V{x6_4} -> bot[4]() | bot[3]() | bot[0]() ,V{x6_6} -> V{x3_4} | tail_l() ,V{x6_19} -> V{x6_20} | V{x7_25} ,V{x6_20} -> V{x6_20} | V{x7_25} ,V{x6_25} -> V{x6_27} ,V{x6_27} -> @(R{30},V{x8_25}) | @(@(R{32},V{x6_25}),V{x8_25}) | @(@(@(zipwith_l(),V{x1_25}),V{x6_25}),V{x8_25}) | @(@(@(V{x1_4},V{x2_4}),fibs(V{x1_4},V{x2_4},V{x3_4})),@(V{x3_4},fibs(V{x1_4},V{x2_4},V{x3_4}))) | @(@(R{32},fibs(V{x1_4},V{x2_4},V{x3_4})),@(V{x3_4},fibs(V{x1_4},V{x2_4},V{x3_4}))) | @(@(@(V{x1_4},V{x2_4}),fibs(V{x1_4},V{x2_4},V{x3_4})),R{17}) | @(@(R{32},fibs(V{x1_4},V{x2_4},V{x3_4})),R{17}) | @(R{30},@(V{x3_4},fibs(V{x1_4},V{x2_4},V{x3_4}))) | @(R{30},R{17}) | R{29} | fibs_2(V{x2_6},V{x4_6},V{x6_6}) ,V{x7_25} -> @(@(V{x1_25},V{x5_25}),V{x7_25}) | @(R{22},V{x7_25}) | R{19} | R{20} | S(0()) ,V{x8_13} -> V{x16_10} | V{x12_33} ,V{x8_20} -> R{20} | R{19} | @(R{22},V{x6_20}) | @(@(plus(),V{x8_20}),V{x6_20}) | 0() ,V{x8_25} -> @(R{30},V{x8_25}) | @(@(R{32},V{x6_25}),V{x8_25}) | @(@(@(zipwith_l(),V{x1_25}),V{x6_25}),V{x8_25}) | @(@(@(V{x1_4},V{x2_4}),fibs(V{x1_4},V{x2_4},V{x3_4})),@(V{x3_4},fibs(V{x1_4},V{x2_4},V{x3_4}))) | @(@(R{32},fibs(V{x1_4},V{x2_4},V{x3_4})),@(V{x3_4},fibs(V{x1_4},V{x2_4},V{x3_4}))) | @(@(@(V{x1_4},V{x2_4}),fibs(V{x1_4},V{x2_4},V{x3_4})),R{17}) | @(@(R{32},fibs(V{x1_4},V{x2_4},V{x3_4})),R{17}) | @(R{30},@(V{x3_4},fibs(V{x1_4},V{x2_4},V{x3_4}))) | @(R{30},R{17}) | R{29} ,V{x10_6} -> bot[4]() | bot[2]() | bot[0]() ,V{x12_9} -> R{20} | R{19} | @(R{22},V{x7_25}) | @(@(V{x1_25},V{x5_25}),V{x7_25}) | S(0()) | 0() ,V{x12_10} -> R{20} | R{19} | @(R{22},V{x7_25}) | @(@(V{x1_25},V{x5_25}),V{x7_25}) | S(0()) | 0() ,V{x12_33} -> X{*} ,V{x14_9} -> @(R{30},V{x8_25}) | @(@(R{32},V{x6_25}),V{x8_25}) | @(@(@(zipwith_l(),V{x1_25}),V{x6_25}),V{x8_25}) | @(@(@(V{x1_4},V{x2_4}),fibs(V{x1_4},V{x2_4},V{x3_4})),@(V{x3_4},fibs(V{x1_4},V{x2_4},V{x3_4}))) | @(@(R{32},fibs(V{x1_4},V{x2_4},V{x3_4})),@(V{x3_4},fibs(V{x1_4},V{x2_4},V{x3_4}))) | @(@(@(V{x1_4},V{x2_4}),fibs(V{x1_4},V{x2_4},V{x3_4})),R{17}) | @(@(R{32},fibs(V{x1_4},V{x2_4},V{x3_4})),R{17}) | @(R{30},@(V{x3_4},fibs(V{x1_4},V{x2_4},V{x3_4}))) | @(R{30},R{17}) | R{29} | fibs_2(V{x2_6},V{x4_6},V{x6_6}) ,V{x14_10} -> @(R{30},V{x8_25}) | @(@(R{32},V{x6_25}),V{x8_25}) | @(@(@(zipwith_l(),V{x1_25}),V{x6_25}),V{x8_25}) | @(@(@(V{x1_4},V{x2_4}),fibs(V{x1_4},V{x2_4},V{x3_4})),@(V{x3_4},fibs(V{x1_4},V{x2_4},V{x3_4}))) | @(@(R{32},fibs(V{x1_4},V{x2_4},V{x3_4})),@(V{x3_4},fibs(V{x1_4},V{x2_4},V{x3_4}))) | @(@(@(V{x1_4},V{x2_4}),fibs(V{x1_4},V{x2_4},V{x3_4})),R{17}) | @(@(R{32},fibs(V{x1_4},V{x2_4},V{x3_4})),R{17}) | @(R{30},@(V{x3_4},fibs(V{x1_4},V{x2_4},V{x3_4}))) | @(R{30},R{17}) | R{29} | fibs_2(V{x2_6},V{x4_6},V{x6_6}) ,V{x16_10} -> X{*} ,R{0} -> R{33} | main(X{*}) ,R{4} -> ConsL(S(0()),R{29}) | ConsL(S(0()),@(R{30},R{17})) | ConsL(S(0()),@(R{30},@(V{x3_4},fibs(V{x1_4},V{x2_4},V{x3_4})))) | ConsL(S(0()),@(@(R{32},fibs(V{x1_4},V{x2_4},V{x3_4})),R{17})) | ConsL(S(0()),@(@(@(V{x1_4},V{x2_4}),fibs(V{x1_4},V{x2_4},V{x3_4})),R{17})) | ConsL(S(0()),@(@(R{32},fibs(V{x1_4},V{x2_4},V{x3_4})),@(V{x3_4},fibs(V{x1_4},V{x2_4},V{x3_4})))) | ConsL(S(0()) ,@(@(@(V{x1_4},V{x2_4}),fibs(V{x1_4},V{x2_4},V{x3_4})),@(V{x3_4},fibs(V{x1_4},V{x2_4},V{x3_4})))) ,R{6} -> ConsL(0(),fibs_2(V{x2_6},V{x4_6},V{x6_6})) ,R{9} -> Nil() ,R{10} -> Cons(V{x12_10},R{11}) | Cons(V{x12_10},@(R{13},V{x14_10})) | Cons(V{x12_10},@(@(take_l(),V{x16_10}),V{x14_10})) ,R{11} -> cond_take_l_n_xs(R{28},V{x4_11}) | cond_take_l_n_xs(R{4},V{x4_11}) | R{10} | R{9} | cond_take_l_n_xs(R{6},V{x4_11}) | cond_take_l_n_xs(@(V{x5_11},bot[0]()),V{x4_11}) ,R{13} -> take_l_n(V{x8_13}) ,R{16} -> V{x5_16} ,R{17} -> R{16} | cond_tail_l_xs(R{6}) | cond_tail_l_xs(@(V{x3_17},bot[2]())) ,R{19} -> V{x6_19} ,R{20} -> S(R{20}) | S(R{19}) | S(@(R{22},V{x6_20})) | S(@(@(plus(),V{x8_20}),V{x6_20})) ,R{22} -> plus_x(V{x4_22}) ,R{25} -> ConsL(R{19},R{29}) | ConsL(R{20},R{29}) | ConsL(R{20},@(@(@(zipwith_l(),V{x1_25}),V{x6_25}),V{x8_25})) | ConsL(R{20},@(@(R{32},V{x6_25}),V{x8_25})) | ConsL(R{20},@(R{30},V{x8_25})) | ConsL(R{19},@(R{30},V{x8_25})) | ConsL(@(R{22},V{x7_25}),R{29}) | ConsL(@(@(V{x1_25},V{x5_25}),V{x7_25}),R{29}) | ConsL(@(R{22},V{x7_25}),@(R{30},V{x8_25})) | ConsL(R{19},@(@(R{32},V{x6_25}),V{x8_25})) | ConsL(R{19},@(@(@(zipwith_l(),V{x1_25}),V{x6_25}),V{x8_25})) | ConsL(@(@(V{x1_25},V{x5_25}),V{x7_25}),@(R{30},V{x8_25})) | ConsL(@(R{22},V{x7_25}),@(@(R{32},V{x6_25}),V{x8_25})) | ConsL(@(@(V{x1_25},V{x5_25}),V{x7_25}),@(@(R{32},V{x6_25}),V{x8_25})) | ConsL(@(R{22},V{x7_25}),@(@(@(zipwith_l(),V{x1_25}),V{x6_25}),V{x8_25})) | ConsL(@(@(V{x1_25},V{x5_25}),V{x7_25}),@(@(@(zipwith_l(),V{x1_25}),V{x6_25}),V{x8_25})) ,R{27} -> cond_zipwith_l_f_xs_ys_1(R{28},V{x1_27},V{x5_27},V{x6_27}) | R{25} | cond_zipwith_l_f_xs_ys_1(R{4},V{x1_27},V{x5_27},V{x6_27}) | cond_zipwith_l_f_xs_ys_1(@(V{x3_27},bot[3]()),V{x1_27},V{x5_27},V{x6_27}) ,R{28} -> cond_zipwith_l_f_xs_ys(R{28},V{x1_28},V{x3_28}) | cond_zipwith_l_f_xs_ys(R{4},V{x1_28},V{x3_28}) | R{27} | cond_zipwith_l_f_xs_ys(R{6},V{x1_28},V{x3_28}) | cond_zipwith_l_f_xs_ys(@(V{x2_28},bot[4]()),V{x1_28},V{x3_28}) ,R{29} -> zipwith_l_f_xs_ys(V{x1_29},V{x2_29},V{x3_29}) ,R{30} -> zipwith_l_f_xs(V{x1_30},V{x2_30}) ,R{32} -> zipwith_l_f(V{x2_32}) ,R{33} -> R{11} | @(R{13},fibs(zipwith_l(),plus(),tail_l())) | @(@(take_l(),V{x12_33}),fibs(zipwith_l(),plus(),tail_l()))} * Step 11: UncurryATRS MAYBE + Considered Problem: 4: fibs_2(zipwith_l(), plus(), tail_l()) x1 -> ConsL(S(0()), zipwith_l() plus() fibs(zipwith_l(), plus() , tail_l()) (tail_l() fibs(zipwith_l(), plus(), tail_l()))) 6: fibs(zipwith_l(), plus(), tail_l()) x1 -> ConsL(0(), fibs_2(zipwith_l(), plus(), tail_l())) 9: cond_take_l_n_xs(ConsL(x12, x14), 0()) -> Nil() 10: cond_take_l_n_xs(ConsL(x3, x2), S(x1)) -> Cons(x3, take_l() x1 x2) 11: take_l_n(x1) fibs(zipwith_l(), plus(), tail_l()) -> cond_take_l_n_xs(fibs(zipwith_l(), plus(), tail_l()) bot[0](), x1) 12: take_l_n(x4) fibs_2(x1, x2, x3) -> cond_take_l_n_xs(fibs_2(x1, x2, x3) bot[0](), x4) 13: take_l_n(x4) zipwith_l_f_xs_ys(x1, x2, x3) -> cond_take_l_n_xs(zipwith_l_f_xs_ys(x1, x2, x3) bot[0]() , x4) 15: take_l() x8 -> take_l_n(x8) 18: cond_tail_l_xs(ConsL(0(), fibs_2(x1, x2, x3))) -> fibs_2(x1, x2, x3) 19: tail_l() fibs(x1, x2, x3) -> cond_tail_l_xs(fibs(x1, x2, x3) bot[2]()) 21: plus_x(0()) x6 -> x6 22: plus_x(S(x2)) x1 -> S(plus() x2 x1) 24: plus() x4 -> plus_x(x4) 27: cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), plus(), x2, x1) -> ConsL(plus() x2 x4, zipwith_l() plus() x1 x3) 29: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), zipwith_l_f_xs_ys(x1, x2, x3)) -> cond_zipwith_l_f_xs_ys_1(zipwith_l_f_xs_ys(x1, x2, x3) bot[3](), plus(), x5, x4) 30: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), fibs_2(x1, x2, x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2(x1 , x2 , x3) bot[3]() , plus() , x5 , x4) 31: zipwith_l_f_xs_ys(plus(), fibs(x3, x4, x5), x2) x1 -> cond_zipwith_l_f_xs_ys(fibs(x3, x4, x5) bot[4]() , plus(), x2) 32: zipwith_l_f_xs_ys(plus(), fibs_2(x3, x4, x5), x2) x1 -> cond_zipwith_l_f_xs_ys(fibs_2(x3, x4, x5) bot[4](), plus(), x2) 33: zipwith_l_f_xs_ys(plus(), zipwith_l_f_xs_ys(x3, x4, x5), x2) x1 -> cond_zipwith_l_f_xs_ys(zipwith_l_f_xs_ys(x3, x4, x5) bot[4](), plus(), x2) 34: zipwith_l_f_xs(plus(), x2) x1 -> zipwith_l_f_xs_ys(plus(), x2, x1) 35: zipwith_l_f(plus()) x1 -> zipwith_l_f_xs(plus(), x1) 37: zipwith_l() plus() -> zipwith_l_f(plus()) 38: main(x1) -> take_l() x1 fibs(zipwith_l(), plus(), tail_l()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a llist) -> 'a llist Nil :: 'a list S :: nat -> nat zipwith_l_f :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist take_l_n :: nat -> (Unit -> nat llist) -> nat list tail_l :: (Unit -> nat llist) -> Unit -> nat llist plus_x :: nat -> nat -> nat zipwith_l_f_xs :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist fibs_2 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist bot[0] :: Unit bot[2] :: Unit bot[3] :: Unit bot[4] :: Unit cond_take_l_n_xs :: nat llist -> nat -> nat list cond_tail_l_xs :: nat llist -> Unit -> nat llist cond_zipwith_l_f_xs_ys :: nat llist -> (nat -> nat -> nat) -> (Unit -> nat llist) -> nat llist cond_zipwith_l_f_xs_ys_1 :: nat llist -> (nat -> nat -> nat) -> nat -> (Unit -> nat llist) -> nat llist fibs :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist plus :: nat -> nat -> nat take_l :: nat -> (Unit -> nat llist) -> nat list zipwith_l :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist main :: nat -> nat list + Applied Processor: UncurryATRS + Details: none * Step 12: UsableRules MAYBE + Considered Problem: 1: fibs_2#1(zipwith_l(), plus(), tail_l(), x1) -> ConsL(S(0()), zipwith_l#3(plus(), fibs(zipwith_l(), plus() , tail_l()) , tail_l#1(fibs(zipwith_l(), plus() , tail_l())))) 2: fibs#1(zipwith_l(), plus(), tail_l(), x1) -> ConsL(0(), fibs_2(zipwith_l(), plus(), tail_l())) 3: cond_take_l_n_xs(ConsL(x12, x14), 0()) -> Nil() 4: cond_take_l_n_xs(ConsL(x3, x2), S(x1)) -> Cons(x3, take_l#2(x1, x2)) 5: take_l_n#1(x1, fibs(zipwith_l(), plus(), tail_l())) -> cond_take_l_n_xs(fibs#1(zipwith_l(), plus() , tail_l() , bot[0]()), x1) 6: take_l_n#1(x4, fibs_2(x1, x2, x3)) -> cond_take_l_n_xs(fibs_2#1(x1, x2, x3, bot[0]()), x4) 7: take_l_n#1(x4, zipwith_l_f_xs_ys(x1, x2, x3)) -> cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x1, x2 , x3 , bot[0]()), x4) 8: take_l#1(x8) -> take_l_n(x8) 9: take_l#2(x8, x9) -> take_l_n#1(x8, x9) 10: cond_tail_l_xs(ConsL(0(), fibs_2(x1, x2, x3))) -> fibs_2(x1, x2, x3) 11: tail_l#1(fibs(x1, x2, x3)) -> cond_tail_l_xs(fibs#1(x1, x2, x3, bot[2]())) 12: plus_x#1(0(), x6) -> x6 13: plus_x#1(S(x2), x1) -> S(plus#2(x2, x1)) 14: plus#1(x4) -> plus_x(x4) 15: plus#2(x4, x5) -> plus_x#1(x4, x5) 16: cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), plus(), x2, x1) -> ConsL(plus#2(x2, x4), zipwith_l#3(plus(), x1 , x3)) 17: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), 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[3]()), plus(), x5, x4) 18: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), fibs_2(x1, x2, x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3, bot[3]()), plus(), x5, x4) 19: zipwith_l_f_xs_ys#1(plus(), fibs(x3, x4, x5), x2, x1) -> cond_zipwith_l_f_xs_ys(fibs#1(x3, x4 , x5 , bot[4]()), plus() , x2) 20: 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[4]()) , plus(), x2) 21: 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[4]()), plus(), x2) 22: zipwith_l_f_xs#1(plus(), x2, x1) -> zipwith_l_f_xs_ys(plus(), x2, x1) 23: zipwith_l_f#1(plus(), x1) -> zipwith_l_f_xs(plus(), x1) 24: zipwith_l_f#2(plus(), x1, x2) -> zipwith_l_f_xs#1(plus(), x1, x2) 25: zipwith_l#1(plus()) -> zipwith_l_f(plus()) 26: zipwith_l#2(plus(), x0) -> zipwith_l_f#1(plus(), x0) 27: zipwith_l#3(plus(), x0, x1) -> zipwith_l_f#2(plus(), x0, x1) 28: main(x1) -> take_l#2(x1, fibs(zipwith_l(), plus(), tail_l())) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a llist) -> 'a llist Nil :: 'a list S :: nat -> nat bot[0] :: Unit bot[2] :: Unit bot[3] :: Unit bot[4] :: Unit cond_tail_l_xs :: nat llist -> Unit -> nat llist cond_take_l_n_xs :: nat llist -> nat -> nat list cond_zipwith_l_f_xs_ys :: nat llist -> (nat -> nat -> nat) -> (Unit -> nat llist) -> nat llist cond_zipwith_l_f_xs_ys_1 :: nat llist -> (nat -> nat -> nat) -> nat -> (Unit -> nat llist) -> nat llist fibs :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main :: nat -> nat list plus :: nat -> nat -> nat plus#1 :: nat -> nat -> nat plus#2 :: nat -> nat -> nat plus_x :: nat -> nat -> nat plus_x#1 :: nat -> nat -> nat tail_l :: (Unit -> nat llist) -> Unit -> nat llist tail_l#1 :: (Unit -> nat llist) -> Unit -> nat llist take_l#1 :: nat -> (Unit -> nat llist) -> nat list take_l#2 :: nat -> (Unit -> nat llist) -> nat list take_l_n :: nat -> (Unit -> nat llist) -> nat list take_l_n#1 :: nat -> (Unit -> nat llist) -> nat list zipwith_l :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l#1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l#2 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l#3 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f#1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f#2 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs#1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys#1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 13: Inline MAYBE + Considered Problem: 1: fibs_2#1(zipwith_l(), plus(), tail_l(), x1) -> ConsL(S(0()), zipwith_l#3(plus(), fibs(zipwith_l(), plus() , tail_l()) , tail_l#1(fibs(zipwith_l(), plus() , tail_l())))) 2: fibs#1(zipwith_l(), plus(), tail_l(), x1) -> ConsL(0(), fibs_2(zipwith_l(), plus(), tail_l())) 3: cond_take_l_n_xs(ConsL(x12, x14), 0()) -> Nil() 4: cond_take_l_n_xs(ConsL(x3, x2), S(x1)) -> Cons(x3, take_l#2(x1, x2)) 5: take_l_n#1(x1, fibs(zipwith_l(), plus(), tail_l())) -> cond_take_l_n_xs(fibs#1(zipwith_l(), plus() , tail_l() , bot[0]()), x1) 6: take_l_n#1(x4, fibs_2(x1, x2, x3)) -> cond_take_l_n_xs(fibs_2#1(x1, x2, x3, bot[0]()), x4) 7: take_l_n#1(x4, zipwith_l_f_xs_ys(x1, x2, x3)) -> cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x1, x2 , x3 , bot[0]()), x4) 9: take_l#2(x8, x9) -> take_l_n#1(x8, x9) 10: cond_tail_l_xs(ConsL(0(), fibs_2(x1, x2, x3))) -> fibs_2(x1, x2, x3) 11: tail_l#1(fibs(x1, x2, x3)) -> cond_tail_l_xs(fibs#1(x1, x2, x3, bot[2]())) 12: plus_x#1(0(), x6) -> x6 13: plus_x#1(S(x2), x1) -> S(plus#2(x2, x1)) 15: plus#2(x4, x5) -> plus_x#1(x4, x5) 16: cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), plus(), x2, x1) -> ConsL(plus#2(x2, x4), zipwith_l#3(plus(), x1 , x3)) 17: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), 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[3]()), plus(), x5, x4) 18: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), fibs_2(x1, x2, x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3, bot[3]()), plus(), x5, x4) 19: zipwith_l_f_xs_ys#1(plus(), fibs(x3, x4, x5), x2, x1) -> cond_zipwith_l_f_xs_ys(fibs#1(x3, x4 , x5 , bot[4]()), plus() , x2) 20: 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[4]()) , plus(), x2) 21: 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[4]()), plus(), x2) 22: zipwith_l_f_xs#1(plus(), x2, x1) -> zipwith_l_f_xs_ys(plus(), x2, x1) 24: zipwith_l_f#2(plus(), x1, x2) -> zipwith_l_f_xs#1(plus(), x1, x2) 27: zipwith_l#3(plus(), x0, x1) -> zipwith_l_f#2(plus(), x0, x1) 28: main(x1) -> take_l#2(x1, fibs(zipwith_l(), plus(), tail_l())) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a llist) -> 'a llist Nil :: 'a list S :: nat -> nat bot[0] :: Unit bot[2] :: Unit bot[3] :: Unit bot[4] :: Unit cond_tail_l_xs :: nat llist -> Unit -> nat llist cond_take_l_n_xs :: nat llist -> nat -> nat list cond_zipwith_l_f_xs_ys :: nat llist -> (nat -> nat -> nat) -> (Unit -> nat llist) -> nat llist cond_zipwith_l_f_xs_ys_1 :: nat llist -> (nat -> nat -> nat) -> nat -> (Unit -> nat llist) -> nat llist fibs :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main :: nat -> nat list plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat plus_x#1 :: nat -> nat -> nat tail_l :: (Unit -> nat llist) -> Unit -> nat llist tail_l#1 :: (Unit -> nat llist) -> Unit -> nat llist take_l#2 :: nat -> (Unit -> nat llist) -> nat list take_l_n#1 :: nat -> (Unit -> nat llist) -> nat list zipwith_l :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l#3 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f#2 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs#1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys#1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 14: UsableRules MAYBE + Considered Problem: 1: fibs_2#1(zipwith_l(), plus(), tail_l(), x3) -> ConsL(S(0()), zipwith_l#3(plus(), fibs(zipwith_l(), plus() , tail_l()) , cond_tail_l_xs(fibs#1(zipwith_l() , plus() , tail_l() , bot[2]())))) 2: fibs#1(zipwith_l(), plus(), tail_l(), x1) -> ConsL(0(), fibs_2(zipwith_l(), plus(), tail_l())) 3: cond_take_l_n_xs(ConsL(x12, x14), 0()) -> Nil() 4: cond_take_l_n_xs(ConsL(x3, x2), S(x1)) -> Cons(x3, take_l#2(x1, x2)) 5: take_l_n#1(x1, fibs(zipwith_l(), plus(), tail_l())) -> cond_take_l_n_xs(fibs#1(zipwith_l(), plus() , tail_l() , bot[0]()), x1) 6: take_l_n#1(x4, fibs_2(x1, x2, x3)) -> cond_take_l_n_xs(fibs_2#1(x1, x2, x3, bot[0]()), x4) 7: take_l_n#1(x4, zipwith_l_f_xs_ys(x1, x2, x3)) -> cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x1, x2 , x3 , bot[0]()), x4) 8: take_l#2(x2, fibs(zipwith_l(), plus(), tail_l())) -> cond_take_l_n_xs(fibs#1(zipwith_l(), plus() , tail_l() , bot[0]()), x2) 9: take_l#2(x8, fibs_2(x2, x4, x6)) -> cond_take_l_n_xs(fibs_2#1(x2, x4, x6, bot[0]()), x8) 10: take_l#2(x8, zipwith_l_f_xs_ys(x2, x4, x6)) -> cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x2, x4 , x6 , bot[0]()), x8) 11: cond_tail_l_xs(ConsL(0(), fibs_2(x1, x2, x3))) -> fibs_2(x1, x2, x3) 12: tail_l#1(fibs(x1, x2, x3)) -> cond_tail_l_xs(fibs#1(x1, x2, x3, bot[2]())) 13: plus_x#1(0(), x6) -> x6 14: plus_x#1(S(x2), x1) -> S(plus#2(x2, x1)) 15: plus#2(0(), x12) -> x12 16: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 17: cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), plus(), x2, x1) -> ConsL(plus#2(x2, x4), zipwith_l#3(plus(), x1 , x3)) 18: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), 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[3]()), plus(), x5, x4) 19: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), fibs_2(x1, x2, x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3, bot[3]()), plus(), x5, x4) 20: zipwith_l_f_xs_ys#1(plus(), fibs(x3, x4, x5), x2, x1) -> cond_zipwith_l_f_xs_ys(fibs#1(x3, x4 , x5 , bot[4]()), plus() , x2) 21: 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[4]()) , plus(), x2) 22: 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[4]()), plus(), x2) 23: zipwith_l_f_xs#1(plus(), x2, x1) -> zipwith_l_f_xs_ys(plus(), x2, x1) 24: zipwith_l_f#2(plus(), x4, x2) -> zipwith_l_f_xs_ys(plus(), x4, x2) 25: zipwith_l#3(plus(), x2, x4) -> zipwith_l_f_xs#1(plus(), x2, x4) 26: main(x1) -> take_l#2(x1, fibs(zipwith_l(), plus(), tail_l())) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a llist) -> 'a llist Nil :: 'a list S :: nat -> nat bot[0] :: Unit bot[2] :: Unit bot[3] :: Unit bot[4] :: Unit cond_tail_l_xs :: nat llist -> Unit -> nat llist cond_take_l_n_xs :: nat llist -> nat -> nat list cond_zipwith_l_f_xs_ys :: nat llist -> (nat -> nat -> nat) -> (Unit -> nat llist) -> nat llist cond_zipwith_l_f_xs_ys_1 :: nat llist -> (nat -> nat -> nat) -> nat -> (Unit -> nat llist) -> nat llist fibs :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main :: nat -> nat list plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat plus_x#1 :: nat -> nat -> nat tail_l :: (Unit -> nat llist) -> Unit -> nat llist tail_l#1 :: (Unit -> nat llist) -> Unit -> nat llist take_l#2 :: nat -> (Unit -> nat llist) -> nat list take_l_n#1 :: nat -> (Unit -> nat llist) -> nat list zipwith_l :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l#3 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f#2 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs#1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys#1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 15: Inline MAYBE + Considered Problem: 1: fibs_2#1(zipwith_l(), plus(), tail_l(), x3) -> ConsL(S(0()), zipwith_l#3(plus(), fibs(zipwith_l(), plus() , tail_l()) , cond_tail_l_xs(fibs#1(zipwith_l() , plus() , tail_l() , bot[2]())))) 2: fibs#1(zipwith_l(), plus(), tail_l(), x1) -> ConsL(0(), fibs_2(zipwith_l(), plus(), tail_l())) 3: cond_take_l_n_xs(ConsL(x12, x14), 0()) -> Nil() 4: cond_take_l_n_xs(ConsL(x3, x2), S(x1)) -> Cons(x3, take_l#2(x1, x2)) 8: take_l#2(x2, fibs(zipwith_l(), plus(), tail_l())) -> cond_take_l_n_xs(fibs#1(zipwith_l(), plus() , tail_l() , bot[0]()), x2) 9: take_l#2(x8, fibs_2(x2, x4, x6)) -> cond_take_l_n_xs(fibs_2#1(x2, x4, x6, bot[0]()), x8) 10: take_l#2(x8, zipwith_l_f_xs_ys(x2, x4, x6)) -> cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x2, x4 , x6 , bot[0]()), x8) 11: cond_tail_l_xs(ConsL(0(), fibs_2(x1, x2, x3))) -> fibs_2(x1, x2, x3) 15: plus#2(0(), x12) -> x12 16: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 17: cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), plus(), x2, x1) -> ConsL(plus#2(x2, x4), zipwith_l#3(plus(), x1 , x3)) 18: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), 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[3]()), plus(), x5, x4) 19: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), fibs_2(x1, x2, x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3, bot[3]()), plus(), x5, x4) 20: zipwith_l_f_xs_ys#1(plus(), fibs(x3, x4, x5), x2, x1) -> cond_zipwith_l_f_xs_ys(fibs#1(x3, x4 , x5 , bot[4]()), plus() , x2) 21: 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[4]()) , plus(), x2) 22: 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[4]()), plus(), x2) 23: zipwith_l_f_xs#1(plus(), x2, x1) -> zipwith_l_f_xs_ys(plus(), x2, x1) 25: zipwith_l#3(plus(), x2, x4) -> zipwith_l_f_xs#1(plus(), x2, x4) 26: main(x1) -> take_l#2(x1, fibs(zipwith_l(), plus(), tail_l())) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a llist) -> 'a llist Nil :: 'a list S :: nat -> nat bot[0] :: Unit bot[2] :: Unit bot[3] :: Unit bot[4] :: Unit cond_tail_l_xs :: nat llist -> Unit -> nat llist cond_take_l_n_xs :: nat llist -> nat -> nat list cond_zipwith_l_f_xs_ys :: nat llist -> (nat -> nat -> nat) -> (Unit -> nat llist) -> nat llist cond_zipwith_l_f_xs_ys_1 :: nat llist -> (nat -> nat -> nat) -> nat -> (Unit -> nat llist) -> nat llist fibs :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main :: nat -> nat list plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat tail_l :: (Unit -> nat llist) -> Unit -> nat llist take_l#2 :: nat -> (Unit -> nat llist) -> nat list zipwith_l :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l#3 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs#1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys#1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 16: UsableRules MAYBE + Considered Problem: 1: fibs_2#1(zipwith_l(), plus(), tail_l(), x3) -> ConsL(S(0()), zipwith_l#3(plus(), fibs(zipwith_l(), plus() , tail_l()) , cond_tail_l_xs(fibs#1(zipwith_l() , plus() , tail_l() , bot[2]())))) 2: fibs#1(zipwith_l(), plus(), tail_l(), x1) -> ConsL(0(), fibs_2(zipwith_l(), plus(), tail_l())) 3: cond_take_l_n_xs(ConsL(x12, x14), 0()) -> Nil() 4: cond_take_l_n_xs(ConsL(x3, x2), S(x1)) -> Cons(x3, take_l#2(x1, x2)) 5: take_l#2(x2, fibs(zipwith_l(), plus(), tail_l())) -> cond_take_l_n_xs(fibs#1(zipwith_l(), plus() , tail_l() , bot[0]()), x2) 6: take_l#2(x8, fibs_2(x2, x4, x6)) -> cond_take_l_n_xs(fibs_2#1(x2, x4, x6, bot[0]()), x8) 7: take_l#2(x8, zipwith_l_f_xs_ys(x2, x4, x6)) -> cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x2, x4, x6, bot[0]()) , x8) 8: cond_tail_l_xs(ConsL(0(), fibs_2(x1, x2, x3))) -> fibs_2(x1, x2, x3) 9: plus#2(0(), x12) -> x12 10: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 11: cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), plus(), x2, x1) -> ConsL(plus#2(x2, x4), zipwith_l#3(plus(), x1 , x3)) 12: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), 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[3]()), plus(), x5, x4) 13: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), fibs_2(x1, x2, x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3, bot[3]()), plus(), x5, x4) 14: zipwith_l_f_xs_ys#1(plus(), fibs(x3, x4, x5), x2, x1) -> cond_zipwith_l_f_xs_ys(fibs#1(x3, x4 , x5 , bot[4]()), plus() , x2) 15: 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[4]()) , plus(), x2) 16: 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[4]()), plus(), x2) 17: zipwith_l_f_xs#1(plus(), x2, x1) -> zipwith_l_f_xs_ys(plus(), x2, x1) 18: zipwith_l#3(plus(), x4, x2) -> zipwith_l_f_xs_ys(plus(), x4, x2) 19: main(x1) -> take_l#2(x1, fibs(zipwith_l(), plus(), tail_l())) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a llist) -> 'a llist Nil :: 'a list S :: nat -> nat bot[0] :: Unit bot[2] :: Unit bot[3] :: Unit bot[4] :: Unit cond_tail_l_xs :: nat llist -> Unit -> nat llist cond_take_l_n_xs :: nat llist -> nat -> nat list cond_zipwith_l_f_xs_ys :: nat llist -> (nat -> nat -> nat) -> (Unit -> nat llist) -> nat llist cond_zipwith_l_f_xs_ys_1 :: nat llist -> (nat -> nat -> nat) -> nat -> (Unit -> nat llist) -> nat llist fibs :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main :: nat -> nat list plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat tail_l :: (Unit -> nat llist) -> Unit -> nat llist take_l#2 :: nat -> (Unit -> nat llist) -> nat list zipwith_l :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l#3 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs#1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys#1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 17: UsableRules MAYBE + Considered Problem: 1: fibs_2#1(zipwith_l(), plus(), tail_l(), x3) -> ConsL(S(0()), zipwith_l#3(plus(), fibs(zipwith_l(), plus() , tail_l()) , cond_tail_l_xs(fibs#1(zipwith_l() , plus() , tail_l() , bot[2]())))) 2: fibs#1(zipwith_l(), plus(), tail_l(), x1) -> ConsL(0(), fibs_2(zipwith_l(), plus(), tail_l())) 3: cond_take_l_n_xs(ConsL(x12, x14), 0()) -> Nil() 4: cond_take_l_n_xs(ConsL(x3, x2), S(x1)) -> Cons(x3, take_l#2(x1, x2)) 5: take_l#2(x2, fibs(zipwith_l(), plus(), tail_l())) -> cond_take_l_n_xs(fibs#1(zipwith_l(), plus() , tail_l() , bot[0]()), x2) 6: take_l#2(x8, fibs_2(x2, x4, x6)) -> cond_take_l_n_xs(fibs_2#1(x2, x4, x6, bot[0]()), x8) 7: take_l#2(x8, zipwith_l_f_xs_ys(x2, x4, x6)) -> cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x2, x4, x6, bot[0]()) , x8) 8: cond_tail_l_xs(ConsL(0(), fibs_2(x1, x2, x3))) -> fibs_2(x1, x2, x3) 9: plus#2(0(), x12) -> x12 10: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 11: cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), plus(), x2, x1) -> ConsL(plus#2(x2, x4), zipwith_l#3(plus(), x1 , x3)) 12: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), 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[3]()), plus(), x5, x4) 13: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), fibs_2(x1, x2, x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3, bot[3]()), plus(), x5, x4) 14: zipwith_l_f_xs_ys#1(plus(), fibs(x3, x4, x5), x2, x1) -> cond_zipwith_l_f_xs_ys(fibs#1(x3, x4 , x5 , bot[4]()), plus() , x2) 15: 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[4]()) , plus(), x2) 16: 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[4]()), plus(), x2) 18: zipwith_l#3(plus(), x4, x2) -> zipwith_l_f_xs_ys(plus(), x4, x2) 19: main(x1) -> take_l#2(x1, fibs(zipwith_l(), plus(), tail_l())) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a llist) -> 'a llist Nil :: 'a list S :: nat -> nat bot[0] :: Unit bot[2] :: Unit bot[3] :: Unit bot[4] :: Unit cond_tail_l_xs :: nat llist -> Unit -> nat llist cond_take_l_n_xs :: nat llist -> nat -> nat list cond_zipwith_l_f_xs_ys :: nat llist -> (nat -> nat -> nat) -> (Unit -> nat llist) -> nat llist cond_zipwith_l_f_xs_ys_1 :: nat llist -> (nat -> nat -> nat) -> nat -> (Unit -> nat llist) -> nat llist fibs :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main :: nat -> nat list plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat tail_l :: (Unit -> nat llist) -> Unit -> nat llist take_l#2 :: nat -> (Unit -> nat llist) -> nat list zipwith_l :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l#3 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys#1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 18: Inline MAYBE + Considered Problem: 1: fibs_2#1(zipwith_l(), plus(), tail_l(), x3) -> ConsL(S(0()), zipwith_l#3(plus(), fibs(zipwith_l(), plus() , tail_l()) , cond_tail_l_xs(fibs#1(zipwith_l() , plus() , tail_l() , bot[2]())))) 2: fibs#1(zipwith_l(), plus(), tail_l(), x1) -> ConsL(0(), fibs_2(zipwith_l(), plus(), tail_l())) 3: cond_take_l_n_xs(ConsL(x12, x14), 0()) -> Nil() 4: cond_take_l_n_xs(ConsL(x3, x2), S(x1)) -> Cons(x3, take_l#2(x1, x2)) 5: take_l#2(x2, fibs(zipwith_l(), plus(), tail_l())) -> cond_take_l_n_xs(fibs#1(zipwith_l(), plus() , tail_l() , bot[0]()), x2) 6: take_l#2(x8, fibs_2(x2, x4, x6)) -> cond_take_l_n_xs(fibs_2#1(x2, x4, x6, bot[0]()), x8) 7: take_l#2(x8, zipwith_l_f_xs_ys(x2, x4, x6)) -> cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x2, x4, x6, bot[0]()) , x8) 8: cond_tail_l_xs(ConsL(0(), fibs_2(x1, x2, x3))) -> fibs_2(x1, x2, x3) 9: plus#2(0(), x12) -> x12 10: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 11: cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), plus(), x2, x1) -> ConsL(plus#2(x2, x4), zipwith_l#3(plus(), x1 , x3)) 12: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), 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[3]()), plus(), x5, x4) 13: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), fibs_2(x1, x2, x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3, bot[3]()), plus(), x5, x4) 14: zipwith_l_f_xs_ys#1(plus(), fibs(x3, x4, x5), x2, x1) -> cond_zipwith_l_f_xs_ys(fibs#1(x3, x4 , x5 , bot[4]()), plus() , x2) 15: 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[4]()) , plus(), x2) 16: 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[4]()), plus(), x2) 17: zipwith_l#3(plus(), x4, x2) -> zipwith_l_f_xs_ys(plus(), x4, x2) 18: main(x1) -> take_l#2(x1, fibs(zipwith_l(), plus(), tail_l())) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a llist) -> 'a llist Nil :: 'a list S :: nat -> nat bot[0] :: Unit bot[2] :: Unit bot[3] :: Unit bot[4] :: Unit cond_tail_l_xs :: nat llist -> Unit -> nat llist cond_take_l_n_xs :: nat llist -> nat -> nat list cond_zipwith_l_f_xs_ys :: nat llist -> (nat -> nat -> nat) -> (Unit -> nat llist) -> nat llist cond_zipwith_l_f_xs_ys_1 :: nat llist -> (nat -> nat -> nat) -> nat -> (Unit -> nat llist) -> nat llist fibs :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main :: nat -> nat list plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat tail_l :: (Unit -> nat llist) -> Unit -> nat llist take_l#2 :: nat -> (Unit -> nat llist) -> nat list zipwith_l :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l#3 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys#1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 19: UsableRules MAYBE + Considered Problem: 1: fibs_2#1(zipwith_l(), plus(), tail_l(), x3) -> ConsL(S(0()), zipwith_l#3(plus(), fibs(zipwith_l(), plus() , tail_l()) , cond_tail_l_xs(fibs#1(zipwith_l() , plus() , tail_l() , bot[2]())))) 2: fibs#1(zipwith_l(), plus(), tail_l(), x1) -> ConsL(0(), fibs_2(zipwith_l(), plus(), tail_l())) 3: cond_take_l_n_xs(ConsL(x12, x14), 0()) -> Nil() 4: 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)) 5: 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)) 6: take_l#2(x2, fibs(zipwith_l(), plus(), tail_l())) -> cond_take_l_n_xs(fibs#1(zipwith_l(), plus() , tail_l() , bot[0]()), x2) 7: take_l#2(x8, fibs_2(x2, x4, x6)) -> cond_take_l_n_xs(fibs_2#1(x2, x4, x6, bot[0]()), x8) 8: take_l#2(x8, zipwith_l_f_xs_ys(x2, x4, x6)) -> cond_take_l_n_xs(zipwith_l_f_xs_ys#1(x2, x4, x6, bot[0]()) , x8) 9: cond_tail_l_xs(ConsL(0(), fibs_2(x1, x2, x3))) -> fibs_2(x1, x2, x3) 10: plus#2(0(), x12) -> x12 11: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 12: cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), plus(), x2, x1) -> ConsL(plus#2(x2, x4), zipwith_l#3(plus(), x1 , x3)) 13: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), 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[3]()), plus(), x5, x4) 14: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), fibs_2(x1, x2, x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3, bot[3]()), plus(), x5, x4) 15: zipwith_l_f_xs_ys#1(plus(), fibs(x3, x4, x5), x2, x1) -> cond_zipwith_l_f_xs_ys(fibs#1(x3, x4 , x5 , bot[4]()), plus() , x2) 16: 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[4]()) , plus(), x2) 17: 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[4]()), plus(), x2) 18: zipwith_l#3(plus(), x4, x2) -> zipwith_l_f_xs_ys(plus(), x4, x2) 19: main(x4) -> cond_take_l_n_xs(fibs#1(zipwith_l(), plus(), tail_l(), bot[0]()), x4) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a llist) -> 'a llist Nil :: 'a list S :: nat -> nat bot[0] :: Unit bot[2] :: Unit bot[3] :: Unit bot[4] :: Unit cond_tail_l_xs :: nat llist -> Unit -> nat llist cond_take_l_n_xs :: nat llist -> nat -> nat list cond_zipwith_l_f_xs_ys :: nat llist -> (nat -> nat -> nat) -> (Unit -> nat llist) -> nat llist cond_zipwith_l_f_xs_ys_1 :: nat llist -> (nat -> nat -> nat) -> nat -> (Unit -> nat llist) -> nat llist fibs :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main :: nat -> nat list plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat tail_l :: (Unit -> nat llist) -> Unit -> nat llist take_l#2 :: nat -> (Unit -> nat llist) -> nat list zipwith_l :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l#3 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys#1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 20: UsableRules MAYBE + Considered Problem: 1: fibs_2#1(zipwith_l(), plus(), tail_l(), x3) -> ConsL(S(0()), zipwith_l#3(plus(), fibs(zipwith_l(), plus() , tail_l()) , cond_tail_l_xs(fibs#1(zipwith_l() , plus() , tail_l() , bot[2]())))) 2: fibs#1(zipwith_l(), plus(), tail_l(), x1) -> ConsL(0(), fibs_2(zipwith_l(), plus(), tail_l())) 3: cond_take_l_n_xs(ConsL(x12, x14), 0()) -> Nil() 4: 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)) 5: 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)) 9: cond_tail_l_xs(ConsL(0(), fibs_2(x1, x2, x3))) -> fibs_2(x1, x2, x3) 10: plus#2(0(), x12) -> x12 11: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 12: cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), plus(), x2, x1) -> ConsL(plus#2(x2, x4), zipwith_l#3(plus(), x1 , x3)) 13: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), 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[3]()), plus(), x5, x4) 14: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), fibs_2(x1, x2, x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3, bot[3]()), plus(), x5, x4) 15: zipwith_l_f_xs_ys#1(plus(), fibs(x3, x4, x5), x2, x1) -> cond_zipwith_l_f_xs_ys(fibs#1(x3, x4 , x5 , bot[4]()), plus() , x2) 16: 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[4]()) , plus(), x2) 17: 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[4]()), plus(), x2) 18: zipwith_l#3(plus(), x4, x2) -> zipwith_l_f_xs_ys(plus(), x4, x2) 19: main(x4) -> cond_take_l_n_xs(fibs#1(zipwith_l(), plus(), tail_l(), bot[0]()), x4) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a llist) -> 'a llist Nil :: 'a list S :: nat -> nat bot[0] :: Unit bot[2] :: Unit bot[3] :: Unit bot[4] :: Unit cond_tail_l_xs :: nat llist -> Unit -> nat llist cond_take_l_n_xs :: nat llist -> nat -> nat list cond_zipwith_l_f_xs_ys :: nat llist -> (nat -> nat -> nat) -> (Unit -> nat llist) -> nat llist cond_zipwith_l_f_xs_ys_1 :: nat llist -> (nat -> nat -> nat) -> nat -> (Unit -> nat llist) -> nat llist fibs :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main :: nat -> nat list plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat tail_l :: (Unit -> nat llist) -> Unit -> nat llist zipwith_l :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l#3 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys#1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 21: Compression MAYBE + Considered Problem: 1: fibs_2#1(zipwith_l(), plus(), tail_l(), x3) -> ConsL(S(0()), zipwith_l#3(plus(), fibs(zipwith_l(), plus() , tail_l()) , cond_tail_l_xs(fibs#1(zipwith_l() , plus() , tail_l() , bot[2]())))) 2: fibs#1(zipwith_l(), plus(), tail_l(), x1) -> ConsL(0(), fibs_2(zipwith_l(), plus(), tail_l())) 3: cond_take_l_n_xs(ConsL(x12, x14), 0()) -> Nil() 4: 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)) 5: 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)) 6: cond_tail_l_xs(ConsL(0(), fibs_2(x1, x2, x3))) -> fibs_2(x1, x2, x3) 7: plus#2(0(), x12) -> x12 8: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 9: cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), plus(), x2, x1) -> ConsL(plus#2(x2, x4), zipwith_l#3(plus(), x1 , x3)) 10: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), 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[3]()), plus(), x5, x4) 11: cond_zipwith_l_f_xs_ys(ConsL(x5, x4), plus(), fibs_2(x1, x2, x3)) -> cond_zipwith_l_f_xs_ys_1(fibs_2#1(x1, x2, x3, bot[3]()), plus(), x5, x4) 12: zipwith_l_f_xs_ys#1(plus(), fibs(x3, x4, x5), x2, x1) -> cond_zipwith_l_f_xs_ys(fibs#1(x3, x4 , x5 , bot[4]()), plus() , x2) 13: 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[4]()) , plus(), x2) 14: 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[4]()), plus(), x2) 15: zipwith_l#3(plus(), x4, x2) -> zipwith_l_f_xs_ys(plus(), x4, x2) 16: main(x4) -> cond_take_l_n_xs(fibs#1(zipwith_l(), plus(), tail_l(), bot[0]()), x4) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a llist) -> 'a llist Nil :: 'a list S :: nat -> nat bot[0] :: Unit bot[2] :: Unit bot[3] :: Unit bot[4] :: Unit cond_tail_l_xs :: nat llist -> Unit -> nat llist cond_take_l_n_xs :: nat llist -> nat -> nat list cond_zipwith_l_f_xs_ys :: nat llist -> (nat -> nat -> nat) -> (Unit -> nat llist) -> nat llist cond_zipwith_l_f_xs_ys_1 :: nat llist -> (nat -> nat -> nat) -> nat -> (Unit -> nat llist) -> nat llist fibs :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main :: nat -> nat list plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat tail_l :: (Unit -> nat llist) -> Unit -> nat llist zipwith_l :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l#3 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys#1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist + Applied Processor: Compression + Details: none * Step 22: ToTctProblem MAYBE + Considered Problem: 1: fibs_2#1(zipwith_l(), plus(), tail_l(), x3) -> ConsL(S(0()), zipwith_l#3(fibs(zipwith_l(), plus() , tail_l()) , cond_tail_l_xs(fibs#1(zipwith_l() , plus() , tail_l() , bot[2]())))) 2: fibs#1(zipwith_l(), plus(), tail_l(), x1) -> ConsL(0(), fibs_2(zipwith_l(), plus(), tail_l())) 3: cond_take_l_n_xs(ConsL(x12, x14), 0()) -> Nil() 4: 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)) 5: 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)) 6: cond_tail_l_xs(ConsL(0(), fibs_2(x1, x2, x3))) -> fibs_2(x1, x2, x3) 7: plus#2(0(), x12) -> x12 8: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 9: cond_zipwith_l_f_xs_ys_1(ConsL(x4, x3), x2, x1) -> ConsL(plus#2(x2, x4), zipwith_l#3(x1, x3)) 10: 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[3]()), x5, x4) 11: 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[3]()) , x5, x4) 12: zipwith_l_f_xs_ys#1(plus(), fibs(x3, x4, x5), x2, x1) -> cond_zipwith_l_f_xs_ys(fibs#1(x3, x4 , x5 , bot[4]()), x2) 13: 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[4]()), x2) 14: 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[4]()), x2) 15: zipwith_l#3(x4, x2) -> zipwith_l_f_xs_ys(plus(), x4, x2) 16: main(x4) -> cond_take_l_n_xs(fibs#1(zipwith_l(), plus(), tail_l(), bot[0]()), x4) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a llist) -> 'a llist Nil :: 'a list S :: nat -> nat bot[0] :: Unit bot[2] :: Unit bot[3] :: Unit bot[4] :: Unit cond_tail_l_xs :: nat llist -> Unit -> nat llist cond_take_l_n_xs :: nat llist -> nat -> nat list cond_zipwith_l_f_xs_ys :: nat llist -> (Unit -> nat llist) -> nat llist cond_zipwith_l_f_xs_ys_1 :: nat llist -> nat -> (Unit -> nat llist) -> nat llist fibs :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist fibs_2#1 :: ((nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist) -> (nat -> nat -> nat) -> ((Unit -> nat llist) -> Unit -> nat llist) -> Unit -> nat llist main :: nat -> nat list plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat tail_l :: (Unit -> nat llist) -> Unit -> nat llist zipwith_l :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l#3 :: (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist zipwith_l_f_xs_ys#1 :: (nat -> nat -> nat) -> (Unit -> nat llist) -> (Unit -> nat llist) -> Unit -> nat llist + Applied Processor: ToTctProblem + Details: none * Step 23: Failure MAYBE timed out MAYBE