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: NaturalMI 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: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(Cons) = {2}, uargs(S) = {1}, uargs(comp_f_g) = {2}, uargs(comp_f_g#1) = {2}, uargs(foldr_f#3) = {1}, uargs(plus_x#1) = {2} Following symbols are considered usable: {comp_f_g#1,foldr#3,foldr_f#3,main,map#2,plus_x#1} TcT has computed the following interpretation: p(0) = [3] p(Cons) = [1] x2 + [0] p(Nil) = [0] p(S) = [1] x1 + [0] p(comp_f_g) = [2] x2 + [0] p(comp_f_g#1) = [1] x2 + [2] x3 + [1] p(foldr#3) = [0] p(foldr_f#3) = [1] x1 + [3] x2 + [6] p(id) = [0] p(main) = [15] p(map#2) = [0] p(plus_x) = [1] x1 + [8] p(plus_x#1) = [1] x2 + [0] Following rules are strictly oriented: comp_f_g#1(plus_x(x3),id(),0()) = [7] > [3] = plus_x#1(x3,0()) foldr_f#3(Cons(x16,x5),x24) = [3] x24 + [1] x5 + [6] > [2] x24 + [1] = comp_f_g#1(x16,foldr#3(x5),x24) foldr_f#3(Nil(),0()) = [15] > [3] = 0() Following rules are (at-least) weakly oriented: comp_f_g#1(plus_x(x3),comp_f_g(x1,x2),0()) = [2] x2 + [7] >= [1] x2 + [7] = plus_x#1(x3,comp_f_g#1(x1,x2,0())) foldr#3(Cons(x8,x13)) = [0] >= [0] = comp_f_g(x8,foldr#3(x13)) foldr#3(Nil()) = [0] >= [0] = id() main(x3) = [15] >= [15] = foldr_f#3(map#2(x3),0()) map#2(Cons(x8,x5)) = [0] >= [0] = Cons(plus_x(x8),map#2(x5)) map#2(Nil()) = [0] >= [0] = Nil() plus_x#1(0(),x6) = [1] x6 + [0] >= [1] x6 + [0] = x6 plus_x#1(S(x8),x10) = [1] x10 + [0] >= [1] x10 + [0] = S(plus_x#1(x8,x10)) * Step 23: NaturalMI 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())) foldr#3(Cons(x8,x13)) -> comp_f_g(x8,foldr#3(x13)) foldr#3(Nil()) -> id() 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)) - Weak TRS: comp_f_g#1(plus_x(x3),id(),0()) -> plus_x#1(x3,0()) foldr_f#3(Cons(x16,x5),x24) -> comp_f_g#1(x16,foldr#3(x5),x24) foldr_f#3(Nil(),0()) -> 0() - 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: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(Cons) = {2}, uargs(S) = {1}, uargs(comp_f_g) = {2}, uargs(comp_f_g#1) = {2}, uargs(foldr_f#3) = {1}, uargs(plus_x#1) = {2} Following symbols are considered usable: {comp_f_g#1,foldr#3,foldr_f#3,main,map#2,plus_x#1} TcT has computed the following interpretation: p(0) = [0] p(Cons) = [1] x1 + [1] x2 + [0] p(Nil) = [0] p(S) = [1] x1 + [0] p(comp_f_g) = [8] x2 + [0] p(comp_f_g#1) = [1] x2 + [0] p(foldr#3) = [0] p(foldr_f#3) = [8] x1 + [14] p(id) = [0] p(main) = [8] x1 + [15] p(map#2) = [1] x1 + [0] p(plus_x) = [1] x1 + [0] p(plus_x#1) = [8] x2 + [0] Following rules are strictly oriented: main(x3) = [8] x3 + [15] > [8] x3 + [14] = foldr_f#3(map#2(x3),0()) Following rules are (at-least) weakly oriented: comp_f_g#1(plus_x(x3),comp_f_g(x1,x2),0()) = [8] x2 + [0] >= [8] x2 + [0] = plus_x#1(x3,comp_f_g#1(x1,x2,0())) comp_f_g#1(plus_x(x3),id(),0()) = [0] >= [0] = plus_x#1(x3,0()) foldr#3(Cons(x8,x13)) = [0] >= [0] = comp_f_g(x8,foldr#3(x13)) foldr#3(Nil()) = [0] >= [0] = id() foldr_f#3(Cons(x16,x5),x24) = [8] x16 + [8] x5 + [14] >= [0] = comp_f_g#1(x16,foldr#3(x5),x24) foldr_f#3(Nil(),0()) = [14] >= [0] = 0() map#2(Cons(x8,x5)) = [1] x5 + [1] x8 + [0] >= [1] x5 + [1] x8 + [0] = Cons(plus_x(x8),map#2(x5)) map#2(Nil()) = [0] >= [0] = Nil() plus_x#1(0(),x6) = [8] x6 + [0] >= [1] x6 + [0] = x6 plus_x#1(S(x8),x10) = [8] x10 + [0] >= [8] x10 + [0] = S(plus_x#1(x8,x10)) * Step 24: NaturalPI 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())) foldr#3(Cons(x8,x13)) -> comp_f_g(x8,foldr#3(x13)) foldr#3(Nil()) -> id() 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)) - Weak TRS: comp_f_g#1(plus_x(x3),id(),0()) -> plus_x#1(x3,0()) 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()) - 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: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(Cons) = {2}, uargs(S) = {1}, uargs(comp_f_g) = {2}, uargs(comp_f_g#1) = {2}, uargs(foldr_f#3) = {1}, uargs(plus_x#1) = {2} Following symbols are considered usable: {comp_f_g#1,foldr#3,foldr_f#3,main,map#2,plus_x#1} TcT has computed the following interpretation: p(0) = 0 p(Cons) = 4 + x1 + x2 p(Nil) = 2 p(S) = x1 p(comp_f_g) = 8 + x1 + x2 p(comp_f_g#1) = x1 + 2*x2 p(foldr#3) = 1 + 2*x1 p(foldr_f#3) = 4*x1 p(id) = 1 p(main) = 6 + 11*x1 p(map#2) = 1 + x1 p(plus_x) = 0 p(plus_x#1) = 2 + x2 Following rules are strictly oriented: comp_f_g#1(plus_x(x3),comp_f_g(x1,x2),0()) = 16 + 2*x1 + 2*x2 > 2 + x1 + 2*x2 = plus_x#1(x3,comp_f_g#1(x1,x2,0())) foldr#3(Nil()) = 5 > 1 = id() map#2(Nil()) = 3 > 2 = Nil() plus_x#1(0(),x6) = 2 + x6 > x6 = x6 Following rules are (at-least) weakly oriented: comp_f_g#1(plus_x(x3),id(),0()) = 2 >= 2 = plus_x#1(x3,0()) foldr#3(Cons(x8,x13)) = 9 + 2*x13 + 2*x8 >= 9 + 2*x13 + x8 = comp_f_g(x8,foldr#3(x13)) foldr_f#3(Cons(x16,x5),x24) = 16 + 4*x16 + 4*x5 >= 2 + x16 + 4*x5 = comp_f_g#1(x16,foldr#3(x5),x24) foldr_f#3(Nil(),0()) = 8 >= 0 = 0() main(x3) = 6 + 11*x3 >= 4 + 4*x3 = foldr_f#3(map#2(x3),0()) map#2(Cons(x8,x5)) = 5 + x5 + x8 >= 5 + x5 = Cons(plus_x(x8),map#2(x5)) plus_x#1(S(x8),x10) = 2 + x10 >= 2 + x10 = S(plus_x#1(x8,x10)) * Step 25: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: foldr#3(Cons(x8,x13)) -> comp_f_g(x8,foldr#3(x13)) map#2(Cons(x8,x5)) -> Cons(plus_x(x8),map#2(x5)) plus_x#1(S(x8),x10) -> S(plus_x#1(x8,x10)) - Weak 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(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(Nil()) -> Nil() plus_x#1(0(),x6) -> x6 - 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: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(Cons) = {2}, uargs(S) = {1}, uargs(comp_f_g) = {2}, uargs(comp_f_g#1) = {2}, uargs(foldr_f#3) = {1}, uargs(plus_x#1) = {2} Following symbols are considered usable: {comp_f_g#1,foldr#3,foldr_f#3,main,map#2,plus_x#1} TcT has computed the following interpretation: p(0) = 5 p(Cons) = 9 + x1 + x2 p(Nil) = 0 p(S) = x1 p(comp_f_g) = x2 p(comp_f_g#1) = 10 + 8*x2 p(foldr#3) = 2 p(foldr_f#3) = 8 + 2*x1 p(id) = 1 p(main) = 15 + 12*x1 p(map#2) = 3 + 3*x1 p(plus_x) = 9 p(plus_x#1) = x2 Following rules are strictly oriented: map#2(Cons(x8,x5)) = 30 + 3*x5 + 3*x8 > 21 + 3*x5 = Cons(plus_x(x8),map#2(x5)) Following rules are (at-least) weakly oriented: comp_f_g#1(plus_x(x3),comp_f_g(x1,x2),0()) = 10 + 8*x2 >= 10 + 8*x2 = plus_x#1(x3,comp_f_g#1(x1,x2,0())) comp_f_g#1(plus_x(x3),id(),0()) = 18 >= 5 = plus_x#1(x3,0()) foldr#3(Cons(x8,x13)) = 2 >= 2 = comp_f_g(x8,foldr#3(x13)) foldr#3(Nil()) = 2 >= 1 = id() foldr_f#3(Cons(x16,x5),x24) = 26 + 2*x16 + 2*x5 >= 26 = comp_f_g#1(x16,foldr#3(x5),x24) foldr_f#3(Nil(),0()) = 8 >= 5 = 0() main(x3) = 15 + 12*x3 >= 14 + 6*x3 = foldr_f#3(map#2(x3),0()) map#2(Nil()) = 3 >= 0 = Nil() plus_x#1(0(),x6) = x6 >= x6 = x6 plus_x#1(S(x8),x10) = x10 >= x10 = S(plus_x#1(x8,x10)) * Step 26: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: foldr#3(Cons(x8,x13)) -> comp_f_g(x8,foldr#3(x13)) plus_x#1(S(x8),x10) -> S(plus_x#1(x8,x10)) - Weak 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(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 - 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: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(Cons) = {2}, uargs(S) = {1}, uargs(comp_f_g) = {2}, uargs(comp_f_g#1) = {2}, uargs(foldr_f#3) = {1}, uargs(plus_x#1) = {2} Following symbols are considered usable: {comp_f_g#1,foldr#3,foldr_f#3,main,map#2,plus_x#1} TcT has computed the following interpretation: p(0) = [1] p(Cons) = [1] x2 + [4] p(Nil) = [2] p(S) = [1] x1 + [0] p(comp_f_g) = [1] x2 + [2] p(comp_f_g#1) = [2] x2 + [1] x3 + [4] p(foldr#3) = [1] x1 + [0] p(foldr_f#3) = [2] x1 + [1] x2 + [0] p(id) = [0] p(main) = [6] x1 + [10] p(map#2) = [3] x1 + [4] p(plus_x) = [8] x1 + [0] p(plus_x#1) = [1] x2 + [0] Following rules are strictly oriented: foldr#3(Cons(x8,x13)) = [1] x13 + [4] > [1] x13 + [2] = comp_f_g(x8,foldr#3(x13)) Following rules are (at-least) weakly oriented: comp_f_g#1(plus_x(x3),comp_f_g(x1,x2),0()) = [2] x2 + [9] >= [2] x2 + [5] = plus_x#1(x3,comp_f_g#1(x1,x2,0())) comp_f_g#1(plus_x(x3),id(),0()) = [5] >= [1] = plus_x#1(x3,0()) foldr#3(Nil()) = [2] >= [0] = id() foldr_f#3(Cons(x16,x5),x24) = [1] x24 + [2] x5 + [8] >= [1] x24 + [2] x5 + [4] = comp_f_g#1(x16,foldr#3(x5),x24) foldr_f#3(Nil(),0()) = [5] >= [1] = 0() main(x3) = [6] x3 + [10] >= [6] x3 + [9] = foldr_f#3(map#2(x3),0()) map#2(Cons(x8,x5)) = [3] x5 + [16] >= [3] x5 + [8] = Cons(plus_x(x8),map#2(x5)) map#2(Nil()) = [10] >= [2] = Nil() plus_x#1(0(),x6) = [1] x6 + [0] >= [1] x6 + [0] = x6 plus_x#1(S(x8),x10) = [1] x10 + [0] >= [1] x10 + [0] = S(plus_x#1(x8,x10)) * Step 27: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: plus_x#1(S(x8),x10) -> S(plus_x#1(x8,x10)) - Weak 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 - 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: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(Cons) = {2}, uargs(S) = {1}, uargs(comp_f_g) = {2}, uargs(comp_f_g#1) = {2}, uargs(foldr_f#3) = {1}, uargs(plus_x#1) = {2} Following symbols are considered usable: {comp_f_g#1,foldr#3,foldr_f#3,main,map#2,plus_x#1} TcT has computed the following interpretation: p(0) = 8 p(Cons) = 2 + x1 + x2 p(Nil) = 2 p(S) = 8 + x1 p(comp_f_g) = 1 + x1 + x2 p(comp_f_g#1) = 14 + 8*x1 + 8*x2 + x3 p(foldr#3) = x1 p(foldr_f#3) = 10*x1 + x2 p(id) = 0 p(main) = 8 + 15*x1 p(map#2) = x1 p(plus_x) = x1 p(plus_x#1) = 8 + 2*x1 + x2 Following rules are strictly oriented: plus_x#1(S(x8),x10) = 24 + x10 + 2*x8 > 16 + x10 + 2*x8 = S(plus_x#1(x8,x10)) Following rules are (at-least) weakly oriented: comp_f_g#1(plus_x(x3),comp_f_g(x1,x2),0()) = 30 + 8*x1 + 8*x2 + 8*x3 >= 30 + 8*x1 + 8*x2 + 2*x3 = plus_x#1(x3,comp_f_g#1(x1,x2,0())) comp_f_g#1(plus_x(x3),id(),0()) = 22 + 8*x3 >= 16 + 2*x3 = plus_x#1(x3,0()) foldr#3(Cons(x8,x13)) = 2 + x13 + x8 >= 1 + x13 + x8 = comp_f_g(x8,foldr#3(x13)) foldr#3(Nil()) = 2 >= 0 = id() foldr_f#3(Cons(x16,x5),x24) = 20 + 10*x16 + x24 + 10*x5 >= 14 + 8*x16 + x24 + 8*x5 = comp_f_g#1(x16,foldr#3(x5),x24) foldr_f#3(Nil(),0()) = 28 >= 8 = 0() main(x3) = 8 + 15*x3 >= 8 + 10*x3 = foldr_f#3(map#2(x3),0()) map#2(Cons(x8,x5)) = 2 + x5 + x8 >= 2 + x5 + x8 = Cons(plus_x(x8),map#2(x5)) map#2(Nil()) = 2 >= 2 = Nil() plus_x#1(0(),x6) = 24 + x6 >= x6 = x6 * Step 28: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak 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: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))