MAYBE * Step 1: Desugar MAYBE + Considered Problem: type 'a list = Nil | Cons of 'a * 'a list ;; type nat = 0 | S of nat ;; type 'a option = None | Some of 'a ;; let rec plus x y = match x with | 0 -> y | S(x') -> S(plus x' y) ;; let rec mult x y = match x with | 0 -> 0 | S(x') -> plus y (mult x' y) ;; let square x = mult x x ;; let rec unfoldr f z = match f z with | None -> Nil | Some(z') -> Cons(z',unfoldr f z') ;; let countdown m = match m with | 0 -> None | S(m') -> Some(m') ;; let enum n = match n with | 0 -> Nil | S(n') -> Cons(n, unfoldr countdown n) ;; let rec map f xs = match xs with | Nil -> Nil | Cons(x,xs') -> Cons(f x, map f xs') ;; let rec sum xs = match xs with | Nil -> 0 | Cons(x,xs') -> plus x (sum xs') ;; let sum_sqs n = sum (map square (enum n)) ;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization MAYBE + Considered Problem: λn : nat. (λplus : nat -> nat -> nat. (λmult : nat -> nat -> nat. (λsquare : nat -> nat. (λunfoldr : (nat -> nat option) -> nat -> nat list. (λcountdown : nat -> nat option. (λenum : nat -> nat list. (λmap : (nat -> nat) -> nat list -> nat list. (λsum : nat list -> nat. (λsum_sqs : nat -> nat. sum_sqs n) (λn : nat. sum (map square (enum n)))) (μsum : nat list -> nat. λxs : nat list. case xs of | Nil -> 0 | Cons -> λx : nat. λxs' : nat list. plus x (sum xs'))) (μmap : (nat -> nat) -> nat list -> nat list. λf : nat -> nat. λxs : nat list. case xs of | Nil -> Nil | Cons -> λx : nat. λxs' : nat list. Cons(f x,map f xs'))) (λn : nat. case n of | 0 -> Nil | S -> λn' : nat. Cons(n,unfoldr countdown n))) (λm : nat. case m of | 0 -> None | S -> λm' : nat. Some(m'))) (μunfoldr : (nat -> nat option) -> nat -> nat list. λf : nat -> nat option. λz : nat. case f z of | None -> Nil | Some -> λz' : nat. Cons(z',unfoldr f z'))) (λx : nat. mult x x)) (μmult : nat -> nat -> nat. λx : nat. λy : nat. case x of | 0 -> 0 | S -> λx' : nat. plus y (mult x' y))) (μplus : nat -> nat -> nat. λx : nat. λy : nat. case x of | 0 -> y | S -> λx' : nat. S(plus x' y)) : nat -> nat where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list None :: 'a option S :: nat -> nat Some :: 'a -> 'a option + Applied Processor: Defunctionalization + Details: none * Step 3: Inline MAYBE + Considered Problem: 1: main_9(x0) x9 -> x9 x0 2: sum_sqs(x3, x6, x7, x8) x9 -> x8 (x7 x3 (x6 x9)) 3: main_8(x0, x3, x6, x7) x8 -> main_9(x0) sum_sqs(x3, x6, x7, x8) 4: cond_sum_xs(Nil(), x1) -> 0() 5: cond_sum_xs(Cons(x9, x10), x1) -> x1 x9 (sum(x1) x10) 6: sum_1(x1) x8 -> cond_sum_xs(x8, x1) 7: sum(x1) x2 -> sum_1(x1) x2 8: main_7(x0, x1, x3, x6) x7 -> main_8(x0, x3, x6, x7) sum(x1) 9: cond_map_f_xs(Nil(), x7) -> Nil() 10: cond_map_f_xs(Cons(x9, x10), x7) -> Cons(x7 x9, map() x7 x10) 11: map_f(x7) x8 -> cond_map_f_xs(x8, x7) 12: map_1() x7 -> map_f(x7) 13: map() x0 -> map_1() x0 14: main_6(x0, x1, x3) x6 -> main_7(x0, x1, x3, x6) map() 15: cond_enum_n(0(), x4, x5, x6) -> Nil() 16: cond_enum_n(S(x7), x4, x5, x6) -> Cons(x6, x4 x5 x6) 17: enum(x4, x5) x6 -> cond_enum_n(x6, x4, x5, x6) 18: main_5(x0, x1, x3, x4) x5 -> main_6(x0, x1, x3) enum(x4, x5) 19: cond_countdown_m(0()) -> None() 20: cond_countdown_m(S(x6)) -> Some(x6) 21: countdown() x5 -> cond_countdown_m(x5) 22: main_4(x0, x1, x3) x4 -> main_5(x0, x1, x3, x4) countdown() 23: cond_unfoldr_f_z(None(), x4) -> Nil() 24: cond_unfoldr_f_z(Some(x6), x4) -> Cons(x6, unfoldr() x4 x6) 25: unfoldr_f(x4) x5 -> cond_unfoldr_f_z(x4 x5, x4) 26: unfoldr_1() x4 -> unfoldr_f(x4) 27: unfoldr() x0 -> unfoldr_1() x0 28: main_3(x0, x1) x3 -> main_4(x0, x1, x3) unfoldr() 29: square(x2) x3 -> x2 x3 x3 30: main_2(x0, x1) x2 -> main_3(x0, x1) square(x2) 31: cond_mult_x_y(0(), x1, x3) -> 0() 32: cond_mult_x_y(S(x4), x1, x3) -> x1 x3 (mult(x1) x4 x3) 33: mult_x(x1, x2) x3 -> cond_mult_x_y(x2, x1, x3) 34: mult_1(x1) x2 -> mult_x(x1, x2) 35: mult(x1) x2 -> mult_1(x1) x2 36: main_1(x0) x1 -> main_2(x0, x1) mult(x1) 37: cond_plus_x_y(0(), x2) -> x2 38: cond_plus_x_y(S(x3), x2) -> S(plus() x3 x2) 39: plus_x(x1) x2 -> cond_plus_x_y(x1, x2) 40: plus_1() x1 -> plus_x(x1) 41: plus() x0 -> plus_1() x0 42: main(x0) -> main_1(x0) plus() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list None :: 'a option S :: nat -> nat Some :: 'a -> 'a option countdown :: nat -> nat option enum :: ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat -> nat list map_f :: (nat -> nat) -> nat list -> nat list unfoldr_f :: (nat -> nat option) -> nat -> nat list square :: (nat -> nat -> nat) -> nat -> nat sum_sqs :: (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> (nat list -> nat) -> nat -> nat mult_x :: (nat -> nat -> nat) -> nat -> nat -> nat plus_x :: nat -> nat -> nat main_1 :: nat -> (nat -> nat -> nat) -> nat map_1 :: (nat -> nat) -> nat list -> nat list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat sum_1 :: (nat -> nat -> nat) -> nat list -> nat unfoldr_1 :: (nat -> nat option) -> nat -> nat list main_2 :: nat -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> nat main_4 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> ((nat -> nat option) -> nat -> nat list) -> nat main_5 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat main_6 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> (nat -> nat list) -> nat main_7 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> nat main_8 :: nat -> (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> (nat list -> nat) -> nat main_9 :: nat -> (nat -> nat) -> nat cond_countdown_m :: nat -> nat option cond_enum_n :: nat -> ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat -> nat list cond_map_f_xs :: nat list -> (nat -> nat) -> nat list cond_sum_xs :: nat list -> (nat -> nat -> nat) -> nat cond_mult_x_y :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_x_y :: nat -> nat -> nat cond_unfoldr_f_z :: nat option -> (nat -> nat option) -> nat list map :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat sum :: (nat -> nat -> nat) -> nat list -> nat unfoldr :: (nat -> nat option) -> nat -> nat list main :: nat -> nat + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline MAYBE + Considered Problem: 1: main_9(x0) x9 -> x9 x0 2: sum_sqs(x3, x6, x7, x8) x9 -> x8 (x7 x3 (x6 x9)) 3: main_8(x0, x7, x13, x15) x17 -> sum_sqs(x7, x13, x15, x17) x0 4: cond_sum_xs(Nil(), x1) -> 0() 5: cond_sum_xs(Cons(x9, x10), x1) -> x1 x9 (sum(x1) x10) 6: sum_1(x1) x8 -> cond_sum_xs(x8, x1) 7: sum(x2) x16 -> cond_sum_xs(x16, x2) 8: main_7(x0, x3, x6, x12) x14 -> main_9(x0) sum_sqs(x6, x12, x14, sum(x3)) 9: cond_map_f_xs(Nil(), x7) -> Nil() 10: cond_map_f_xs(Cons(x9, x10), x7) -> Cons(x7 x9, map() x7 x10) 11: map_f(x7) x8 -> cond_map_f_xs(x8, x7) 12: map_1() x7 -> map_f(x7) 13: map() x14 -> map_f(x14) 14: main_6(x0, x2, x6) x12 -> main_8(x0, x6, x12, map()) sum(x2) 15: cond_enum_n(0(), x4, x5, x6) -> Nil() 16: cond_enum_n(S(x7), x4, x5, x6) -> Cons(x6, x4 x5 x6) 17: enum(x4, x5) x6 -> cond_enum_n(x6, x4, x5, x6) 18: main_5(x0, x2, x6, x9) x11 -> main_7(x0, x2, x6, enum(x9, x11)) map() 19: cond_countdown_m(0()) -> None() 20: cond_countdown_m(S(x6)) -> Some(x6) 21: countdown() x5 -> cond_countdown_m(x5) 22: main_4(x0, x2, x6) x8 -> main_6(x0, x2, x6) enum(x8, countdown()) 23: cond_unfoldr_f_z(None(), x4) -> Nil() 24: cond_unfoldr_f_z(Some(x6), x4) -> Cons(x6, unfoldr() x4 x6) 25: unfoldr_f(x4) x5 -> cond_unfoldr_f_z(x4 x5, x4) 26: unfoldr_1() x4 -> unfoldr_f(x4) 27: unfoldr() x8 -> unfoldr_f(x8) 28: main_3(x0, x2) x6 -> main_5(x0, x2, x6, unfoldr()) countdown() 29: square(x2) x3 -> x2 x3 x3 30: main_2(x0, x2) x5 -> main_4(x0, x2, square(x5)) unfoldr() 31: cond_mult_x_y(0(), x1, x3) -> 0() 32: cond_mult_x_y(S(x4), x1, x3) -> x1 x3 (mult(x1) x4 x3) 33: mult_x(x1, x2) x3 -> cond_mult_x_y(x2, x1, x3) 34: mult_1(x1) x2 -> mult_x(x1, x2) 35: mult(x2) x4 -> mult_x(x2, x4) 36: main_1(x0) x2 -> main_3(x0, x2) square(mult(x2)) 37: cond_plus_x_y(0(), x2) -> x2 38: cond_plus_x_y(S(x3), x2) -> S(plus() x3 x2) 39: plus_x(x1) x2 -> cond_plus_x_y(x1, x2) 40: plus_1() x1 -> plus_x(x1) 41: plus() x2 -> plus_x(x2) 42: main(x0) -> main_2(x0, plus()) mult(plus()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list None :: 'a option S :: nat -> nat Some :: 'a -> 'a option countdown :: nat -> nat option enum :: ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat -> nat list map_f :: (nat -> nat) -> nat list -> nat list unfoldr_f :: (nat -> nat option) -> nat -> nat list square :: (nat -> nat -> nat) -> nat -> nat sum_sqs :: (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> (nat list -> nat) -> nat -> nat mult_x :: (nat -> nat -> nat) -> nat -> nat -> nat plus_x :: nat -> nat -> nat main_1 :: nat -> (nat -> nat -> nat) -> nat map_1 :: (nat -> nat) -> nat list -> nat list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat sum_1 :: (nat -> nat -> nat) -> nat list -> nat unfoldr_1 :: (nat -> nat option) -> nat -> nat list main_2 :: nat -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> nat main_4 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> ((nat -> nat option) -> nat -> nat list) -> nat main_5 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat main_6 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> (nat -> nat list) -> nat main_7 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> nat main_8 :: nat -> (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> (nat list -> nat) -> nat main_9 :: nat -> (nat -> nat) -> nat cond_countdown_m :: nat -> nat option cond_enum_n :: nat -> ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat -> nat list cond_map_f_xs :: nat list -> (nat -> nat) -> nat list cond_sum_xs :: nat list -> (nat -> nat -> nat) -> nat cond_mult_x_y :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_x_y :: nat -> nat -> nat cond_unfoldr_f_z :: nat option -> (nat -> nat option) -> nat list map :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat sum :: (nat -> nat -> nat) -> nat list -> nat unfoldr :: (nat -> nat option) -> nat -> nat list main :: nat -> nat + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 5: Inline MAYBE + Considered Problem: 1: main_9(x0) x9 -> x9 x0 2: sum_sqs(x3, x6, x7, x8) x9 -> x8 (x7 x3 (x6 x9)) 3: main_8(x18, x6, x12, x14) x16 -> x16 (x14 x6 (x12 x18)) 4: cond_sum_xs(Nil(), x1) -> 0() 5: cond_sum_xs(Cons(x9, x10), x1) -> x1 x9 (sum(x1) x10) 6: sum_1(x1) x8 -> cond_sum_xs(x8, x1) 7: sum(x2) x16 -> cond_sum_xs(x16, x2) 8: main_7(x0, x7, x13, x25) x29 -> sum_sqs(x13, x25, x29, sum(x7)) x0 9: cond_map_f_xs(Nil(), x7) -> Nil() 10: cond_map_f_xs(Cons(x9, x10), x7) -> Cons(x7 x9, map() x7 x10) 11: map_f(x7) x8 -> cond_map_f_xs(x8, x7) 12: map_1() x7 -> map_f(x7) 13: map() x14 -> map_f(x14) 14: main_6(x0, x5, x14) x26 -> sum_sqs(x14, x26, map(), sum(x5)) x0 15: cond_enum_n(0(), x4, x5, x6) -> Nil() 16: cond_enum_n(S(x7), x4, x5, x6) -> Cons(x6, x4 x5 x6) 17: enum(x4, x5) x6 -> cond_enum_n(x6, x4, x5, x6) 18: main_5(x0, x6, x12, x19) x23 -> main_9(x0) sum_sqs(x12, enum(x19, x23), map(), sum(x6)) 19: cond_countdown_m(0()) -> None() 20: cond_countdown_m(S(x6)) -> Some(x6) 21: countdown() x5 -> cond_countdown_m(x5) 22: main_4(x0, x4, x12) x17 -> main_8(x0, x12, enum(x17, countdown()), map()) sum(x4) 23: cond_unfoldr_f_z(None(), x4) -> Nil() 24: cond_unfoldr_f_z(Some(x6), x4) -> Cons(x6, unfoldr() x4 x6) 25: unfoldr_f(x4) x5 -> cond_unfoldr_f_z(x4 x5, x4) 26: unfoldr_1() x4 -> unfoldr_f(x4) 27: unfoldr() x8 -> unfoldr_f(x8) 28: main_3(x0, x4) x12 -> main_7(x0, x4, x12, enum(unfoldr(), countdown())) map() 29: square(x2) x3 -> x2 x3 x3 30: main_2(x0, x4) x11 -> main_6(x0, x4, square(x11)) enum(unfoldr(), countdown()) 31: cond_mult_x_y(0(), x1, x3) -> 0() 32: cond_mult_x_y(S(x4), x1, x3) -> x1 x3 (mult(x1) x4 x3) 33: mult_x(x1, x2) x3 -> cond_mult_x_y(x2, x1, x3) 34: mult_1(x1) x2 -> mult_x(x1, x2) 35: mult(x2) x4 -> mult_x(x2, x4) 36: main_1(x0) x4 -> main_5(x0, x4, square(mult(x4)), unfoldr()) countdown() 37: cond_plus_x_y(0(), x2) -> x2 38: cond_plus_x_y(S(x3), x2) -> S(plus() x3 x2) 39: plus_x(x1) x2 -> cond_plus_x_y(x1, x2) 40: plus_1() x1 -> plus_x(x1) 41: plus() x2 -> plus_x(x2) 42: main(x0) -> main_4(x0, plus(), square(mult(plus()))) unfoldr() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list None :: 'a option S :: nat -> nat Some :: 'a -> 'a option countdown :: nat -> nat option enum :: ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat -> nat list map_f :: (nat -> nat) -> nat list -> nat list unfoldr_f :: (nat -> nat option) -> nat -> nat list square :: (nat -> nat -> nat) -> nat -> nat sum_sqs :: (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> (nat list -> nat) -> nat -> nat mult_x :: (nat -> nat -> nat) -> nat -> nat -> nat plus_x :: nat -> nat -> nat main_1 :: nat -> (nat -> nat -> nat) -> nat map_1 :: (nat -> nat) -> nat list -> nat list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat sum_1 :: (nat -> nat -> nat) -> nat list -> nat unfoldr_1 :: (nat -> nat option) -> nat -> nat list main_2 :: nat -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> nat main_4 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> ((nat -> nat option) -> nat -> nat list) -> nat main_5 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat main_6 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> (nat -> nat list) -> nat main_7 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> nat main_8 :: nat -> (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> (nat list -> nat) -> nat main_9 :: nat -> (nat -> nat) -> nat cond_countdown_m :: nat -> nat option cond_enum_n :: nat -> ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat -> nat list cond_map_f_xs :: nat list -> (nat -> nat) -> nat list cond_sum_xs :: nat list -> (nat -> nat -> nat) -> nat cond_mult_x_y :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_x_y :: nat -> nat -> nat cond_unfoldr_f_z :: nat option -> (nat -> nat option) -> nat list map :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat sum :: (nat -> nat -> nat) -> nat list -> nat unfoldr :: (nat -> nat option) -> nat -> nat list main :: nat -> nat + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 6: Inline MAYBE + Considered Problem: 1: main_9(x0) x9 -> x9 x0 2: sum_sqs(x3, x6, x7, x8) x9 -> x8 (x7 x3 (x6 x9)) 3: main_8(x18, x6, x12, x14) x16 -> x16 (x14 x6 (x12 x18)) 4: cond_sum_xs(Nil(), x1) -> 0() 5: cond_sum_xs(Cons(x9, x10), x1) -> x1 x9 (sum(x1) x10) 6: sum_1(x1) x8 -> cond_sum_xs(x8, x1) 7: sum(x2) x16 -> cond_sum_xs(x16, x2) 8: main_7(x18, x15, x6, x12) x14 -> sum(x15) (x14 x6 (x12 x18)) 9: cond_map_f_xs(Nil(), x7) -> Nil() 10: cond_map_f_xs(Cons(x9, x10), x7) -> Cons(x7 x9, map() x7 x10) 11: map_f(x7) x8 -> cond_map_f_xs(x8, x7) 12: map_1() x7 -> map_f(x7) 13: map() x14 -> map_f(x14) 14: main_6(x18, x11, x6) x12 -> sum(x11) (map() x6 (x12 x18)) 15: cond_enum_n(0(), x4, x5, x6) -> Nil() 16: cond_enum_n(S(x7), x4, x5, x6) -> Cons(x6, x4 x5 x6) 17: enum(x4, x5) x6 -> cond_enum_n(x6, x4, x5, x6) 18: main_5(x0, x13, x25, x39) x47 -> sum_sqs(x25, enum(x39, x47), map(), sum(x13)) x0 19: cond_countdown_m(0()) -> None() 20: cond_countdown_m(S(x6)) -> Some(x6) 21: countdown() x5 -> cond_countdown_m(x5) 22: main_4(x36, x9, x12) x35 -> sum(x9) (map() x12 (enum(x35, countdown()) x36)) 23: cond_unfoldr_f_z(None(), x4) -> Nil() 24: cond_unfoldr_f_z(Some(x6), x4) -> Cons(x6, unfoldr() x4 x6) 25: unfoldr_f(x4) x5 -> cond_unfoldr_f_z(x4 x5, x4) 26: unfoldr_1() x4 -> unfoldr_f(x4) 27: unfoldr() x8 -> unfoldr_f(x8) 28: main_3(x0, x14) x26 -> sum_sqs(x26, enum(unfoldr(), countdown()), map(), sum(x14)) x0 29: square(x2) x3 -> x2 x3 x3 30: main_2(x0, x10) x23 -> sum_sqs(square(x23), enum(unfoldr(), countdown()), map(), sum(x10)) x0 31: cond_mult_x_y(0(), x1, x3) -> 0() 32: cond_mult_x_y(S(x4), x1, x3) -> x1 x3 (mult(x1) x4 x3) 33: mult_x(x1, x2) x3 -> cond_mult_x_y(x2, x1, x3) 34: mult_1(x1) x2 -> mult_x(x1, x2) 35: mult(x2) x4 -> mult_x(x2, x4) 36: main_1(x0) x12 -> main_9(x0) sum_sqs(square(mult(x12)), enum(unfoldr(), countdown()), map(), sum(x12)) 37: cond_plus_x_y(0(), x2) -> x2 38: cond_plus_x_y(S(x3), x2) -> S(plus() x3 x2) 39: plus_x(x1) x2 -> cond_plus_x_y(x1, x2) 40: plus_1() x1 -> plus_x(x1) 41: plus() x2 -> plus_x(x2) 42: main(x0) -> main_8(x0, square(mult(plus())), enum(unfoldr(), countdown()), map()) sum(plus()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list None :: 'a option S :: nat -> nat Some :: 'a -> 'a option countdown :: nat -> nat option enum :: ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat -> nat list map_f :: (nat -> nat) -> nat list -> nat list unfoldr_f :: (nat -> nat option) -> nat -> nat list square :: (nat -> nat -> nat) -> nat -> nat sum_sqs :: (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> (nat list -> nat) -> nat -> nat mult_x :: (nat -> nat -> nat) -> nat -> nat -> nat plus_x :: nat -> nat -> nat main_1 :: nat -> (nat -> nat -> nat) -> nat map_1 :: (nat -> nat) -> nat list -> nat list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat sum_1 :: (nat -> nat -> nat) -> nat list -> nat unfoldr_1 :: (nat -> nat option) -> nat -> nat list main_2 :: nat -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> nat main_4 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> ((nat -> nat option) -> nat -> nat list) -> nat main_5 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat main_6 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> (nat -> nat list) -> nat main_7 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> nat main_8 :: nat -> (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> (nat list -> nat) -> nat main_9 :: nat -> (nat -> nat) -> nat cond_countdown_m :: nat -> nat option cond_enum_n :: nat -> ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat -> nat list cond_map_f_xs :: nat list -> (nat -> nat) -> nat list cond_sum_xs :: nat list -> (nat -> nat -> nat) -> nat cond_mult_x_y :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_x_y :: nat -> nat -> nat cond_unfoldr_f_z :: nat option -> (nat -> nat option) -> nat list map :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat sum :: (nat -> nat -> nat) -> nat list -> nat unfoldr :: (nat -> nat option) -> nat -> nat list main :: nat -> nat + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 7: Inline MAYBE + Considered Problem: 1: main_9(x0) x9 -> x9 x0 2: sum_sqs(x3, x6, x7, x8) x9 -> x8 (x7 x3 (x6 x9)) 3: main_8(x18, x6, x12, x14) x16 -> x16 (x14 x6 (x12 x18)) 4: cond_sum_xs(Nil(), x1) -> 0() 5: cond_sum_xs(Cons(x9, x10), x1) -> x1 x9 (sum(x1) x10) 6: sum_1(x1) x8 -> cond_sum_xs(x8, x1) 7: sum(x2) x16 -> cond_sum_xs(x16, x2) 8: main_7(x18, x15, x6, x12) x14 -> sum(x15) (x14 x6 (x12 x18)) 9: cond_map_f_xs(Nil(), x7) -> Nil() 10: cond_map_f_xs(Cons(x9, x10), x7) -> Cons(x7 x9, map() x7 x10) 11: map_f(x7) x8 -> cond_map_f_xs(x8, x7) 12: map_1() x7 -> map_f(x7) 13: map() x14 -> map_f(x14) 14: main_6(x18, x11, x6) x12 -> sum(x11) (map() x6 (x12 x18)) 15: cond_enum_n(0(), x4, x5, x6) -> Nil() 16: cond_enum_n(S(x7), x4, x5, x6) -> Cons(x6, x4 x5 x6) 17: enum(x4, x5) x6 -> cond_enum_n(x6, x4, x5, x6) 18: main_5(x18, x27, x6, x79) x95 -> sum(x27) (map() x6 (enum(x79, x95) x18)) 19: cond_countdown_m(0()) -> None() 20: cond_countdown_m(S(x6)) -> Some(x6) 21: countdown() x5 -> cond_countdown_m(x5) 22: main_4(x12, x19, x25) x8 -> sum(x19) (map() x25 cond_enum_n(x12, x8, countdown(), x12)) 23: cond_unfoldr_f_z(None(), x4) -> Nil() 24: cond_unfoldr_f_z(Some(x6), x4) -> Cons(x6, unfoldr() x4 x6) 25: unfoldr_f(x4) x5 -> cond_unfoldr_f_z(x4 x5, x4) 26: unfoldr_1() x4 -> unfoldr_f(x4) 27: unfoldr() x8 -> unfoldr_f(x8) 28: main_3(x18, x29) x6 -> sum(x29) (map() x6 (enum(unfoldr(), countdown()) x18)) 29: square(x2) x3 -> x2 x3 x3 30: main_2(x18, x21) x47 -> sum(x21) (map() square(x47) (enum(unfoldr(), countdown()) x18)) 31: cond_mult_x_y(0(), x1, x3) -> 0() 32: cond_mult_x_y(S(x4), x1, x3) -> x1 x3 (mult(x1) x4 x3) 33: mult_x(x1, x2) x3 -> cond_mult_x_y(x2, x1, x3) 34: mult_1(x1) x2 -> mult_x(x1, x2) 35: mult(x2) x4 -> mult_x(x2, x4) 36: main_1(x0) x25 -> sum_sqs(square(mult(x25)), enum(unfoldr(), countdown()), map(), sum(x25)) x0 37: cond_plus_x_y(0(), x2) -> x2 38: cond_plus_x_y(S(x3), x2) -> S(plus() x3 x2) 39: plus_x(x1) x2 -> cond_plus_x_y(x1, x2) 40: plus_1() x1 -> plus_x(x1) 41: plus() x2 -> plus_x(x2) 42: main(x36) -> sum(plus()) (map() square(mult(plus())) (enum(unfoldr(), countdown()) x36)) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list None :: 'a option S :: nat -> nat Some :: 'a -> 'a option countdown :: nat -> nat option enum :: ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat -> nat list map_f :: (nat -> nat) -> nat list -> nat list unfoldr_f :: (nat -> nat option) -> nat -> nat list square :: (nat -> nat -> nat) -> nat -> nat sum_sqs :: (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> (nat list -> nat) -> nat -> nat mult_x :: (nat -> nat -> nat) -> nat -> nat -> nat plus_x :: nat -> nat -> nat main_1 :: nat -> (nat -> nat -> nat) -> nat map_1 :: (nat -> nat) -> nat list -> nat list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat sum_1 :: (nat -> nat -> nat) -> nat list -> nat unfoldr_1 :: (nat -> nat option) -> nat -> nat list main_2 :: nat -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> nat main_4 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> ((nat -> nat option) -> nat -> nat list) -> nat main_5 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat main_6 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> (nat -> nat list) -> nat main_7 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> nat main_8 :: nat -> (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> (nat list -> nat) -> nat main_9 :: nat -> (nat -> nat) -> nat cond_countdown_m :: nat -> nat option cond_enum_n :: nat -> ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat -> nat list cond_map_f_xs :: nat list -> (nat -> nat) -> nat list cond_sum_xs :: nat list -> (nat -> nat -> nat) -> nat cond_mult_x_y :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_x_y :: nat -> nat -> nat cond_unfoldr_f_z :: nat option -> (nat -> nat option) -> nat list map :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat sum :: (nat -> nat -> nat) -> nat list -> nat unfoldr :: (nat -> nat option) -> nat -> nat list main :: nat -> nat + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 8: Inline MAYBE + Considered Problem: 1: main_9(x0) x9 -> x9 x0 2: sum_sqs(x3, x6, x7, x8) x9 -> x8 (x7 x3 (x6 x9)) 3: main_8(x18, x6, x12, x14) x16 -> x16 (x14 x6 (x12 x18)) 4: cond_sum_xs(Nil(), x1) -> 0() 5: cond_sum_xs(Cons(x9, x10), x1) -> x1 x9 (sum(x1) x10) 6: sum_1(x1) x8 -> cond_sum_xs(x8, x1) 7: sum(x2) x16 -> cond_sum_xs(x16, x2) 8: main_7(x18, x15, x6, x12) x14 -> sum(x15) (x14 x6 (x12 x18)) 9: cond_map_f_xs(Nil(), x7) -> Nil() 10: cond_map_f_xs(Cons(x9, x10), x7) -> Cons(x7 x9, map() x7 x10) 11: map_f(x7) x8 -> cond_map_f_xs(x8, x7) 12: map_1() x7 -> map_f(x7) 13: map() x14 -> map_f(x14) 14: main_6(x18, x11, x6) x12 -> sum(x11) (map() x6 (x12 x18)) 15: cond_enum_n(0(), x4, x5, x6) -> Nil() 16: cond_enum_n(S(x7), x4, x5, x6) -> Cons(x6, x4 x5 x6) 17: enum(x4, x5) x6 -> cond_enum_n(x6, x4, x5, x6) 18: main_5(x12, x55, x13, x8) x10 -> sum(x55) (map() x13 cond_enum_n(x12, x8, x10, x12)) 19: cond_countdown_m(0()) -> None() 20: cond_countdown_m(S(x6)) -> Some(x6) 21: countdown() x5 -> cond_countdown_m(x5) 22: main_4(x12, x19, x25) x8 -> sum(x19) (map() x25 cond_enum_n(x12, x8, countdown(), x12)) 23: cond_unfoldr_f_z(None(), x4) -> Nil() 24: cond_unfoldr_f_z(Some(x6), x4) -> Cons(x6, unfoldr() x4 x6) 25: unfoldr_f(x4) x5 -> cond_unfoldr_f_z(x4 x5, x4) 26: unfoldr_1() x4 -> unfoldr_f(x4) 27: unfoldr() x8 -> unfoldr_f(x8) 28: main_3(x12, x59) x13 -> sum(x59) (map() x13 cond_enum_n(x12, unfoldr(), countdown(), x12)) 29: square(x2) x3 -> x2 x3 x3 30: main_2(x12, x43) x95 -> sum(x43) (map() square(x95) cond_enum_n(x12, unfoldr(), countdown(), x12)) 31: cond_mult_x_y(0(), x1, x3) -> 0() 32: cond_mult_x_y(S(x4), x1, x3) -> x1 x3 (mult(x1) x4 x3) 33: mult_x(x1, x2) x3 -> cond_mult_x_y(x2, x1, x3) 34: mult_1(x1) x2 -> mult_x(x1, x2) 35: mult(x2) x4 -> mult_x(x2, x4) 36: main_1(x18) x51 -> sum(x51) (map() square(mult(x51)) (enum(unfoldr(), countdown()) x18)) 37: cond_plus_x_y(0(), x2) -> x2 38: cond_plus_x_y(S(x3), x2) -> S(plus() x3 x2) 39: plus_x(x1) x2 -> cond_plus_x_y(x1, x2) 40: plus_1() x1 -> plus_x(x1) 41: plus() x2 -> plus_x(x2) 42: main(x12) -> sum(plus()) (map() square(mult(plus())) cond_enum_n(x12, unfoldr(), countdown(), x12)) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list None :: 'a option S :: nat -> nat Some :: 'a -> 'a option countdown :: nat -> nat option enum :: ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat -> nat list map_f :: (nat -> nat) -> nat list -> nat list unfoldr_f :: (nat -> nat option) -> nat -> nat list square :: (nat -> nat -> nat) -> nat -> nat sum_sqs :: (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> (nat list -> nat) -> nat -> nat mult_x :: (nat -> nat -> nat) -> nat -> nat -> nat plus_x :: nat -> nat -> nat main_1 :: nat -> (nat -> nat -> nat) -> nat map_1 :: (nat -> nat) -> nat list -> nat list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat sum_1 :: (nat -> nat -> nat) -> nat list -> nat unfoldr_1 :: (nat -> nat option) -> nat -> nat list main_2 :: nat -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> nat main_4 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> ((nat -> nat option) -> nat -> nat list) -> nat main_5 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat main_6 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> (nat -> nat list) -> nat main_7 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> nat main_8 :: nat -> (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> (nat list -> nat) -> nat main_9 :: nat -> (nat -> nat) -> nat cond_countdown_m :: nat -> nat option cond_enum_n :: nat -> ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat -> nat list cond_map_f_xs :: nat list -> (nat -> nat) -> nat list cond_sum_xs :: nat list -> (nat -> nat -> nat) -> nat cond_mult_x_y :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_x_y :: nat -> nat -> nat cond_unfoldr_f_z :: nat option -> (nat -> nat option) -> nat list map :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat sum :: (nat -> nat -> nat) -> nat list -> nat unfoldr :: (nat -> nat option) -> nat -> nat list main :: nat -> nat + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 9: Inline MAYBE + Considered Problem: 1: main_9(x0) x9 -> x9 x0 2: sum_sqs(x3, x6, x7, x8) x9 -> x8 (x7 x3 (x6 x9)) 3: main_8(x18, x6, x12, x14) x16 -> x16 (x14 x6 (x12 x18)) 4: cond_sum_xs(Nil(), x1) -> 0() 5: cond_sum_xs(Cons(x9, x10), x1) -> x1 x9 (sum(x1) x10) 6: sum_1(x1) x8 -> cond_sum_xs(x8, x1) 7: sum(x2) x16 -> cond_sum_xs(x16, x2) 8: main_7(x18, x15, x6, x12) x14 -> sum(x15) (x14 x6 (x12 x18)) 9: cond_map_f_xs(Nil(), x7) -> Nil() 10: cond_map_f_xs(Cons(x9, x10), x7) -> Cons(x7 x9, map() x7 x10) 11: map_f(x7) x8 -> cond_map_f_xs(x8, x7) 12: map_1() x7 -> map_f(x7) 13: map() x14 -> map_f(x14) 14: main_6(x18, x11, x6) x12 -> sum(x11) (map() x6 (x12 x18)) 15: cond_enum_n(0(), x4, x5, x6) -> Nil() 16: cond_enum_n(S(x7), x4, x5, x6) -> Cons(x6, x4 x5 x6) 17: enum(x4, x5) x6 -> cond_enum_n(x6, x4, x5, x6) 18: main_5(x12, x55, x13, x8) x10 -> sum(x55) (map() x13 cond_enum_n(x12, x8, x10, x12)) 19: cond_countdown_m(0()) -> None() 20: cond_countdown_m(S(x6)) -> Some(x6) 21: countdown() x5 -> cond_countdown_m(x5) 22: main_4(x12, x19, x25) x8 -> sum(x19) (map() x25 cond_enum_n(x12, x8, countdown(), x12)) 23: cond_unfoldr_f_z(None(), x4) -> Nil() 24: cond_unfoldr_f_z(Some(x6), x4) -> Cons(x6, unfoldr() x4 x6) 25: unfoldr_f(x4) x5 -> cond_unfoldr_f_z(x4 x5, x4) 26: unfoldr_1() x4 -> unfoldr_f(x4) 27: unfoldr() x8 -> unfoldr_f(x8) 28: main_3(x12, x59) x13 -> sum(x59) (map() x13 cond_enum_n(x12, unfoldr(), countdown(), x12)) 29: square(x2) x3 -> x2 x3 x3 30: main_2(x12, x43) x95 -> sum(x43) (map() square(x95) cond_enum_n(x12, unfoldr(), countdown(), x12)) 31: cond_mult_x_y(0(), x1, x3) -> 0() 32: cond_mult_x_y(S(x4), x1, x3) -> x1 x3 (mult(x1) x4 x3) 33: mult_x(x1, x2) x3 -> cond_mult_x_y(x2, x1, x3) 34: mult_1(x1) x2 -> mult_x(x1, x2) 35: mult(x2) x4 -> mult_x(x2, x4) 36: main_1(x12) x103 -> sum(x103) (map() square(mult(x103)) cond_enum_n(x12, unfoldr(), countdown(), x12)) 37: cond_plus_x_y(0(), x2) -> x2 38: cond_plus_x_y(S(x3), x2) -> S(plus() x3 x2) 39: plus_x(x1) x2 -> cond_plus_x_y(x1, x2) 40: plus_1() x1 -> plus_x(x1) 41: plus() x2 -> plus_x(x2) 42: main(x12) -> sum(plus()) (map() square(mult(plus())) cond_enum_n(x12, unfoldr(), countdown(), x12)) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list None :: 'a option S :: nat -> nat Some :: 'a -> 'a option countdown :: nat -> nat option enum :: ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat -> nat list map_f :: (nat -> nat) -> nat list -> nat list unfoldr_f :: (nat -> nat option) -> nat -> nat list square :: (nat -> nat -> nat) -> nat -> nat sum_sqs :: (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> (nat list -> nat) -> nat -> nat mult_x :: (nat -> nat -> nat) -> nat -> nat -> nat plus_x :: nat -> nat -> nat main_1 :: nat -> (nat -> nat -> nat) -> nat map_1 :: (nat -> nat) -> nat list -> nat list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat sum_1 :: (nat -> nat -> nat) -> nat list -> nat unfoldr_1 :: (nat -> nat option) -> nat -> nat list main_2 :: nat -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> nat main_4 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> ((nat -> nat option) -> nat -> nat list) -> nat main_5 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat main_6 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> (nat -> nat list) -> nat main_7 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> nat main_8 :: nat -> (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> (nat list -> nat) -> nat main_9 :: nat -> (nat -> nat) -> nat cond_countdown_m :: nat -> nat option cond_enum_n :: nat -> ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat -> nat list cond_map_f_xs :: nat list -> (nat -> nat) -> nat list cond_sum_xs :: nat list -> (nat -> nat -> nat) -> nat cond_mult_x_y :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_x_y :: nat -> nat -> nat cond_unfoldr_f_z :: nat option -> (nat -> nat option) -> nat list map :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat sum :: (nat -> nat -> nat) -> nat list -> nat unfoldr :: (nat -> nat option) -> nat -> nat list main :: nat -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 10: UsableRules MAYBE + Considered Problem: 1: main_9(x0) x9 -> x9 x0 2: sum_sqs(x3, x6, x7, x8) x9 -> x8 (x7 x3 (x6 x9)) 3: main_8(x18, x6, x12, x14) x16 -> x16 (x14 x6 (x12 x18)) 4: cond_sum_xs(Nil(), x1) -> 0() 5: cond_sum_xs(Cons(x9, x10), x1) -> x1 x9 (sum(x1) x10) 6: sum_1(x2) Nil() -> 0() 7: sum_1(x2) Cons(x18, x20) -> x2 x18 (sum(x2) x20) 8: sum(x2) Nil() -> 0() 9: sum(x2) Cons(x18, x20) -> x2 x18 (sum(x2) x20) 10: main_7(x18, x15, x6, x12) x14 -> sum(x15) (x14 x6 (x12 x18)) 11: cond_map_f_xs(Nil(), x7) -> Nil() 12: cond_map_f_xs(Cons(x9, x10), x7) -> Cons(x7 x9, map() x7 x10) 13: map_f(x14) Nil() -> Nil() 14: map_f(x14) Cons(x18, x20) -> Cons(x14 x18, map() x14 x20) 15: map_1() x7 -> map_f(x7) 16: map() x14 -> map_f(x14) 17: main_6(x18, x11, x6) x12 -> sum(x11) (map() x6 (x12 x18)) 18: cond_enum_n(0(), x4, x5, x6) -> Nil() 19: cond_enum_n(S(x7), x4, x5, x6) -> Cons(x6, x4 x5 x6) 20: enum(x8, x10) 0() -> Nil() 21: enum(x8, x10) S(x14) -> Cons(S(x14), x8 x10 S(x14)) 22: main_5(0(), x111, x27, x8) x10 -> sum(x111) (map() x27 Nil()) 23: main_5(S(x14), x111, x27, x8) x10 -> sum(x111) (map() x27 Cons(S(x14), x8 x10 S(x14))) 24: cond_countdown_m(0()) -> None() 25: cond_countdown_m(S(x6)) -> Some(x6) 26: countdown() 0() -> None() 27: countdown() S(x12) -> Some(x12) 28: main_4(0(), x39, x51) x8 -> sum(x39) (map() x51 Nil()) 29: main_4(S(x14), x39, x51) x8 -> sum(x39) (map() x51 Cons(S(x14), x8 countdown() S(x14))) 30: cond_unfoldr_f_z(None(), x4) -> Nil() 31: cond_unfoldr_f_z(Some(x6), x4) -> Cons(x6, unfoldr() x4 x6) 32: unfoldr_f(x4) x5 -> cond_unfoldr_f_z(x4 x5, x4) 33: unfoldr_1() x4 -> unfoldr_f(x4) 34: unfoldr() x8 -> unfoldr_f(x8) 35: main_3(0(), x119) x27 -> sum(x119) (map() x27 Nil()) 36: main_3(S(x14), x119) x27 -> sum(x119) (map() x27 Cons(S(x14), unfoldr() countdown() S(x14))) 37: square(x2) x3 -> x2 x3 x3 38: main_2(0(), x87) x191 -> sum(x87) (map() square(x191) Nil()) 39: main_2(S(x14), x87) x191 -> sum(x87) (map() square(x191) Cons(S(x14), unfoldr() countdown() S(x14))) 40: cond_mult_x_y(0(), x1, x3) -> 0() 41: cond_mult_x_y(S(x4), x1, x3) -> x1 x3 (mult(x1) x4 x3) 42: mult_x(x2, 0()) x6 -> 0() 43: mult_x(x2, S(x8)) x6 -> x2 x6 (mult(x2) x8 x6) 44: mult_1(x1) x2 -> mult_x(x1, x2) 45: mult(x2) x4 -> mult_x(x2, x4) 46: main_1(0()) x207 -> sum(x207) (map() square(mult(x207)) Nil()) 47: main_1(S(x14)) x207 -> sum(x207) (map() square(mult(x207)) Cons(S(x14), unfoldr() countdown() S(x14))) 48: cond_plus_x_y(0(), x2) -> x2 49: cond_plus_x_y(S(x3), x2) -> S(plus() x3 x2) 50: plus_x(0()) x4 -> x4 51: plus_x(S(x6)) x4 -> S(plus() x6 x4) 52: plus_1() x1 -> plus_x(x1) 53: plus() x2 -> plus_x(x2) 54: main(0()) -> sum(plus()) (map() square(mult(plus())) Nil()) 55: main(S(x14)) -> sum(plus()) (map() square(mult(plus())) Cons(S(x14), unfoldr() countdown() S(x14))) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list None :: 'a option S :: nat -> nat Some :: 'a -> 'a option countdown :: nat -> nat option enum :: ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat -> nat list map_f :: (nat -> nat) -> nat list -> nat list unfoldr_f :: (nat -> nat option) -> nat -> nat list square :: (nat -> nat -> nat) -> nat -> nat sum_sqs :: (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> (nat list -> nat) -> nat -> nat mult_x :: (nat -> nat -> nat) -> nat -> nat -> nat plus_x :: nat -> nat -> nat main_1 :: nat -> (nat -> nat -> nat) -> nat map_1 :: (nat -> nat) -> nat list -> nat list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat sum_1 :: (nat -> nat -> nat) -> nat list -> nat unfoldr_1 :: (nat -> nat option) -> nat -> nat list main_2 :: nat -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> nat main_4 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> ((nat -> nat option) -> nat -> nat list) -> nat main_5 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat main_6 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> (nat -> nat list) -> nat main_7 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> nat main_8 :: nat -> (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> (nat list -> nat) -> nat main_9 :: nat -> (nat -> nat) -> nat cond_countdown_m :: nat -> nat option cond_enum_n :: nat -> ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat -> nat list cond_map_f_xs :: nat list -> (nat -> nat) -> nat list cond_sum_xs :: nat list -> (nat -> nat -> nat) -> nat cond_mult_x_y :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_x_y :: nat -> nat -> nat cond_unfoldr_f_z :: nat option -> (nat -> nat option) -> nat list map :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat sum :: (nat -> nat -> nat) -> nat list -> nat unfoldr :: (nat -> nat option) -> nat -> nat list main :: nat -> nat + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 11: NeededRules MAYBE + Considered Problem: 1: main_9(x0) x9 -> x9 x0 2: sum_sqs(x3, x6, x7, x8) x9 -> x8 (x7 x3 (x6 x9)) 3: main_8(x18, x6, x12, x14) x16 -> x16 (x14 x6 (x12 x18)) 6: sum_1(x2) Nil() -> 0() 7: sum_1(x2) Cons(x18, x20) -> x2 x18 (sum(x2) x20) 8: sum(x2) Nil() -> 0() 9: sum(x2) Cons(x18, x20) -> x2 x18 (sum(x2) x20) 10: main_7(x18, x15, x6, x12) x14 -> sum(x15) (x14 x6 (x12 x18)) 13: map_f(x14) Nil() -> Nil() 14: map_f(x14) Cons(x18, x20) -> Cons(x14 x18, map() x14 x20) 15: map_1() x7 -> map_f(x7) 16: map() x14 -> map_f(x14) 17: main_6(x18, x11, x6) x12 -> sum(x11) (map() x6 (x12 x18)) 20: enum(x8, x10) 0() -> Nil() 21: enum(x8, x10) S(x14) -> Cons(S(x14), x8 x10 S(x14)) 22: main_5(0(), x111, x27, x8) x10 -> sum(x111) (map() x27 Nil()) 23: main_5(S(x14), x111, x27, x8) x10 -> sum(x111) (map() x27 Cons(S(x14), x8 x10 S(x14))) 26: countdown() 0() -> None() 27: countdown() S(x12) -> Some(x12) 28: main_4(0(), x39, x51) x8 -> sum(x39) (map() x51 Nil()) 29: main_4(S(x14), x39, x51) x8 -> sum(x39) (map() x51 Cons(S(x14), x8 countdown() S(x14))) 30: cond_unfoldr_f_z(None(), x4) -> Nil() 31: cond_unfoldr_f_z(Some(x6), x4) -> Cons(x6, unfoldr() x4 x6) 32: unfoldr_f(x4) x5 -> cond_unfoldr_f_z(x4 x5, x4) 33: unfoldr_1() x4 -> unfoldr_f(x4) 34: unfoldr() x8 -> unfoldr_f(x8) 35: main_3(0(), x119) x27 -> sum(x119) (map() x27 Nil()) 36: main_3(S(x14), x119) x27 -> sum(x119) (map() x27 Cons(S(x14), unfoldr() countdown() S(x14))) 37: square(x2) x3 -> x2 x3 x3 38: main_2(0(), x87) x191 -> sum(x87) (map() square(x191) Nil()) 39: main_2(S(x14), x87) x191 -> sum(x87) (map() square(x191) Cons(S(x14), unfoldr() countdown() S(x14))) 42: mult_x(x2, 0()) x6 -> 0() 43: mult_x(x2, S(x8)) x6 -> x2 x6 (mult(x2) x8 x6) 44: mult_1(x1) x2 -> mult_x(x1, x2) 45: mult(x2) x4 -> mult_x(x2, x4) 46: main_1(0()) x207 -> sum(x207) (map() square(mult(x207)) Nil()) 47: main_1(S(x14)) x207 -> sum(x207) (map() square(mult(x207)) Cons(S(x14), unfoldr() countdown() S(x14))) 50: plus_x(0()) x4 -> x4 51: plus_x(S(x6)) x4 -> S(plus() x6 x4) 52: plus_1() x1 -> plus_x(x1) 53: plus() x2 -> plus_x(x2) 54: main(0()) -> sum(plus()) (map() square(mult(plus())) Nil()) 55: main(S(x14)) -> sum(plus()) (map() square(mult(plus())) Cons(S(x14), unfoldr() countdown() S(x14))) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list None :: 'a option S :: nat -> nat Some :: 'a -> 'a option countdown :: nat -> nat option enum :: ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat -> nat list map_f :: (nat -> nat) -> nat list -> nat list unfoldr_f :: (nat -> nat option) -> nat -> nat list square :: (nat -> nat -> nat) -> nat -> nat sum_sqs :: (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> (nat list -> nat) -> nat -> nat mult_x :: (nat -> nat -> nat) -> nat -> nat -> nat plus_x :: nat -> nat -> nat main_1 :: nat -> (nat -> nat -> nat) -> nat map_1 :: (nat -> nat) -> nat list -> nat list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat sum_1 :: (nat -> nat -> nat) -> nat list -> nat unfoldr_1 :: (nat -> nat option) -> nat -> nat list main_2 :: nat -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> nat main_4 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> ((nat -> nat option) -> nat -> nat list) -> nat main_5 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat main_6 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> (nat -> nat list) -> nat main_7 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> nat main_8 :: nat -> (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> (nat list -> nat) -> nat main_9 :: nat -> (nat -> nat) -> nat cond_unfoldr_f_z :: nat option -> (nat -> nat option) -> nat list map :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat sum :: (nat -> nat -> nat) -> nat list -> nat unfoldr :: (nat -> nat option) -> nat -> nat list main :: nat -> nat + Applied Processor: NeededRules + Details: none * Step 12: CFA MAYBE + Considered Problem: 1: main_9(x0) x9 -> x9 x0 2: sum_sqs(x3, x6, x7, x8) x9 -> x8 (x7 x3 (x6 x9)) 3: main_8(x18, x6, x12, x14) x16 -> x16 (x14 x6 (x12 x18)) 4: sum_1(x2) Nil() -> 0() 5: sum_1(x2) Cons(x18, x20) -> x2 x18 (sum(x2) x20) 6: sum(x2) Nil() -> 0() 7: sum(x2) Cons(x18, x20) -> x2 x18 (sum(x2) x20) 8: main_7(x18, x15, x6, x12) x14 -> sum(x15) (x14 x6 (x12 x18)) 9: map_f(x14) Nil() -> Nil() 10: map_f(x14) Cons(x18, x20) -> Cons(x14 x18, map() x14 x20) 11: map_1() x7 -> map_f(x7) 12: map() x14 -> map_f(x14) 13: main_6(x18, x11, x6) x12 -> sum(x11) (map() x6 (x12 x18)) 14: enum(x8, x10) 0() -> Nil() 15: enum(x8, x10) S(x14) -> Cons(S(x14), x8 x10 S(x14)) 16: main_5(0(), x111, x27, x8) x10 -> sum(x111) (map() x27 Nil()) 17: main_5(S(x14), x111, x27, x8) x10 -> sum(x111) (map() x27 Cons(S(x14), x8 x10 S(x14))) 18: countdown() 0() -> None() 19: countdown() S(x12) -> Some(x12) 20: main_4(0(), x39, x51) x8 -> sum(x39) (map() x51 Nil()) 21: main_4(S(x14), x39, x51) x8 -> sum(x39) (map() x51 Cons(S(x14), x8 countdown() S(x14))) 22: cond_unfoldr_f_z(None(), x4) -> Nil() 23: cond_unfoldr_f_z(Some(x6), x4) -> Cons(x6, unfoldr() x4 x6) 24: unfoldr_f(x4) x5 -> cond_unfoldr_f_z(x4 x5, x4) 25: unfoldr_1() x4 -> unfoldr_f(x4) 26: unfoldr() x8 -> unfoldr_f(x8) 27: main_3(0(), x119) x27 -> sum(x119) (map() x27 Nil()) 28: main_3(S(x14), x119) x27 -> sum(x119) (map() x27 Cons(S(x14), unfoldr() countdown() S(x14))) 29: square(x2) x3 -> x2 x3 x3 30: main_2(0(), x87) x191 -> sum(x87) (map() square(x191) Nil()) 31: main_2(S(x14), x87) x191 -> sum(x87) (map() square(x191) Cons(S(x14), unfoldr() countdown() S(x14))) 32: mult_x(x2, 0()) x6 -> 0() 33: mult_x(x2, S(x8)) x6 -> x2 x6 (mult(x2) x8 x6) 34: mult_1(x1) x2 -> mult_x(x1, x2) 35: mult(x2) x4 -> mult_x(x2, x4) 36: main_1(0()) x207 -> sum(x207) (map() square(mult(x207)) Nil()) 37: main_1(S(x14)) x207 -> sum(x207) (map() square(mult(x207)) Cons(S(x14), unfoldr() countdown() S(x14))) 38: plus_x(0()) x4 -> x4 39: plus_x(S(x6)) x4 -> S(plus() x6 x4) 40: plus_1() x1 -> plus_x(x1) 41: plus() x2 -> plus_x(x2) 42: main(0()) -> sum(plus()) (map() square(mult(plus())) Nil()) 43: main(S(x14)) -> sum(plus()) (map() square(mult(plus())) Cons(S(x14), unfoldr() countdown() S(x14))) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list None :: 'a option S :: nat -> nat Some :: 'a -> 'a option countdown :: nat -> nat option enum :: ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat -> nat list map_f :: (nat -> nat) -> nat list -> nat list unfoldr_f :: (nat -> nat option) -> nat -> nat list square :: (nat -> nat -> nat) -> nat -> nat sum_sqs :: (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> (nat list -> nat) -> nat -> nat mult_x :: (nat -> nat -> nat) -> nat -> nat -> nat plus_x :: nat -> nat -> nat main_1 :: nat -> (nat -> nat -> nat) -> nat map_1 :: (nat -> nat) -> nat list -> nat list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat sum_1 :: (nat -> nat -> nat) -> nat list -> nat unfoldr_1 :: (nat -> nat option) -> nat -> nat list main_2 :: nat -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> nat main_4 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> ((nat -> nat option) -> nat -> nat list) -> nat main_5 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> ((nat -> nat option) -> nat -> nat list) -> (nat -> nat option) -> nat main_6 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> (nat -> nat list) -> nat main_7 :: nat -> (nat -> nat -> nat) -> (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> nat main_8 :: nat -> (nat -> nat) -> (nat -> nat list) -> ((nat -> nat) -> nat list -> nat list) -> (nat list -> nat) -> nat main_9 :: nat -> (nat -> nat) -> nat cond_unfoldr_f_z :: nat option -> (nat -> nat option) -> nat list map :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat sum :: (nat -> nat -> nat) -> nat list -> nat unfoldr :: (nat -> nat option) -> nat -> nat list main :: nat -> nat + Applied Processor: CFA {cfaRefinement = } + Details: {X{*} -> S(X{*}) | S(X{*}) | Cons(X{*},X{*}) | S(X{*}) | Nil() | 0() | S(X{*}) | S(X{*}) | 0() | S(X{*}) | S(X{*}) | Cons(X{*},X{*}) | S(X{*}) | Nil() | 0() | S(X{*}) | 0() | 0() | S(X{*}) | S(X{*}) | Cons(X{*},X{*}) | S(X{*}) | Nil() | 0() | S(X{*}) | S(X{*}) | Cons(X{*},X{*}) | S(X{*}) | Nil() | 0() | Cons(X{*},X{*}) | Some(X{*}) | Nil() | None() | S(X{*}) | S(X{*}) | Cons(X{*},X{*}) | S(X{*}) | Nil() | 0() | Some(X{*}) | S(X{*}) | None() | 0() | S(X{*}) | S(X{*}) | Cons(X{*},X{*}) | S(X{*}) | Nil() | 0() | S(X{*}) | S(X{*}) | Cons(X{*},X{*}) | S(X{*}) | Nil() | 0() | Cons(X{*},X{*}) | Cons(X{*},X{*}) | Nil() | Nil() | Cons(X{*},X{*}) | 0() | Nil() | Cons(X{*},X{*}) | 0() | Nil() ,V{x2_6} -> V{x2_7} | plus() ,V{x2_7} -> V{x2_7} | plus() ,V{x2_29} -> mult(plus()) ,V{x2_32} -> V{x2_35} ,V{x2_33} -> V{x2_35} ,V{x2_35} -> V{x2_33} | plus() ,V{x2_41} -> V{x6_39} | V{x6_33} | V{x18_7} ,V{x3_29} -> V{x18_10} ,V{x4_22} -> V{x4_24} ,V{x4_23} -> V{x4_24} ,V{x4_24} -> V{x8_26} ,V{x4_35} -> V{x8_33} | V{x3_29} ,V{x4_38} -> V{x4_39} | R{33} | R{32} | R{7} | R{6} ,V{x4_39} -> V{x4_39} | R{33} | R{32} | R{7} | R{6} ,V{x5_24} -> V{x6_23} | S(V{x14_43}) ,V{x6_23} -> V{x12_19} ,V{x6_32} -> V{x6_33} | V{x3_29} ,V{x6_33} -> V{x6_33} | V{x3_29} ,V{x6_39} -> R{39} | R{38} | @(R{41},V{x4_39}) | @(@(plus(),V{x6_39}),V{x4_39}) | X{*} | V{x14_43} ,V{x8_26} -> V{x4_23} | countdown() ,V{x8_33} -> X{*} | V{x14_43} ,V{x12_19} -> X{*} | V{x14_43} ,V{x14_9} -> V{x14_12} ,V{x14_10} -> V{x14_12} ,V{x14_12} -> V{x14_10} | square(mult(plus())) ,V{x14_43} -> X{*} ,V{x18_7} -> @(V{x14_10},V{x18_10}) | R{29} ,V{x18_10} -> V{x6_23} | S(V{x14_43}) ,V{x20_7} -> R{9} | @(@(map(),V{x14_10}),V{x20_10}) | @(R{12},V{x20_10}) | R{10} ,V{x20_10} -> @(@(unfoldr(),V{x4_23}),V{x6_23}) | @(R{26},V{x6_23}) | R{24} ,R{0} -> R{43} | R{42} | main(X{*}) | main(X{*}) ,R{6} -> 0() ,R{7} -> R{39} | R{38} | @(R{41},R{6}) | @(R{41},R{7}) | @(@(V{x2_7},V{x18_7}),R{7}) | @(@(V{x2_7},V{x18_7}),R{6}) | @(R{41},@(sum(V{x2_7}),V{x20_7})) | @(@(V{x2_7},V{x18_7}),@(sum(V{x2_7}),V{x20_7})) ,R{9} -> Nil() ,R{10} -> Cons(@(V{x14_10},V{x18_10}),R{9}) | Cons(R{29},R{9}) | Cons(R{29},R{10}) | Cons(@(V{x14_10},V{x18_10}),R{10}) | Cons(R{29},@(R{12},V{x20_10})) | Cons(@(V{x14_10},V{x18_10}),@(R{12},V{x20_10})) | Cons(R{29},@(@(map(),V{x14_10}),V{x20_10})) | Cons(@(V{x14_10},V{x18_10}),@(@(map(),V{x14_10}),V{x20_10})) ,R{12} -> map_f(V{x14_12}) ,R{18} -> None() ,R{19} -> Some(V{x12_19}) ,R{22} -> Nil() ,R{23} -> Cons(V{x6_23},R{24}) | Cons(V{x6_23},@(R{26},V{x6_23})) | Cons(V{x6_23},@(@(unfoldr(),V{x4_23}),V{x6_23})) ,R{24} -> R{22} | cond_unfoldr_f_z(R{18},V{x4_24}) | R{23} | cond_unfoldr_f_z(R{19},V{x4_24}) | cond_unfoldr_f_z(@(V{x4_24},V{x5_24}),V{x4_24}) ,R{26} -> unfoldr_f(V{x8_26}) ,R{29} -> R{33} | R{32} | @(R{35},V{x3_29}) | @(@(V{x2_29},V{x3_29}),V{x3_29}) ,R{32} -> 0() ,R{33} -> R{39} | R{38} | @(R{41},R{32}) | @(R{41},R{33}) | @(@(V{x2_33},V{x6_33}),R{33}) | @(@(V{x2_33},V{x6_33}),R{32}) | @(R{41},@(R{35},V{x6_33})) | @(@(V{x2_33},V{x6_33}),@(R{35},V{x6_33})) | @(R{41},@(@(mult(V{x2_33}),V{x8_33}),V{x6_33})) | @(@(V{x2_33},V{x6_33}),@(@(mult(V{x2_33}),V{x8_33}),V{x6_33})) ,R{35} -> mult_x(V{x2_35},V{x4_35}) ,R{38} -> V{x4_38} ,R{39} -> S(R{39}) | S(R{38}) | S(@(R{41},V{x4_39})) | S(@(@(plus(),V{x6_39}),V{x4_39})) ,R{41} -> plus_x(V{x2_41}) ,R{42} -> R{6} | @(sum(plus()),R{9}) | @(sum(plus()),@(R{12},Nil())) | @(sum(plus()),@(@(map(),square(mult(plus()))),Nil())) ,R{43} -> R{7} | @(sum(plus()),R{10}) | @(sum(plus()),@(R{12},Cons(S(V{x14_43}),R{24}))) | @(sum(plus()),@(@(map(),square(mult(plus()))),Cons(S(V{x14_43}),R{24}))) | @(sum(plus()),@(R{12},Cons(S(V{x14_43}),@(R{26},S(V{x14_43}))))) | @(sum(plus()),@(@(map(),square(mult(plus()))),Cons(S(V{x14_43}),@(R{26},S(V{x14_43}))))) | @(sum(plus()),@(R{12},Cons(S(V{x14_43}),@(@(unfoldr(),countdown()),S(V{x14_43}))))) | @(sum(plus()) ,@(@(map(),square(mult(plus()))),Cons(S(V{x14_43}),@(@(unfoldr(),countdown()),S(V{x14_43})))))} * Step 13: UncurryATRS MAYBE + Considered Problem: 6: sum(plus()) Nil() -> 0() 7: sum(plus()) Cons(x2, x1) -> plus() x2 (sum(plus()) x1) 9: map_f(square(mult(plus()))) Nil() -> Nil() 10: map_f(square(mult(plus()))) Cons(x2, x1) -> Cons(square(mult(plus())) x2, map() square(mult(plus())) x1) 12: map() square(mult(plus())) -> map_f(square(mult(plus()))) 18: countdown() 0() -> None() 19: countdown() S(x12) -> Some(x12) 22: cond_unfoldr_f_z(None(), countdown()) -> Nil() 23: cond_unfoldr_f_z(Some(x1), countdown()) -> Cons(x1, unfoldr() countdown() x1) 24: unfoldr_f(countdown()) x1 -> cond_unfoldr_f_z(countdown() x1, countdown()) 26: unfoldr() countdown() -> unfoldr_f(countdown()) 29: square(mult(plus())) x1 -> mult(plus()) x1 x1 32: mult_x(plus(), 0()) x1 -> 0() 33: mult_x(plus(), S(x2)) x1 -> plus() x1 (mult(plus()) x2 x1) 35: mult(plus()) x1 -> mult_x(plus(), x1) 38: plus_x(0()) x4 -> x4 39: plus_x(S(x2)) x1 -> S(plus() x2 x1) 41: plus() x2 -> plus_x(x2) 42: main(0()) -> sum(plus()) (map() square(mult(plus())) Nil()) 43: main(S(x1)) -> sum(plus()) (map() square(mult(plus())) Cons(S(x1), unfoldr() countdown() S(x1))) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list None :: 'a option S :: nat -> nat Some :: 'a -> 'a option countdown :: nat -> nat option map_f :: (nat -> nat) -> nat list -> nat list unfoldr_f :: (nat -> nat option) -> nat -> nat list square :: (nat -> nat -> nat) -> nat -> nat mult_x :: (nat -> nat -> nat) -> nat -> nat -> nat plus_x :: nat -> nat -> nat cond_unfoldr_f_z :: nat option -> (nat -> nat option) -> nat list map :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat sum :: (nat -> nat -> nat) -> nat list -> nat unfoldr :: (nat -> nat option) -> nat -> nat list main :: nat -> nat + Applied Processor: UncurryATRS + Details: none * Step 14: UsableRules MAYBE + Considered Problem: 1: sum#1(plus(), Nil()) -> 0() 2: sum#1(plus(), Cons(x2, x1)) -> plus#2(x2, sum#1(plus(), x1)) 3: map_f#1(square(mult(plus())), Nil()) -> Nil() 4: map_f#1(square(mult(plus())), Cons(x2, x1)) -> Cons(square#1(mult(plus()), x2) , map#2(square(mult(plus())), x1)) 5: map#1(square(mult(plus()))) -> map_f(square(mult(plus()))) 6: map#2(square(mult(plus())), x0) -> map_f#1(square(mult(plus())), x0) 7: countdown#1(0()) -> None() 8: countdown#1(S(x12)) -> Some(x12) 9: cond_unfoldr_f_z(None(), countdown()) -> Nil() 10: cond_unfoldr_f_z(Some(x1), countdown()) -> Cons(x1, unfoldr#2(countdown(), x1)) 11: unfoldr_f#1(countdown(), x1) -> cond_unfoldr_f_z(countdown#1(x1), countdown()) 12: unfoldr#1(countdown()) -> unfoldr_f(countdown()) 13: unfoldr#2(countdown(), x0) -> unfoldr_f#1(countdown(), x0) 14: square#1(mult(plus()), x1) -> mult#2(plus(), x1, x1) 15: mult_x#1(plus(), 0(), x1) -> 0() 16: mult_x#1(plus(), S(x2), x1) -> plus#2(x1, mult#2(plus(), x2, x1)) 17: mult#1(plus(), x1) -> mult_x(plus(), x1) 18: mult#2(plus(), x1, x2) -> mult_x#1(plus(), x1, x2) 19: plus_x#1(0(), x4) -> x4 20: plus_x#1(S(x2), x1) -> S(plus#2(x2, x1)) 21: plus#1(x2) -> plus_x(x2) 22: plus#2(x2, x3) -> plus_x#1(x2, x3) 23: main(0()) -> sum#1(plus(), map#2(square(mult(plus())), Nil())) 24: main(S(x1)) -> sum#1(plus(), map#2(square(mult(plus())), Cons(S(x1), unfoldr#2(countdown(), S(x1))))) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list None :: 'a option S :: nat -> nat Some :: 'a -> 'a option cond_unfoldr_f_z :: nat option -> (nat -> nat option) -> nat list countdown :: nat -> nat option countdown#1 :: nat -> nat option main :: nat -> nat map#1 :: (nat -> nat) -> nat list -> nat list map#2 :: (nat -> nat) -> nat list -> nat list map_f :: (nat -> nat) -> nat list -> nat list map_f#1 :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat mult#1 :: (nat -> nat -> nat) -> nat -> nat -> nat mult#2 :: (nat -> nat -> nat) -> nat -> nat -> nat mult_x :: (nat -> nat -> nat) -> nat -> nat -> nat mult_x#1 :: (nat -> nat -> nat) -> nat -> nat -> nat 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 square :: (nat -> nat -> nat) -> nat -> nat square#1 :: (nat -> nat -> nat) -> nat -> nat sum#1 :: (nat -> nat -> nat) -> nat list -> nat unfoldr#1 :: (nat -> nat option) -> nat -> nat list unfoldr#2 :: (nat -> nat option) -> nat -> nat list unfoldr_f :: (nat -> nat option) -> nat -> nat list unfoldr_f#1 :: (nat -> nat option) -> nat -> nat list + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 15: Inline MAYBE + Considered Problem: 1: sum#1(plus(), Nil()) -> 0() 2: sum#1(plus(), Cons(x2, x1)) -> plus#2(x2, sum#1(plus(), x1)) 3: map_f#1(square(mult(plus())), Nil()) -> Nil() 4: map_f#1(square(mult(plus())), Cons(x2, x1)) -> Cons(square#1(mult(plus()), x2) , map#2(square(mult(plus())), x1)) 6: map#2(square(mult(plus())), x0) -> map_f#1(square(mult(plus())), x0) 7: countdown#1(0()) -> None() 8: countdown#1(S(x12)) -> Some(x12) 9: cond_unfoldr_f_z(None(), countdown()) -> Nil() 10: cond_unfoldr_f_z(Some(x1), countdown()) -> Cons(x1, unfoldr#2(countdown(), x1)) 11: unfoldr_f#1(countdown(), x1) -> cond_unfoldr_f_z(countdown#1(x1), countdown()) 13: unfoldr#2(countdown(), x0) -> unfoldr_f#1(countdown(), x0) 14: square#1(mult(plus()), x1) -> mult#2(plus(), x1, x1) 15: mult_x#1(plus(), 0(), x1) -> 0() 16: mult_x#1(plus(), S(x2), x1) -> plus#2(x1, mult#2(plus(), x2, x1)) 18: mult#2(plus(), x1, x2) -> mult_x#1(plus(), x1, x2) 19: plus_x#1(0(), x4) -> x4 20: plus_x#1(S(x2), x1) -> S(plus#2(x2, x1)) 22: plus#2(x2, x3) -> plus_x#1(x2, x3) 23: main(0()) -> sum#1(plus(), map#2(square(mult(plus())), Nil())) 24: main(S(x1)) -> sum#1(plus(), map#2(square(mult(plus())), Cons(S(x1), unfoldr#2(countdown(), S(x1))))) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list None :: 'a option S :: nat -> nat Some :: 'a -> 'a option cond_unfoldr_f_z :: nat option -> (nat -> nat option) -> nat list countdown :: nat -> nat option countdown#1 :: nat -> nat option main :: nat -> nat map#2 :: (nat -> nat) -> nat list -> nat list map_f#1 :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat mult#2 :: (nat -> nat -> nat) -> nat -> nat -> nat mult_x#1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat plus_x#1 :: nat -> nat -> nat square :: (nat -> nat -> nat) -> nat -> nat square#1 :: (nat -> nat -> nat) -> nat -> nat sum#1 :: (nat -> nat -> nat) -> nat list -> nat unfoldr#2 :: (nat -> nat option) -> nat -> nat list unfoldr_f#1 :: (nat -> nat option) -> nat -> nat list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 16: UsableRules MAYBE + Considered Problem: 1: sum#1(plus(), Nil()) -> 0() 2: sum#1(plus(), Cons(x2, x1)) -> plus#2(x2, sum#1(plus(), x1)) 3: map_f#1(square(mult(plus())), Nil()) -> Nil() 4: map_f#1(square(mult(plus())), Cons(x2, x3)) -> Cons(mult#2(plus(), x2, x2), map#2(square(mult(plus())) , x3)) 5: map#2(square(mult(plus())), Nil()) -> Nil() 6: map#2(square(mult(plus())), Cons(x4, x2)) -> Cons(square#1(mult(plus()), x4), map#2(square(mult(plus())) , x2)) 7: countdown#1(0()) -> None() 8: countdown#1(S(x12)) -> Some(x12) 9: cond_unfoldr_f_z(None(), countdown()) -> Nil() 10: cond_unfoldr_f_z(Some(x1), countdown()) -> Cons(x1, unfoldr#2(countdown(), x1)) 11: unfoldr_f#1(countdown(), 0()) -> cond_unfoldr_f_z(None(), countdown()) 12: unfoldr_f#1(countdown(), S(x24)) -> cond_unfoldr_f_z(Some(x24), countdown()) 13: unfoldr#2(countdown(), x2) -> cond_unfoldr_f_z(countdown#1(x2), countdown()) 14: square#1(mult(plus()), x1) -> mult#2(plus(), x1, x1) 15: mult_x#1(plus(), 0(), x1) -> 0() 16: mult_x#1(plus(), S(x2), x1) -> plus#2(x1, mult#2(plus(), x2, x1)) 17: mult#2(plus(), 0(), x2) -> 0() 18: mult#2(plus(), S(x4), x2) -> plus#2(x2, mult#2(plus(), x4, x2)) 19: plus_x#1(0(), x4) -> x4 20: plus_x#1(S(x2), x1) -> S(plus#2(x2, x1)) 21: plus#2(0(), x8) -> x8 22: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 23: main(0()) -> sum#1(plus(), map#2(square(mult(plus())), Nil())) 24: main(S(x1)) -> sum#1(plus(), map#2(square(mult(plus())), Cons(S(x1), unfoldr#2(countdown(), S(x1))))) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list None :: 'a option S :: nat -> nat Some :: 'a -> 'a option cond_unfoldr_f_z :: nat option -> (nat -> nat option) -> nat list countdown :: nat -> nat option countdown#1 :: nat -> nat option main :: nat -> nat map#2 :: (nat -> nat) -> nat list -> nat list map_f#1 :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat mult#2 :: (nat -> nat -> nat) -> nat -> nat -> nat mult_x#1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat plus_x#1 :: nat -> nat -> nat square :: (nat -> nat -> nat) -> nat -> nat square#1 :: (nat -> nat -> nat) -> nat -> nat sum#1 :: (nat -> nat -> nat) -> nat list -> nat unfoldr#2 :: (nat -> nat option) -> nat -> nat list unfoldr_f#1 :: (nat -> nat option) -> nat -> nat list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 17: Inline MAYBE + Considered Problem: 1: sum#1(plus(), Nil()) -> 0() 2: sum#1(plus(), Cons(x2, x1)) -> plus#2(x2, sum#1(plus(), x1)) 5: map#2(square(mult(plus())), Nil()) -> Nil() 6: map#2(square(mult(plus())), Cons(x4, x2)) -> Cons(square#1(mult(plus()), x4), map#2(square(mult(plus())) , x2)) 7: countdown#1(0()) -> None() 8: countdown#1(S(x12)) -> Some(x12) 9: cond_unfoldr_f_z(None(), countdown()) -> Nil() 10: cond_unfoldr_f_z(Some(x1), countdown()) -> Cons(x1, unfoldr#2(countdown(), x1)) 13: unfoldr#2(countdown(), x2) -> cond_unfoldr_f_z(countdown#1(x2), countdown()) 14: square#1(mult(plus()), x1) -> mult#2(plus(), x1, x1) 17: mult#2(plus(), 0(), x2) -> 0() 18: mult#2(plus(), S(x4), x2) -> plus#2(x2, mult#2(plus(), x4, x2)) 21: plus#2(0(), x8) -> x8 22: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 23: main(0()) -> sum#1(plus(), map#2(square(mult(plus())), Nil())) 24: main(S(x1)) -> sum#1(plus(), map#2(square(mult(plus())), Cons(S(x1), unfoldr#2(countdown(), S(x1))))) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list None :: 'a option S :: nat -> nat Some :: 'a -> 'a option cond_unfoldr_f_z :: nat option -> (nat -> nat option) -> nat list countdown :: nat -> nat option countdown#1 :: nat -> nat option main :: nat -> nat map#2 :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat mult#2 :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat square :: (nat -> nat -> nat) -> nat -> nat square#1 :: (nat -> nat -> nat) -> nat -> nat sum#1 :: (nat -> nat -> nat) -> nat list -> nat unfoldr#2 :: (nat -> nat option) -> nat -> nat list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 18: UsableRules MAYBE + Considered Problem: 1: sum#1(plus(), Nil()) -> 0() 2: sum#1(plus(), Cons(x2, x1)) -> plus#2(x2, sum#1(plus(), x1)) 3: map#2(square(mult(plus())), Nil()) -> Nil() 4: map#2(square(mult(plus())), Cons(x2, x5)) -> Cons(mult#2(plus(), x2, x2), map#2(square(mult(plus())) , x5)) 5: countdown#1(0()) -> None() 6: countdown#1(S(x12)) -> Some(x12) 7: cond_unfoldr_f_z(None(), countdown()) -> Nil() 8: cond_unfoldr_f_z(Some(x1), countdown()) -> Cons(x1, unfoldr#2(countdown(), x1)) 9: unfoldr#2(countdown(), 0()) -> cond_unfoldr_f_z(None(), countdown()) 10: unfoldr#2(countdown(), S(x24)) -> cond_unfoldr_f_z(Some(x24), countdown()) 11: square#1(mult(plus()), x1) -> mult#2(plus(), x1, x1) 12: mult#2(plus(), 0(), x2) -> 0() 13: mult#2(plus(), S(x4), x2) -> plus#2(x2, mult#2(plus(), x4, x2)) 14: plus#2(0(), x8) -> x8 15: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 16: main(0()) -> sum#1(plus(), Nil()) 17: main(S(x1)) -> sum#1(plus(), map#2(square(mult(plus())), Cons(S(x1), unfoldr#2(countdown(), S(x1))))) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list None :: 'a option S :: nat -> nat Some :: 'a -> 'a option cond_unfoldr_f_z :: nat option -> (nat -> nat option) -> nat list countdown :: nat -> nat option countdown#1 :: nat -> nat option main :: nat -> nat map#2 :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat mult#2 :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat square :: (nat -> nat -> nat) -> nat -> nat square#1 :: (nat -> nat -> nat) -> nat -> nat sum#1 :: (nat -> nat -> nat) -> nat list -> nat unfoldr#2 :: (nat -> nat option) -> nat -> nat list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 19: Inline MAYBE + Considered Problem: 1: sum#1(plus(), Nil()) -> 0() 2: sum#1(plus(), Cons(x2, x1)) -> plus#2(x2, sum#1(plus(), x1)) 3: map#2(square(mult(plus())), Nil()) -> Nil() 4: map#2(square(mult(plus())), Cons(x2, x5)) -> Cons(mult#2(plus(), x2, x2), map#2(square(mult(plus())) , x5)) 7: cond_unfoldr_f_z(None(), countdown()) -> Nil() 8: cond_unfoldr_f_z(Some(x1), countdown()) -> Cons(x1, unfoldr#2(countdown(), x1)) 9: unfoldr#2(countdown(), 0()) -> cond_unfoldr_f_z(None(), countdown()) 10: unfoldr#2(countdown(), S(x24)) -> cond_unfoldr_f_z(Some(x24), countdown()) 12: mult#2(plus(), 0(), x2) -> 0() 13: mult#2(plus(), S(x4), x2) -> plus#2(x2, mult#2(plus(), x4, x2)) 14: plus#2(0(), x8) -> x8 15: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 16: main(0()) -> sum#1(plus(), Nil()) 17: main(S(x1)) -> sum#1(plus(), map#2(square(mult(plus())), Cons(S(x1), unfoldr#2(countdown(), S(x1))))) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list None :: 'a option S :: nat -> nat Some :: 'a -> 'a option cond_unfoldr_f_z :: nat option -> (nat -> nat option) -> nat list countdown :: nat -> nat option main :: nat -> nat map#2 :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat mult#2 :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat square :: (nat -> nat -> nat) -> nat -> nat sum#1 :: (nat -> nat -> nat) -> nat list -> nat unfoldr#2 :: (nat -> nat option) -> nat -> nat list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 20: UsableRules MAYBE + Considered Problem: 1: sum#1(plus(), Nil()) -> 0() 2: sum#1(plus(), Cons(x2, x1)) -> plus#2(x2, sum#1(plus(), x1)) 3: map#2(square(mult(plus())), Nil()) -> Nil() 4: map#2(square(mult(plus())), Cons(x2, x5)) -> Cons(mult#2(plus(), x2, x2), map#2(square(mult(plus())) , x5)) 5: cond_unfoldr_f_z(None(), countdown()) -> Nil() 6: cond_unfoldr_f_z(Some(x1), countdown()) -> Cons(x1, unfoldr#2(countdown(), x1)) 7: unfoldr#2(countdown(), 0()) -> Nil() 8: unfoldr#2(countdown(), S(x2)) -> Cons(x2, unfoldr#2(countdown(), x2)) 9: mult#2(plus(), 0(), x2) -> 0() 10: mult#2(plus(), S(x4), x2) -> plus#2(x2, mult#2(plus(), x4, x2)) 11: plus#2(0(), x8) -> x8 12: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 13: main(0()) -> 0() 14: main(S(x1)) -> sum#1(plus(), map#2(square(mult(plus())), Cons(S(x1), unfoldr#2(countdown(), S(x1))))) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list None :: 'a option S :: nat -> nat Some :: 'a -> 'a option cond_unfoldr_f_z :: nat option -> (nat -> nat option) -> nat list countdown :: nat -> nat option main :: nat -> nat map#2 :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat mult#2 :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat square :: (nat -> nat -> nat) -> nat -> nat sum#1 :: (nat -> nat -> nat) -> nat list -> nat unfoldr#2 :: (nat -> nat option) -> nat -> nat list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 21: UsableRules MAYBE + Considered Problem: 1: sum#1(plus(), Nil()) -> 0() 2: sum#1(plus(), Cons(x2, x1)) -> plus#2(x2, sum#1(plus(), x1)) 3: map#2(square(mult(plus())), Nil()) -> Nil() 4: map#2(square(mult(plus())), Cons(x2, x5)) -> Cons(mult#2(plus(), x2, x2), map#2(square(mult(plus())) , x5)) 7: unfoldr#2(countdown(), 0()) -> Nil() 8: unfoldr#2(countdown(), S(x2)) -> Cons(x2, unfoldr#2(countdown(), x2)) 9: mult#2(plus(), 0(), x2) -> 0() 10: mult#2(plus(), S(x4), x2) -> plus#2(x2, mult#2(plus(), x4, x2)) 11: plus#2(0(), x8) -> x8 12: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 13: main(0()) -> 0() 14: main(S(x1)) -> sum#1(plus(), map#2(square(mult(plus())), Cons(S(x1), unfoldr#2(countdown(), S(x1))))) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat countdown :: nat -> nat option main :: nat -> nat map#2 :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat mult#2 :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat square :: (nat -> nat -> nat) -> nat -> nat sum#1 :: (nat -> nat -> nat) -> nat list -> nat unfoldr#2 :: (nat -> nat option) -> nat -> nat list + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 22: Compression MAYBE + Considered Problem: 1: sum#1(plus(), Nil()) -> 0() 2: sum#1(plus(), Cons(x2, x1)) -> plus#2(x2, sum#1(plus(), x1)) 3: map#2(square(mult(plus())), Nil()) -> Nil() 4: map#2(square(mult(plus())), Cons(x2, x5)) -> Cons(mult#2(plus(), x2, x2), map#2(square(mult(plus())) , x5)) 5: unfoldr#2(countdown(), 0()) -> Nil() 6: unfoldr#2(countdown(), S(x2)) -> Cons(x2, unfoldr#2(countdown(), x2)) 7: mult#2(plus(), 0(), x2) -> 0() 8: mult#2(plus(), S(x4), x2) -> plus#2(x2, mult#2(plus(), x4, x2)) 9: plus#2(0(), x8) -> x8 10: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 11: main(0()) -> 0() 12: main(S(x1)) -> sum#1(plus(), map#2(square(mult(plus())), Cons(S(x1), unfoldr#2(countdown(), S(x1))))) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat countdown :: nat -> nat option main :: nat -> nat map#2 :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat mult#2 :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat square :: (nat -> nat -> nat) -> nat -> nat sum#1 :: (nat -> nat -> nat) -> nat list -> nat unfoldr#2 :: (nat -> nat option) -> nat -> nat list + Applied Processor: Compression + Details: none * Step 23: ToTctProblem MAYBE + Considered Problem: 1: sum#1(Nil()) -> 0() 2: sum#1(Cons(x2, x1)) -> plus#2(x2, sum#1(x1)) 3: map#2(Nil()) -> Nil() 4: map#2(Cons(x2, x5)) -> Cons(mult#2(x2, x2), map#2(x5)) 5: unfoldr#2(0()) -> Nil() 6: unfoldr#2(S(x2)) -> Cons(x2, unfoldr#2(x2)) 7: mult#2(0(), x2) -> 0() 8: mult#2(S(x4), x2) -> plus#2(x2, mult#2(x4, x2)) 9: plus#2(0(), x8) -> x8 10: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 11: main(0()) -> 0() 12: main(S(x1)) -> sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1))))) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat main :: nat -> nat map#2 :: nat list -> nat list mult#2 :: nat -> nat -> nat plus#2 :: nat -> nat -> nat sum#1 :: nat list -> nat unfoldr#2 :: nat -> nat list + Applied Processor: ToTctProblem + Details: none * Step 24: Failure MAYBE + Considered Problem: - Strict TRS: main(0()) -> 0() main(S(x1)) -> sum#1(map#2(Cons(S(x1),unfoldr#2(S(x1))))) map#2(Cons(x2,x5)) -> Cons(mult#2(x2,x2),map#2(x5)) map#2(Nil()) -> Nil() mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> plus#2(x2,mult#2(x4,x2)) plus#2(0(),x8) -> x8 plus#2(S(x4),x2) -> S(plus#2(x4,x2)) sum#1(Cons(x2,x1)) -> plus#2(x2,sum#1(x1)) sum#1(Nil()) -> 0() unfoldr#2(0()) -> Nil() unfoldr#2(S(x2)) -> Cons(x2,unfoldr#2(x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2,sum#1/1,unfoldr#2/1} / {0/0,Cons/2,Nil/0,S/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,Cons,Nil,S} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE