WORST_CASE(?,O(n^1)) * Step 1: Desugar WORST_CASE(?,O(n^1)) + Considered Problem: type nat = 0 | S of nat ;; type 'a list = Nil | Cons of 'a * 'a list ;; let rec foldr f z xs = match xs with | Nil -> z | Cons(x,xs') -> f x (foldr f z xs') ;; let rec plus x y = match x with | 0 -> y | S(x') -> S(plus x' y) ;; let rec map f xs = match xs with | Nil -> Nil | Cons(x,xs') -> Cons(f x, map f xs') ;; let comp f g z = f (g z) ;; let id x = x ;; let foldsum l = foldr comp id (map plus l) 0 ;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization WORST_CASE(?,O(n^1)) + Considered Problem: λl : nat list. (λfoldr : ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat. (λplus : nat -> nat -> nat. (λmap : (nat -> nat -> nat) -> nat list -> nat -> nat list. (λcomp : (nat -> nat) -> (nat -> nat) -> nat -> nat. (λid : nat -> nat. (λfoldsum : nat list -> nat. foldsum l) (λl : nat list. foldr comp id (map plus l) 0)) (λx : nat. x)) (λf : nat -> nat. λg : nat -> nat. λz : nat. f (g z))) (μmap : (nat -> nat -> nat) -> nat list -> nat -> nat list. λf : nat -> nat -> nat. λxs : nat list. case xs of | Nil -> Nil | Cons -> λx : nat. λxs' : nat list. Cons(f x,map f xs'))) (μplus : nat -> nat -> nat. λx : nat. λy : nat. case x of | 0 -> y | S -> λx' : nat. S(plus x' y))) (μfoldr : ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat. λf : (nat -> nat) -> (nat -> nat) -> nat -> nat. λz : nat -> nat. λxs : nat -> nat list. case xs of | Nil -> z | Cons -> λx : nat -> nat. λxs' : nat -> nat list. f x (foldr f z xs')) : nat list -> nat where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat + Applied Processor: Defunctionalization + Details: none * Step 3: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: foldsum(x1, x2, x3, x4, x5) x6 -> x1 x4 x5 (x3 x2 x6) 0() 3: main_5(x0, x1, x2, x3, x4) x5 -> main_6(x0) foldsum(x1, x2, x3, x4, x5) 4: id() x5 -> x5 5: main_4(x0, x1, x2, x3) x4 -> main_5(x0, x1, x2, x3, x4) id() 6: comp_f_g(x4, x5) x6 -> x4 (x5 x6) 7: comp_f(x4) x5 -> comp_f_g(x4, x5) 8: comp() x4 -> comp_f(x4) 9: main_3(x0, x1, x2) x3 -> main_4(x0, x1, x2, x3) comp() 10: cond_map_f_xs(Nil(), x3) -> Nil() 11: cond_map_f_xs(Cons(x5, x6), x3) -> Cons(x3 x5, map() x3 x6) 12: map_f(x3) x4 -> cond_map_f_xs(x4, x3) 13: map_1() x3 -> map_f(x3) 14: map() x0 -> map_1() x0 15: main_2(x0, x1) x2 -> main_3(x0, x1, x2) map() 16: cond_plus_x_y(0(), x3) -> x3 17: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 18: plus_x(x2) x3 -> cond_plus_x_y(x2, x3) 19: plus_1() x2 -> plus_x(x2) 20: plus() x0 -> plus_1() x0 21: main_1(x0) x1 -> main_2(x0, x1) plus() 22: cond_foldr_f_z_xs(Nil(), x1, x2) -> x2 23: cond_foldr_f_z_xs(Cons(x4, x5), x1, x2) -> x1 x4 (foldr() x1 x2 x5) 24: foldr_f_z(x1, x2) x3 -> cond_foldr_f_z_xs(x3, x1, x2) 25: foldr_f(x1) x2 -> foldr_f_z(x1, x2) 26: foldr_1() x1 -> foldr_f(x1) 27: foldr() x0 -> foldr_1() x0 28: main(x0) -> main_1(x0) foldr() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f :: (nat -> nat) -> (nat -> nat) -> nat -> nat foldr_f :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat map_f :: (nat -> nat -> nat) -> nat list -> nat -> nat list foldsum :: (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat list -> nat comp_f_g :: (nat -> nat) -> (nat -> nat) -> nat -> nat id :: nat -> nat plus_x :: nat -> nat -> nat foldr_f_z :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_1 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat main_1 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> nat map_1 :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus_1 :: nat -> nat -> nat main_2 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> nat main_4 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> nat main_5 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat main_6 :: nat list -> (nat list -> nat) -> nat cond_map_f_xs :: nat list -> (nat -> nat -> nat) -> nat -> nat list cond_foldr_f_z_xs :: nat -> nat list -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat cond_plus_x_y :: nat -> nat -> nat foldr :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat map :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus :: nat -> nat -> nat main :: nat list -> nat + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: foldsum(x1, x2, x3, x4, x5) x6 -> x1 x4 x5 (x3 x2 x6) 0() 3: main_5(x0, x3, x5, x7, x9) x11 -> foldsum(x3, x5, x7, x9, x11) x0 4: id() x5 -> x5 5: main_4(x0, x2, x4, x6) x8 -> main_6(x0) foldsum(x2, x4, x6, x8, id()) 6: comp_f_g(x4, x5) x6 -> x4 (x5 x6) 7: comp_f(x4) x5 -> comp_f_g(x4, x5) 8: comp() x4 -> comp_f(x4) 9: main_3(x0, x2, x4) x6 -> main_5(x0, x2, x4, x6, comp()) id() 10: cond_map_f_xs(Nil(), x3) -> Nil() 11: cond_map_f_xs(Cons(x5, x6), x3) -> Cons(x3 x5, map() x3 x6) 12: map_f(x3) x4 -> cond_map_f_xs(x4, x3) 13: map_1() x3 -> map_f(x3) 14: map() x6 -> map_f(x6) 15: main_2(x0, x2) x4 -> main_4(x0, x2, x4, map()) comp() 16: cond_plus_x_y(0(), x3) -> x3 17: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 18: plus_x(x2) x3 -> cond_plus_x_y(x2, x3) 19: plus_1() x2 -> plus_x(x2) 20: plus() x4 -> plus_x(x4) 21: main_1(x0) x2 -> main_3(x0, x2, plus()) map() 22: cond_foldr_f_z_xs(Nil(), x1, x2) -> x2 23: cond_foldr_f_z_xs(Cons(x4, x5), x1, x2) -> x1 x4 (foldr() x1 x2 x5) 24: foldr_f_z(x1, x2) x3 -> cond_foldr_f_z_xs(x3, x1, x2) 25: foldr_f(x1) x2 -> foldr_f_z(x1, x2) 26: foldr_1() x1 -> foldr_f(x1) 27: foldr() x2 -> foldr_f(x2) 28: main(x0) -> main_2(x0, foldr()) plus() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f :: (nat -> nat) -> (nat -> nat) -> nat -> nat foldr_f :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat map_f :: (nat -> nat -> nat) -> nat list -> nat -> nat list foldsum :: (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat list -> nat comp_f_g :: (nat -> nat) -> (nat -> nat) -> nat -> nat id :: nat -> nat plus_x :: nat -> nat -> nat foldr_f_z :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_1 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat main_1 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> nat map_1 :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus_1 :: nat -> nat -> nat main_2 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> nat main_4 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> nat main_5 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat main_6 :: nat list -> (nat list -> nat) -> nat cond_map_f_xs :: nat list -> (nat -> nat -> nat) -> nat -> nat list cond_foldr_f_z_xs :: nat -> nat list -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat cond_plus_x_y :: nat -> nat -> nat foldr :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat map :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus :: nat -> nat -> nat main :: nat list -> nat + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 5: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: foldsum(x1, x2, x3, x4, x5) x6 -> x1 x4 x5 (x3 x2 x6) 0() 3: main_5(x12, x2, x4, x6, x8) x10 -> x2 x8 x10 (x6 x4 x12) 0() 4: id() x5 -> x5 5: main_4(x0, x5, x9, x13) x17 -> foldsum(x5, x9, x13, x17, id()) x0 6: comp_f_g(x4, x5) x6 -> x4 (x5 x6) 7: comp_f(x4) x5 -> comp_f_g(x4, x5) 8: comp() x4 -> comp_f(x4) 9: main_3(x0, x6, x10) x14 -> foldsum(x6, x10, x14, comp(), id()) x0 10: cond_map_f_xs(Nil(), x3) -> Nil() 11: cond_map_f_xs(Cons(x5, x6), x3) -> Cons(x3 x5, map() x3 x6) 12: map_f(x3) x4 -> cond_map_f_xs(x4, x3) 13: map_1() x3 -> map_f(x3) 14: map() x6 -> map_f(x6) 15: main_2(x0, x4) x8 -> main_6(x0) foldsum(x4, x8, map(), comp(), id()) 16: cond_plus_x_y(0(), x3) -> x3 17: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 18: plus_x(x2) x3 -> cond_plus_x_y(x2, x3) 19: plus_1() x2 -> plus_x(x2) 20: plus() x4 -> plus_x(x4) 21: main_1(x0) x4 -> main_5(x0, x4, plus(), map(), comp()) id() 22: cond_foldr_f_z_xs(Nil(), x1, x2) -> x2 23: cond_foldr_f_z_xs(Cons(x4, x5), x1, x2) -> x1 x4 (foldr() x1 x2 x5) 24: foldr_f_z(x1, x2) x3 -> cond_foldr_f_z_xs(x3, x1, x2) 25: foldr_f(x1) x2 -> foldr_f_z(x1, x2) 26: foldr_1() x1 -> foldr_f(x1) 27: foldr() x2 -> foldr_f(x2) 28: main(x0) -> main_4(x0, foldr(), plus(), map()) comp() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f :: (nat -> nat) -> (nat -> nat) -> nat -> nat foldr_f :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat map_f :: (nat -> nat -> nat) -> nat list -> nat -> nat list foldsum :: (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat list -> nat comp_f_g :: (nat -> nat) -> (nat -> nat) -> nat -> nat id :: nat -> nat plus_x :: nat -> nat -> nat foldr_f_z :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_1 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat main_1 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> nat map_1 :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus_1 :: nat -> nat -> nat main_2 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> nat main_4 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> nat main_5 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat main_6 :: nat list -> (nat list -> nat) -> nat cond_map_f_xs :: nat list -> (nat -> nat -> nat) -> nat -> nat list cond_foldr_f_z_xs :: nat -> nat list -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat cond_plus_x_y :: nat -> nat -> nat foldr :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat map :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus :: nat -> nat -> nat main :: nat list -> nat + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 6: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: foldsum(x1, x2, x3, x4, x5) x6 -> x1 x4 x5 (x3 x2 x6) 0() 3: main_5(x12, x2, x4, x6, x8) x10 -> x2 x8 x10 (x6 x4 x12) 0() 4: id() x5 -> x5 5: main_4(x12, x2, x4, x6) x8 -> x2 x8 id() (x6 x4 x12) 0() 6: comp_f_g(x4, x5) x6 -> x4 (x5 x6) 7: comp_f(x4) x5 -> comp_f_g(x4, x5) 8: comp() x4 -> comp_f(x4) 9: main_3(x12, x2, x4) x6 -> x2 comp() id() (x6 x4 x12) 0() 10: cond_map_f_xs(Nil(), x3) -> Nil() 11: cond_map_f_xs(Cons(x5, x6), x3) -> Cons(x3 x5, map() x3 x6) 12: map_f(x3) x4 -> cond_map_f_xs(x4, x3) 13: map_1() x3 -> map_f(x3) 14: map() x6 -> map_f(x6) 15: main_2(x0, x9) x17 -> foldsum(x9, x17, map(), comp(), id()) x0 16: cond_plus_x_y(0(), x3) -> x3 17: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 18: plus_x(x2) x3 -> cond_plus_x_y(x2, x3) 19: plus_1() x2 -> plus_x(x2) 20: plus() x4 -> plus_x(x4) 21: main_1(x24) x4 -> x4 comp() id() (map() plus() x24) 0() 22: cond_foldr_f_z_xs(Nil(), x1, x2) -> x2 23: cond_foldr_f_z_xs(Cons(x4, x5), x1, x2) -> x1 x4 (foldr() x1 x2 x5) 24: foldr_f_z(x1, x2) x3 -> cond_foldr_f_z_xs(x3, x1, x2) 25: foldr_f(x1) x2 -> foldr_f_z(x1, x2) 26: foldr_1() x1 -> foldr_f(x1) 27: foldr() x2 -> foldr_f(x2) 28: main(x0) -> foldsum(foldr(), plus(), map(), comp(), id()) x0 where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f :: (nat -> nat) -> (nat -> nat) -> nat -> nat foldr_f :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat map_f :: (nat -> nat -> nat) -> nat list -> nat -> nat list foldsum :: (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat list -> nat comp_f_g :: (nat -> nat) -> (nat -> nat) -> nat -> nat id :: nat -> nat plus_x :: nat -> nat -> nat foldr_f_z :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_1 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat main_1 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> nat map_1 :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus_1 :: nat -> nat -> nat main_2 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> nat main_4 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> nat main_5 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat main_6 :: nat list -> (nat list -> nat) -> nat cond_map_f_xs :: nat list -> (nat -> nat -> nat) -> nat -> nat list cond_foldr_f_z_xs :: nat -> nat list -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat cond_plus_x_y :: nat -> nat -> nat foldr :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat map :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus :: nat -> nat -> nat main :: nat list -> nat + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 7: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: foldsum(x1, x2, x3, x4, x5) x6 -> x1 x4 x5 (x3 x2 x6) 0() 3: main_5(x12, x2, x4, x6, x8) x10 -> x2 x8 x10 (x6 x4 x12) 0() 4: id() x5 -> x5 5: main_4(x12, x2, x4, x6) x8 -> x2 x8 id() (x6 x4 x12) 0() 6: comp_f_g(x4, x5) x6 -> x4 (x5 x6) 7: comp_f(x4) x5 -> comp_f_g(x4, x5) 8: comp() x4 -> comp_f(x4) 9: main_3(x12, x2, x4) x6 -> x2 comp() id() (x6 x4 x12) 0() 10: cond_map_f_xs(Nil(), x3) -> Nil() 11: cond_map_f_xs(Cons(x5, x6), x3) -> Cons(x3 x5, map() x3 x6) 12: map_f(x3) x4 -> cond_map_f_xs(x4, x3) 13: map_1() x3 -> map_f(x3) 14: map() x6 -> map_f(x6) 15: main_2(x12, x2) x4 -> x2 comp() id() (map() x4 x12) 0() 16: cond_plus_x_y(0(), x3) -> x3 17: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 18: plus_x(x2) x3 -> cond_plus_x_y(x2, x3) 19: plus_1() x2 -> plus_x(x2) 20: plus() x4 -> plus_x(x4) 21: main_1(x24) x4 -> x4 comp() id() (map() plus() x24) 0() 22: cond_foldr_f_z_xs(Nil(), x1, x2) -> x2 23: cond_foldr_f_z_xs(Cons(x4, x5), x1, x2) -> x1 x4 (foldr() x1 x2 x5) 24: foldr_f_z(x1, x2) x3 -> cond_foldr_f_z_xs(x3, x1, x2) 25: foldr_f(x1) x2 -> foldr_f_z(x1, x2) 26: foldr_1() x1 -> foldr_f(x1) 27: foldr() x2 -> foldr_f(x2) 28: main(x12) -> foldr() comp() id() (map() plus() x12) 0() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f :: (nat -> nat) -> (nat -> nat) -> nat -> nat foldr_f :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat map_f :: (nat -> nat -> nat) -> nat list -> nat -> nat list foldsum :: (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat list -> nat comp_f_g :: (nat -> nat) -> (nat -> nat) -> nat -> nat id :: nat -> nat plus_x :: nat -> nat -> nat foldr_f_z :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_1 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat main_1 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> nat map_1 :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus_1 :: nat -> nat -> nat main_2 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> nat main_4 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> nat main_5 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat main_6 :: nat list -> (nat list -> nat) -> nat cond_map_f_xs :: nat list -> (nat -> nat -> nat) -> nat -> nat list cond_foldr_f_z_xs :: nat -> nat list -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat cond_plus_x_y :: nat -> nat -> nat foldr :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat map :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus :: nat -> nat -> nat main :: nat list -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 8: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: foldsum(x1, x2, x3, x4, x5) x6 -> x1 x4 x5 (x3 x2 x6) 0() 3: main_5(x12, x2, x4, x6, x8) x10 -> x2 x8 x10 (x6 x4 x12) 0() 4: id() x5 -> x5 5: main_4(x12, x2, x4, x6) x8 -> x2 x8 id() (x6 x4 x12) 0() 6: comp_f_g(x4, x5) x6 -> x4 (x5 x6) 7: comp_f(x4) x5 -> comp_f_g(x4, x5) 8: comp() x4 -> comp_f(x4) 9: main_3(x12, x2, x4) x6 -> x2 comp() id() (x6 x4 x12) 0() 10: cond_map_f_xs(Nil(), x3) -> Nil() 11: cond_map_f_xs(Cons(x5, x6), x3) -> Cons(x3 x5, map() x3 x6) 12: map_f(x6) Nil() -> Nil() 13: map_f(x6) Cons(x10, x12) -> Cons(x6 x10, map() x6 x12) 14: map_1() x3 -> map_f(x3) 15: map() x6 -> map_f(x6) 16: main_2(x12, x2) x4 -> x2 comp() id() (map() x4 x12) 0() 17: cond_plus_x_y(0(), x3) -> x3 18: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 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) x4 -> x4 comp() id() (map() plus() x24) 0() 24: cond_foldr_f_z_xs(Nil(), x1, x2) -> x2 25: cond_foldr_f_z_xs(Cons(x4, x5), x1, x2) -> x1 x4 (foldr() x1 x2 x5) 26: foldr_f_z(x2, x4) Nil() -> x4 27: foldr_f_z(x2, x4) Cons(x8, x10) -> x2 x8 (foldr() x2 x4 x10) 28: foldr_f(x1) x2 -> foldr_f_z(x1, x2) 29: foldr_1() x1 -> foldr_f(x1) 30: foldr() x2 -> foldr_f(x2) 31: main(x12) -> foldr() comp() id() (map() plus() x12) 0() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f :: (nat -> nat) -> (nat -> nat) -> nat -> nat foldr_f :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat map_f :: (nat -> nat -> nat) -> nat list -> nat -> nat list foldsum :: (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat list -> nat comp_f_g :: (nat -> nat) -> (nat -> nat) -> nat -> nat id :: nat -> nat plus_x :: nat -> nat -> nat foldr_f_z :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_1 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat main_1 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> nat map_1 :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus_1 :: nat -> nat -> nat main_2 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> nat main_4 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> nat main_5 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat main_6 :: nat list -> (nat list -> nat) -> nat cond_map_f_xs :: nat list -> (nat -> nat -> nat) -> nat -> nat list cond_foldr_f_z_xs :: nat -> nat list -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat cond_plus_x_y :: nat -> nat -> nat foldr :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat map :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus :: nat -> nat -> nat main :: nat list -> nat + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 9: NeededRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: foldsum(x1, x2, x3, x4, x5) x6 -> x1 x4 x5 (x3 x2 x6) 0() 3: main_5(x12, x2, x4, x6, x8) x10 -> x2 x8 x10 (x6 x4 x12) 0() 4: id() x5 -> x5 5: main_4(x12, x2, x4, x6) x8 -> x2 x8 id() (x6 x4 x12) 0() 6: comp_f_g(x4, x5) x6 -> x4 (x5 x6) 7: comp_f(x4) x5 -> comp_f_g(x4, x5) 8: comp() x4 -> comp_f(x4) 9: main_3(x12, x2, x4) x6 -> x2 comp() id() (x6 x4 x12) 0() 12: map_f(x6) Nil() -> Nil() 13: map_f(x6) Cons(x10, x12) -> Cons(x6 x10, map() x6 x12) 14: map_1() x3 -> map_f(x3) 15: map() x6 -> map_f(x6) 16: main_2(x12, x2) x4 -> x2 comp() id() (map() x4 x12) 0() 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) x4 -> x4 comp() id() (map() plus() x24) 0() 26: foldr_f_z(x2, x4) Nil() -> x4 27: foldr_f_z(x2, x4) Cons(x8, x10) -> x2 x8 (foldr() x2 x4 x10) 28: foldr_f(x1) x2 -> foldr_f_z(x1, x2) 29: foldr_1() x1 -> foldr_f(x1) 30: foldr() x2 -> foldr_f(x2) 31: main(x12) -> foldr() comp() id() (map() plus() x12) 0() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f :: (nat -> nat) -> (nat -> nat) -> nat -> nat foldr_f :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat map_f :: (nat -> nat -> nat) -> nat list -> nat -> nat list foldsum :: (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat list -> nat comp_f_g :: (nat -> nat) -> (nat -> nat) -> nat -> nat id :: nat -> nat plus_x :: nat -> nat -> nat foldr_f_z :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_1 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat main_1 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> nat map_1 :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus_1 :: nat -> nat -> nat main_2 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> nat main_4 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> nat main_5 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat main_6 :: nat list -> (nat list -> nat) -> nat foldr :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat map :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus :: nat -> nat -> nat main :: nat list -> nat + Applied Processor: NeededRules + Details: none * Step 10: CFA WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: foldsum(x1, x2, x3, x4, x5) x6 -> x1 x4 x5 (x3 x2 x6) 0() 3: main_5(x12, x2, x4, x6, x8) x10 -> x2 x8 x10 (x6 x4 x12) 0() 4: id() x5 -> x5 5: main_4(x12, x2, x4, x6) x8 -> x2 x8 id() (x6 x4 x12) 0() 6: comp_f_g(x4, x5) x6 -> x4 (x5 x6) 7: comp_f(x4) x5 -> comp_f_g(x4, x5) 8: comp() x4 -> comp_f(x4) 9: main_3(x12, x2, x4) x6 -> x2 comp() id() (x6 x4 x12) 0() 10: map_f(x6) Nil() -> Nil() 11: map_f(x6) Cons(x10, x12) -> Cons(x6 x10, map() x6 x12) 12: map_1() x3 -> map_f(x3) 13: map() x6 -> map_f(x6) 14: main_2(x12, x2) x4 -> x2 comp() id() (map() x4 x12) 0() 15: plus_x(0()) x6 -> x6 16: plus_x(S(x8)) x6 -> S(plus() x8 x6) 17: plus_1() x2 -> plus_x(x2) 18: plus() x4 -> plus_x(x4) 19: main_1(x24) x4 -> x4 comp() id() (map() plus() x24) 0() 20: foldr_f_z(x2, x4) Nil() -> x4 21: foldr_f_z(x2, x4) Cons(x8, x10) -> x2 x8 (foldr() x2 x4 x10) 22: foldr_f(x1) x2 -> foldr_f_z(x1, x2) 23: foldr_1() x1 -> foldr_f(x1) 24: foldr() x2 -> foldr_f(x2) 25: main(x12) -> foldr() comp() id() (map() plus() x12) 0() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f :: (nat -> nat) -> (nat -> nat) -> nat -> nat foldr_f :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat map_f :: (nat -> nat -> nat) -> nat list -> nat -> nat list foldsum :: (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat list -> nat comp_f_g :: (nat -> nat) -> (nat -> nat) -> nat -> nat id :: nat -> nat plus_x :: nat -> nat -> nat foldr_f_z :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_1 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat main_1 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> nat map_1 :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus_1 :: nat -> nat -> nat main_2 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> nat main_4 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> nat main_5 :: nat list -> (((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat) -> (nat -> nat -> nat) -> ((nat -> nat -> nat) -> nat list -> nat -> nat list) -> ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat main_6 :: nat list -> (nat list -> nat) -> nat foldr :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat map :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus :: nat -> nat -> nat main :: nat list -> nat + Applied Processor: CFA {cfaRefinement = } + Details: {X{*} -> 0() | Cons(X{*},X{*}) | Nil() | 0() | S(X{*}) | S(X{*}) | 0() | 0() | Cons(X{*},X{*}) | Cons(X{*},X{*}) | Nil() | Nil() | 0() | 0() | 0() | 0() ,V{x1_22} -> V{x2_24} ,V{x2_20} -> V{x1_22} ,V{x2_21} -> V{x1_22} ,V{x2_22} -> V{x4_21} | id() ,V{x2_24} -> V{x2_21} | comp() ,V{x4_6} -> V{x4_7} ,V{x4_7} -> V{x4_8} ,V{x4_8} -> V{x8_21} ,V{x4_18} -> V{x8_16} | V{x10_11} ,V{x4_20} -> V{x2_22} ,V{x4_21} -> V{x2_22} ,V{x5_4} -> V{x6_6} | 0() ,V{x5_6} -> V{x5_7} ,V{x5_7} -> R{21} | R{20} ,V{x6_6} -> V{x6_6} | 0() ,V{x6_10} -> V{x6_13} ,V{x6_11} -> V{x6_13} ,V{x6_13} -> V{x6_11} | plus() ,V{x6_15} -> V{x6_16} | R{6} | R{4} ,V{x6_16} -> V{x6_16} | R{6} | R{4} ,V{x8_16} -> X{*} ,V{x8_21} -> @(V{x6_11},V{x10_11}) | R{18} ,V{x10_11} -> X{*} ,V{x10_21} -> @(@(map(),V{x6_11}),V{x12_11}) | @(R{13},V{x12_11}) | R{11} | R{10} ,V{x12_11} -> X{*} ,V{x12_25} -> X{*} ,R{0} -> R{25} | main(X{*}) ,R{4} -> V{x5_4} ,R{6} -> R{16} | R{15} | @(V{x4_6},R{6}) | @(V{x4_6},R{4}) | @(V{x4_6},@(V{x5_6},V{x6_6})) ,R{7} -> comp_f_g(V{x4_7},V{x5_7}) ,R{8} -> comp_f(V{x4_8}) ,R{10} -> Nil() ,R{11} -> Cons(R{18},R{10}) | Cons(R{18},R{11}) | Cons(@(V{x6_11},V{x10_11}),R{11}) | Cons(@(V{x6_11},V{x10_11}),R{10}) | Cons(R{18},@(R{13},V{x12_11})) | Cons(@(V{x6_11},V{x10_11}),@(R{13},V{x12_11})) | Cons(R{18},@(@(map(),V{x6_11}),V{x12_11})) | Cons(@(V{x6_11},V{x10_11}),@(@(map(),V{x6_11}),V{x12_11})) ,R{13} -> map_f(V{x6_13}) ,R{15} -> V{x6_15} ,R{16} -> S(R{16}) | S(R{15}) | S(@(R{18},V{x6_16})) | S(@(@(plus(),V{x8_16}),V{x6_16})) ,R{18} -> plus_x(V{x4_18}) ,R{20} -> V{x4_20} ,R{21} -> R{7} | @(R{8},R{20}) | @(R{8},R{21}) | @(@(V{x2_21},V{x8_21}),R{21}) | @(@(V{x2_21},V{x8_21}),R{20}) | @(R{8},@(R{22},V{x10_21})) | @(@(V{x2_21},V{x8_21}),@(R{22},V{x10_21})) | @(R{8},@(@(R{24},V{x4_21}),V{x10_21})) | @(@(V{x2_21},V{x8_21}),@(@(R{24},V{x4_21}),V{x10_21})) | @(R{8},@(@(@(foldr(),V{x2_21}),V{x4_21}),V{x10_21})) | @(@(V{x2_21},V{x8_21}),@(@(@(foldr(),V{x2_21}),V{x4_21}),V{x10_21})) ,R{22} -> foldr_f_z(V{x1_22},V{x2_22}) ,R{24} -> foldr_f(V{x2_24}) ,R{25} -> R{6} | R{4} | @(R{20},0()) | @(R{21},0()) | @(@(R{22},R{11}),0()) | @(@(R{22},R{10}),0()) | @(@(@(R{24},id()),R{10}),0()) | @(@(@(R{24},id()),R{11}),0()) | @(@(R{22},@(R{13},V{x12_25})),0()) | @(@(R{22},@(@(map(),plus()),V{x12_25})),0()) | @(@(@(@(foldr(),comp()),id()),R{11}),0()) | @(@(@(@(foldr(),comp()),id()),R{10}),0()) | @(@(@(R{24},id()),@(R{13},V{x12_25})),0()) | @(@(@(@(foldr(),comp()),id()),@(R{13},V{x12_25})),0()) | @(@(@(R{24},id()),@(@(map(),plus()),V{x12_25})),0()) | @(@(@(@(foldr(),comp()),id()),@(@(map(),plus()),V{x12_25})),0())} * Step 11: UncurryATRS WORST_CASE(?,O(n^1)) + Considered Problem: 4: id() 0() -> 0() 6: comp_f_g(plus_x(x3), comp_f_g(x1, x2)) 0() -> plus_x(x3) (comp_f_g(x1, x2) 0()) 7: comp_f_g(plus_x(x1), id()) 0() -> plus_x(x1) (id() 0()) 8: comp_f(x4) x5 -> comp_f_g(x4, x5) 9: comp() x4 -> comp_f(x4) 11: map_f(plus()) Nil() -> Nil() 12: map_f(plus()) Cons(x2, x1) -> Cons(plus() x2, map() plus() x1) 14: map() plus() -> map_f(plus()) 16: plus_x(0()) x6 -> x6 17: plus_x(S(x2)) x1 -> S(plus() x2 x1) 19: plus() x4 -> plus_x(x4) 21: foldr_f_z(comp(), id()) Nil() -> id() 22: foldr_f_z(comp(), id()) Cons(x2, x1) -> comp() x2 (foldr() comp() id() x1) 23: foldr_f(comp()) id() -> foldr_f_z(comp(), id()) 25: foldr() comp() -> foldr_f(comp()) 26: main(x1) -> foldr() comp() id() (map() plus() x1) 0() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f :: (nat -> nat) -> (nat -> nat) -> nat -> nat foldr_f :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat map_f :: (nat -> nat -> nat) -> nat list -> nat -> nat list comp_f_g :: (nat -> nat) -> (nat -> nat) -> nat -> nat id :: nat -> nat plus_x :: nat -> nat -> nat foldr_f_z :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat map :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus :: nat -> nat -> nat main :: nat list -> nat + Applied Processor: UncurryATRS + Details: none * Step 12: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: id#1(0()) -> 0() 2: comp_f_g#1(plus_x(x3), comp_f_g(x1, x2), 0()) -> plus_x#1(x3, comp_f_g#1(x1, x2, 0())) 3: comp_f_g#1(plus_x(x1), id(), 0()) -> plus_x#1(x1, id#1(0())) 4: comp_f#1(x4, x5) -> comp_f_g(x4, x5) 5: comp_f#2(x4, x5, x6) -> comp_f_g#1(x4, x5, x6) 6: comp#1(x4) -> comp_f(x4) 7: comp#2(x4, x5) -> comp_f#1(x4, x5) 8: comp#3(x4, x5, x6) -> comp_f#2(x4, x5, x6) 9: map_f#1(plus(), Nil()) -> Nil() 10: map_f#1(plus(), Cons(x2, x1)) -> Cons(plus#1(x2), map#2(plus(), x1)) 11: map#1(plus()) -> map_f(plus()) 12: map#2(plus(), x0) -> map_f#1(plus(), x0) 13: plus_x#1(0(), x6) -> x6 14: plus_x#1(S(x2), x1) -> S(plus#2(x2, x1)) 15: plus#1(x4) -> plus_x(x4) 16: plus#2(x4, x5) -> plus_x#1(x4, x5) 17: foldr_f_z#1(comp(), id(), Nil()) -> id() 18: foldr_f_z#2(comp(), id(), Nil(), x0) -> id#1(x0) 19: foldr_f_z#1(comp(), id(), Cons(x2, x1)) -> comp#2(x2, foldr#3(comp(), id(), x1)) 20: foldr_f_z#2(comp(), id(), Cons(x2, x1), x3) -> comp#3(x2, foldr#3(comp(), id(), x1), x3) 21: foldr_f#1(comp(), id()) -> foldr_f_z(comp(), id()) 22: foldr_f#2(comp(), id(), x0) -> foldr_f_z#1(comp(), id(), x0) 23: foldr_f#3(comp(), id(), x0, x1) -> foldr_f_z#2(comp(), id(), x0, x1) 24: foldr#1(comp()) -> foldr_f(comp()) 25: foldr#2(comp(), x0) -> foldr_f#1(comp(), x0) 26: foldr#3(comp(), x0, x1) -> foldr_f#2(comp(), x0, x1) 27: foldr#4(comp(), x0, x1, x2) -> foldr_f#3(comp(), x0, x1, x2) 28: main(x1) -> foldr#4(comp(), id(), map#2(plus(), x1), 0()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp#1 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp#2 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp#3 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f#1 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f#2 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f_g :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f_g#1 :: (nat -> nat) -> (nat -> nat) -> nat -> nat foldr#1 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr#2 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr#3 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr#4 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f#1 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f#2 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f#3 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f_z :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f_z#1 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f_z#2 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat id :: nat -> nat id#1 :: nat -> nat main :: nat list -> nat map#1 :: (nat -> nat -> nat) -> nat list -> nat -> nat list map#2 :: (nat -> nat -> nat) -> nat list -> nat -> nat list map_f :: (nat -> nat -> nat) -> nat list -> nat -> nat list map_f#1 :: (nat -> nat -> nat) -> nat list -> 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 + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 13: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: id#1(0()) -> 0() 2: comp_f_g#1(plus_x(x3), comp_f_g(x1, x2), 0()) -> plus_x#1(x3, comp_f_g#1(x1, x2, 0())) 3: comp_f_g#1(plus_x(x3), id(), 0()) -> plus_x#1(x3, 0()) 4: comp_f#1(x4, x5) -> comp_f_g(x4, x5) 5: comp_f#2(x4, x5, x6) -> comp_f_g#1(x4, x5, x6) 6: comp#1(x4) -> comp_f(x4) 7: comp#2(x4, x5) -> comp_f#1(x4, x5) 8: comp#3(x4, x5, x6) -> comp_f#2(x4, x5, x6) 9: map_f#1(plus(), Nil()) -> Nil() 10: map_f#1(plus(), Cons(x2, x1)) -> Cons(plus#1(x2), map#2(plus(), x1)) 11: map#1(plus()) -> map_f(plus()) 12: map#2(plus(), x0) -> map_f#1(plus(), x0) 13: plus_x#1(0(), x6) -> x6 14: plus_x#1(S(x2), x1) -> S(plus#2(x2, x1)) 15: plus#1(x4) -> plus_x(x4) 16: plus#2(x4, x5) -> plus_x#1(x4, x5) 17: foldr_f_z#1(comp(), id(), Nil()) -> id() 18: foldr_f_z#2(comp(), id(), Nil(), 0()) -> 0() 19: foldr_f_z#1(comp(), id(), Cons(x2, x1)) -> comp#2(x2, foldr#3(comp(), id(), x1)) 20: foldr_f_z#2(comp(), id(), Cons(x2, x1), x3) -> comp#3(x2, foldr#3(comp(), id(), x1), x3) 21: foldr_f#1(comp(), id()) -> foldr_f_z(comp(), id()) 22: foldr_f#2(comp(), id(), x0) -> foldr_f_z#1(comp(), id(), x0) 23: foldr_f#3(comp(), id(), x0, x1) -> foldr_f_z#2(comp(), id(), x0, x1) 24: foldr#1(comp()) -> foldr_f(comp()) 25: foldr#2(comp(), x0) -> foldr_f#1(comp(), x0) 26: foldr#3(comp(), x0, x1) -> foldr_f#2(comp(), x0, x1) 27: foldr#4(comp(), x0, x1, x2) -> foldr_f#3(comp(), x0, x1, x2) 28: main(x1) -> foldr#4(comp(), id(), map#2(plus(), x1), 0()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp#1 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp#2 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp#3 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f#1 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f#2 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f_g :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f_g#1 :: (nat -> nat) -> (nat -> nat) -> nat -> nat foldr#1 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr#2 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr#3 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr#4 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f#1 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f#2 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f#3 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f_z :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f_z#1 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f_z#2 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat id :: nat -> nat id#1 :: nat -> nat main :: nat list -> nat map#1 :: (nat -> nat -> nat) -> nat list -> nat -> nat list map#2 :: (nat -> nat -> nat) -> nat list -> nat -> nat list map_f :: (nat -> nat -> nat) -> nat list -> nat -> nat list map_f#1 :: (nat -> nat -> nat) -> nat list -> 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 + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 14: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 2: comp_f_g#1(plus_x(x3), comp_f_g(x1, x2), 0()) -> plus_x#1(x3, comp_f_g#1(x1, x2, 0())) 3: comp_f_g#1(plus_x(x3), id(), 0()) -> plus_x#1(x3, 0()) 4: comp_f#1(x4, x5) -> comp_f_g(x4, x5) 5: comp_f#2(x4, x5, x6) -> comp_f_g#1(x4, x5, x6) 7: comp#2(x4, x5) -> comp_f#1(x4, x5) 8: comp#3(x4, x5, x6) -> comp_f#2(x4, x5, x6) 9: map_f#1(plus(), Nil()) -> Nil() 10: map_f#1(plus(), Cons(x2, x1)) -> Cons(plus#1(x2), map#2(plus(), x1)) 12: map#2(plus(), x0) -> map_f#1(plus(), x0) 13: plus_x#1(0(), x6) -> x6 14: plus_x#1(S(x2), x1) -> S(plus#2(x2, x1)) 15: plus#1(x4) -> plus_x(x4) 16: plus#2(x4, x5) -> plus_x#1(x4, x5) 17: foldr_f_z#1(comp(), id(), Nil()) -> id() 18: foldr_f_z#2(comp(), id(), Nil(), 0()) -> 0() 19: foldr_f_z#1(comp(), id(), Cons(x2, x1)) -> comp#2(x2, foldr#3(comp(), id(), x1)) 20: foldr_f_z#2(comp(), id(), Cons(x2, x1), x3) -> comp#3(x2, foldr#3(comp(), id(), x1), x3) 22: foldr_f#2(comp(), id(), x0) -> foldr_f_z#1(comp(), id(), x0) 23: foldr_f#3(comp(), id(), x0, x1) -> foldr_f_z#2(comp(), id(), x0, x1) 26: foldr#3(comp(), x0, x1) -> foldr_f#2(comp(), x0, x1) 27: foldr#4(comp(), x0, x1, x2) -> foldr_f#3(comp(), x0, x1, x2) 28: main(x1) -> foldr#4(comp(), id(), map#2(plus(), x1), 0()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp#2 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp#3 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f#1 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f#2 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f_g :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f_g#1 :: (nat -> nat) -> (nat -> nat) -> nat -> nat foldr#3 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr#4 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f#2 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f#3 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f_z#1 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f_z#2 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat id :: nat -> nat main :: nat list -> nat map#2 :: (nat -> nat -> nat) -> nat list -> nat -> nat list map_f#1 :: (nat -> nat -> nat) -> nat list -> 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 + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 15: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: comp_f_g#1(plus_x(x3), comp_f_g(x1, x2), 0()) -> plus_x#1(x3, comp_f_g#1(x1, x2, 0())) 2: comp_f_g#1(plus_x(x3), id(), 0()) -> plus_x#1(x3, 0()) 3: comp_f#1(x4, x5) -> comp_f_g(x4, x5) 4: comp_f#2(x4, x5, x6) -> comp_f_g#1(x4, x5, x6) 5: comp#2(x8, x10) -> comp_f_g(x8, x10) 6: comp#3(x8, x10, x12) -> comp_f_g#1(x8, x10, x12) 7: map_f#1(plus(), Nil()) -> Nil() 8: map_f#1(plus(), Cons(x8, x3)) -> Cons(plus_x(x8), map#2(plus(), x3)) 9: map#2(plus(), Nil()) -> Nil() 10: map#2(plus(), Cons(x4, x2)) -> Cons(plus#1(x4), map#2(plus(), x2)) 11: plus_x#1(0(), x6) -> x6 12: plus_x#1(S(x8), x10) -> S(plus_x#1(x8, x10)) 13: plus#1(x4) -> plus_x(x4) 14: plus#2(x4, x5) -> plus_x#1(x4, x5) 15: foldr_f_z#1(comp(), id(), Nil()) -> id() 16: foldr_f_z#2(comp(), id(), Nil(), 0()) -> 0() 17: foldr_f_z#1(comp(), id(), Cons(x8, x3)) -> comp_f#1(x8, foldr#3(comp(), id(), x3)) 18: foldr_f_z#2(comp(), id(), Cons(x8, x3), x12) -> comp_f#2(x8, foldr#3(comp(), id(), x3), x12) 19: foldr_f#2(comp(), id(), Nil()) -> id() 20: foldr_f#2(comp(), id(), Cons(x4, x2)) -> comp#2(x4, foldr#3(comp(), id(), x2)) 21: foldr_f#3(comp(), id(), Nil(), 0()) -> 0() 22: foldr_f#3(comp(), id(), Cons(x4, x2), x6) -> comp#3(x4, foldr#3(comp(), id(), x2), x6) 23: foldr#3(comp(), id(), x0) -> foldr_f_z#1(comp(), id(), x0) 24: foldr#4(comp(), id(), x0, x2) -> foldr_f_z#2(comp(), id(), x0, x2) 25: main(x3) -> foldr_f#3(comp(), id(), map#2(plus(), x3), 0()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp#2 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp#3 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f#1 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f#2 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f_g :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f_g#1 :: (nat -> nat) -> (nat -> nat) -> nat -> nat foldr#3 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr#4 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f#2 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f#3 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f_z#1 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f_z#2 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat id :: nat -> nat main :: nat list -> nat map#2 :: (nat -> nat -> nat) -> nat list -> nat -> nat list map_f#1 :: (nat -> nat -> nat) -> nat list -> 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 + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 16: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: comp_f_g#1(plus_x(x3), comp_f_g(x1, x2), 0()) -> plus_x#1(x3, comp_f_g#1(x1, x2, 0())) 2: comp_f_g#1(plus_x(x3), id(), 0()) -> plus_x#1(x3, 0()) 3: comp_f#1(x4, x5) -> comp_f_g(x4, x5) 6: comp#3(x8, x10, x12) -> comp_f_g#1(x8, x10, x12) 9: map#2(plus(), Nil()) -> Nil() 10: map#2(plus(), Cons(x4, x2)) -> Cons(plus#1(x4), map#2(plus(), x2)) 11: plus_x#1(0(), x6) -> x6 12: plus_x#1(S(x8), x10) -> S(plus_x#1(x8, x10)) 13: plus#1(x4) -> plus_x(x4) 15: foldr_f_z#1(comp(), id(), Nil()) -> id() 17: foldr_f_z#1(comp(), id(), Cons(x8, x3)) -> comp_f#1(x8, foldr#3(comp(), id(), x3)) 21: foldr_f#3(comp(), id(), Nil(), 0()) -> 0() 22: foldr_f#3(comp(), id(), Cons(x4, x2), x6) -> comp#3(x4, foldr#3(comp(), id(), x2), x6) 23: foldr#3(comp(), id(), x0) -> foldr_f_z#1(comp(), id(), x0) 25: main(x3) -> foldr_f#3(comp(), id(), map#2(plus(), x3), 0()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp#3 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f#1 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f_g :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f_g#1 :: (nat -> nat) -> (nat -> nat) -> nat -> nat foldr#3 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f#3 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f_z#1 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat id :: nat -> nat main :: nat list -> nat map#2 :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus :: nat -> nat -> nat plus#1 :: nat -> nat -> nat plus_x :: nat -> nat -> nat plus_x#1 :: nat -> nat -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 17: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: comp_f_g#1(plus_x(x3), comp_f_g(x1, x2), 0()) -> plus_x#1(x3, comp_f_g#1(x1, x2, 0())) 2: comp_f_g#1(plus_x(x3), id(), 0()) -> plus_x#1(x3, 0()) 3: comp_f#1(x4, x5) -> comp_f_g(x4, x5) 4: comp#3(x8, x10, x12) -> comp_f_g#1(x8, x10, x12) 5: map#2(plus(), Nil()) -> Nil() 6: map#2(plus(), Cons(x8, x5)) -> Cons(plus_x(x8), map#2(plus(), x5)) 7: plus_x#1(0(), x6) -> x6 8: plus_x#1(S(x8), x10) -> S(plus_x#1(x8, x10)) 9: plus#1(x4) -> plus_x(x4) 10: foldr_f_z#1(comp(), id(), Nil()) -> id() 11: foldr_f_z#1(comp(), id(), Cons(x8, x7)) -> comp_f_g(x8, foldr#3(comp(), id(), x7)) 12: foldr_f#3(comp(), id(), Nil(), 0()) -> 0() 13: foldr_f#3(comp(), id(), Cons(x16, x5), x24) -> comp_f_g#1(x16, foldr#3(comp(), id(), x5), x24) 14: foldr#3(comp(), id(), Nil()) -> id() 15: foldr#3(comp(), id(), Cons(x16, x6)) -> comp_f#1(x16, foldr#3(comp(), id(), x6)) 16: main(x3) -> foldr_f#3(comp(), id(), map#2(plus(), x3), 0()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp#3 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f#1 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f_g :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f_g#1 :: (nat -> nat) -> (nat -> nat) -> nat -> nat foldr#3 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f#3 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f_z#1 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat id :: nat -> nat main :: nat list -> nat map#2 :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus :: nat -> nat -> nat plus#1 :: nat -> nat -> nat plus_x :: nat -> nat -> nat plus_x#1 :: nat -> nat -> nat + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 18: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: comp_f_g#1(plus_x(x3), comp_f_g(x1, x2), 0()) -> plus_x#1(x3, comp_f_g#1(x1, x2, 0())) 2: comp_f_g#1(plus_x(x3), id(), 0()) -> plus_x#1(x3, 0()) 3: comp_f#1(x4, x5) -> comp_f_g(x4, x5) 5: map#2(plus(), Nil()) -> Nil() 6: map#2(plus(), Cons(x8, x5)) -> Cons(plus_x(x8), map#2(plus(), x5)) 7: plus_x#1(0(), x6) -> x6 8: plus_x#1(S(x8), x10) -> S(plus_x#1(x8, x10)) 12: foldr_f#3(comp(), id(), Nil(), 0()) -> 0() 13: foldr_f#3(comp(), id(), Cons(x16, x5), x24) -> comp_f_g#1(x16, foldr#3(comp(), id(), x5), x24) 14: foldr#3(comp(), id(), Nil()) -> id() 15: foldr#3(comp(), id(), Cons(x16, x6)) -> comp_f#1(x16, foldr#3(comp(), id(), x6)) 16: main(x3) -> foldr_f#3(comp(), id(), map#2(plus(), x3), 0()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f#1 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f_g :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f_g#1 :: (nat -> nat) -> (nat -> nat) -> nat -> nat foldr#3 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f#3 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat id :: nat -> nat main :: nat list -> nat map#2 :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus :: nat -> nat -> nat plus_x :: nat -> nat -> nat plus_x#1 :: nat -> nat -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 19: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: comp_f_g#1(plus_x(x3), comp_f_g(x1, x2), 0()) -> plus_x#1(x3, comp_f_g#1(x1, x2, 0())) 2: comp_f_g#1(plus_x(x3), id(), 0()) -> plus_x#1(x3, 0()) 3: comp_f#1(x4, x5) -> comp_f_g(x4, x5) 4: map#2(plus(), Nil()) -> Nil() 5: map#2(plus(), Cons(x8, x5)) -> Cons(plus_x(x8), map#2(plus(), x5)) 6: plus_x#1(0(), x6) -> x6 7: plus_x#1(S(x8), x10) -> S(plus_x#1(x8, x10)) 8: foldr_f#3(comp(), id(), Nil(), 0()) -> 0() 9: foldr_f#3(comp(), id(), Cons(x16, x5), x24) -> comp_f_g#1(x16, foldr#3(comp(), id(), x5), x24) 10: foldr#3(comp(), id(), Nil()) -> id() 11: foldr#3(comp(), id(), Cons(x8, x13)) -> comp_f_g(x8, foldr#3(comp(), id(), x13)) 12: main(x3) -> foldr_f#3(comp(), id(), map#2(plus(), x3), 0()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f#1 :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f_g :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f_g#1 :: (nat -> nat) -> (nat -> nat) -> nat -> nat foldr#3 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f#3 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat id :: nat -> nat main :: nat list -> nat map#2 :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus :: nat -> nat -> nat plus_x :: nat -> nat -> nat plus_x#1 :: nat -> nat -> nat + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 20: Compression WORST_CASE(?,O(n^1)) + Considered Problem: 1: comp_f_g#1(plus_x(x3), comp_f_g(x1, x2), 0()) -> plus_x#1(x3, comp_f_g#1(x1, x2, 0())) 2: comp_f_g#1(plus_x(x3), id(), 0()) -> plus_x#1(x3, 0()) 4: map#2(plus(), Nil()) -> Nil() 5: map#2(plus(), Cons(x8, x5)) -> Cons(plus_x(x8), map#2(plus(), x5)) 6: plus_x#1(0(), x6) -> x6 7: plus_x#1(S(x8), x10) -> S(plus_x#1(x8, x10)) 8: foldr_f#3(comp(), id(), Nil(), 0()) -> 0() 9: foldr_f#3(comp(), id(), Cons(x16, x5), x24) -> comp_f_g#1(x16, foldr#3(comp(), id(), x5), x24) 10: foldr#3(comp(), id(), Nil()) -> id() 11: foldr#3(comp(), id(), Cons(x8, x13)) -> comp_f_g(x8, foldr#3(comp(), id(), x13)) 12: main(x3) -> foldr_f#3(comp(), id(), map#2(plus(), x3), 0()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f_g :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f_g#1 :: (nat -> nat) -> (nat -> nat) -> nat -> nat foldr#3 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat foldr_f#3 :: ((nat -> nat) -> (nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat list -> nat -> nat id :: nat -> nat main :: nat list -> nat map#2 :: (nat -> nat -> nat) -> nat list -> nat -> nat list plus :: nat -> nat -> nat plus_x :: nat -> nat -> nat plus_x#1 :: nat -> nat -> nat + Applied Processor: Compression + Details: none * Step 21: ToTctProblem WORST_CASE(?,O(n^1)) + Considered Problem: 1: comp_f_g#1(plus_x(x3), comp_f_g(x1, x2), 0()) -> plus_x#1(x3, comp_f_g#1(x1, x2, 0())) 2: comp_f_g#1(plus_x(x3), id(), 0()) -> plus_x#1(x3, 0()) 3: map#2(Nil()) -> Nil() 4: map#2(Cons(x8, x5)) -> Cons(plus_x(x8), map#2(x5)) 5: plus_x#1(0(), x6) -> x6 6: plus_x#1(S(x8), x10) -> S(plus_x#1(x8, x10)) 7: foldr_f#3(Nil(), 0()) -> 0() 8: foldr_f#3(Cons(x16, x5), x24) -> comp_f_g#1(x16, foldr#3(x5), x24) 9: foldr#3(Nil()) -> id() 10: foldr#3(Cons(x8, x13)) -> comp_f_g(x8, foldr#3(x13)) 11: main(x3) -> foldr_f#3(map#2(x3), 0()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp_f_g :: (nat -> nat) -> (nat -> nat) -> nat -> nat comp_f_g#1 :: (nat -> nat) -> (nat -> nat) -> nat -> nat foldr#3 :: nat -> nat list -> nat -> nat foldr_f#3 :: nat -> nat list -> nat -> nat id :: nat -> nat main :: nat list -> nat map#2 :: nat list -> nat -> nat list plus_x :: nat -> nat -> nat plus_x#1 :: nat -> nat -> nat + Applied Processor: ToTctProblem + Details: none * Step 22: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: comp_f_g#1(plus_x(x3),comp_f_g(x1,x2),0()) -> plus_x#1(x3,comp_f_g#1(x1,x2,0())) comp_f_g#1(plus_x(x3),id(),0()) -> plus_x#1(x3,0()) foldr#3(Cons(x8,x13)) -> comp_f_g(x8,foldr#3(x13)) foldr#3(Nil()) -> id() foldr_f#3(Cons(x16,x5),x24) -> comp_f_g#1(x16,foldr#3(x5),x24) foldr_f#3(Nil(),0()) -> 0() main(x3) -> foldr_f#3(map#2(x3),0()) map#2(Cons(x8,x5)) -> Cons(plus_x(x8),map#2(x5)) map#2(Nil()) -> Nil() plus_x#1(0(),x6) -> x6 plus_x#1(S(x8),x10) -> S(plus_x#1(x8,x10)) - Signature: {comp_f_g#1/3,foldr#3/1,foldr_f#3/2,main/1,map#2/1,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,comp_f_g/2,id/0 ,plus_x/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,Cons,Nil,S} + Applied Processor: Ara {minDegree = 1, maxDegree = 2, araTimeout = 3, araRuleShifting = Nothing} + Details: Signatures used: ---------------- F (TrsFun "0") :: [] -(0)-> "A"(1) F (TrsFun "0") :: [] -(0)-> "A"(14) F (TrsFun "0") :: [] -(0)-> "A"(15) F (TrsFun "0") :: [] -(0)-> "A"(7) F (TrsFun "Cons") :: ["A"(13) x "A"(13)] -(13)-> "A"(13) F (TrsFun "Cons") :: ["A"(15) x "A"(15)] -(15)-> "A"(15) F (TrsFun "Nil") :: [] -(0)-> "A"(13) F (TrsFun "Nil") :: [] -(0)-> "A"(15) F (TrsFun "S") :: ["A"(1)] -(1)-> "A"(1) F (TrsFun "S") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "comp_f_g") :: ["A"(8) x "A"(8)] -(8)-> "A"(8) F (TrsFun "comp_f_g#1") :: ["A"(8) x "A"(8) x "A"(1)] -(3)-> "A"(0) F (TrsFun "foldr#3") :: ["A"(13)] -(3)-> "A"(8) F (TrsFun "foldr_f#3") :: ["A"(13) x "A"(14)] -(3)-> "A"(0) F (TrsFun "id") :: [] -(0)-> "A"(8) F (TrsFun "id") :: [] -(0)-> "A"(15) F (TrsFun "main") :: ["A"(15)] -(16)-> "A"(0) F (TrsFun "map#2") :: ["A"(15)] -(8)-> "A"(13) F (TrsFun "plus_x") :: ["A"(8)] -(0)-> "A"(8) F (TrsFun "plus_x") :: ["A"(13)] -(0)-> "A"(13) F (TrsFun "plus_x#1") :: ["A"(1) x "A"(0)] -(1)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "F (TrsFun \"0\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"Cons\")_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "F (TrsFun \"Nil\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"S\")_A" :: ["A"(1)] -(1)-> "A"(1) "F (TrsFun \"comp_f_g\")_A" :: ["A"(0) x "A"(0)] -(1)-> "A"(1) "F (TrsFun \"id\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"plus_x\")_A" :: ["A"(0)] -(0)-> "A"(1) WORST_CASE(?,O(n^1))