WORST_CASE(?,O(n^2)) * Step 1: Desugar WORST_CASE(?,O(n^2)) + Considered Problem: type nat = 0 | S of nat ;; type 'a list = Nil | Cons of 'a * 'a list ;; let rec map f xs = match xs with | Nil -> Nil | Cons(x,xs') -> Cons(f x, map f xs') ;; let rec plus x y = match x with | 0 -> y | S(x') -> S(plus x' y) ;; let mapplus l x = map (plus x) l ;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization WORST_CASE(?,O(n^2)) + Considered Problem: λl : nat list. λx : nat. (λmap : (nat -> nat) -> nat list -> nat list. (λplus : nat -> nat -> nat. (λmapplus : nat list -> nat -> nat list. mapplus l x) (λl : nat list. λx : nat. map (plus x) l)) (μplus : nat -> nat -> nat. λx : nat. λy : nat. case x of | 0 -> y | S -> λx' : nat. S(plus x' y))) (μmap : (nat -> nat) -> nat list -> nat list. λf : nat -> nat. λxs : nat list. case xs of | Nil -> Nil | Cons -> λx : nat. λxs' : nat list. Cons(f x,map f xs')) : nat list -> nat -> nat list 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^2)) + Considered Problem: 1: main_4(x0, x1) x4 -> x4 x0 x1 2: mapplus_l(x2, x3, x4) x5 -> x2 (x3 x5) x4 3: mapplus(x2, x3) x4 -> mapplus_l(x2, x3, x4) 4: main_3(x0, x1, x2) x3 -> main_4(x0, x1) mapplus(x2, x3) 5: cond_plus_x_y(0(), x4) -> x4 6: cond_plus_x_y(S(x5), x4) -> S(plus() x5 x4) 7: plus_x(x3) x4 -> cond_plus_x_y(x3, x4) 8: plus_1() x3 -> plus_x(x3) 9: plus() x0 -> plus_1() x0 10: main_2(x0, x1) x2 -> main_3(x0, x1, x2) plus() 11: cond_map_f_xs(Nil(), x2) -> Nil() 12: cond_map_f_xs(Cons(x4, x5), x2) -> Cons(x2 x4, map() x2 x5) 13: map_f(x2) x3 -> cond_map_f_xs(x3, x2) 14: map_1() x2 -> map_f(x2) 15: map() x0 -> map_1() x0 16: main(x0, x1) -> main_2(x0, x1) map() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat map_f :: (nat -> nat) -> nat list -> nat list mapplus_l :: ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list -> nat -> nat list mapplus :: ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list -> nat -> nat list plus_x :: nat -> nat -> nat map_1 :: (nat -> nat) -> nat list -> nat list plus_1 :: nat -> nat -> nat main_2 :: nat list -> nat -> ((nat -> nat) -> nat list -> nat list) -> nat list main_3 :: nat list -> nat -> ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list main_4 :: nat list -> nat -> (nat list -> nat -> nat list) -> nat list cond_map_f_xs :: nat list -> (nat -> nat) -> nat list cond_plus_x_y :: nat -> nat -> nat map :: (nat -> nat) -> nat list -> nat list plus :: nat -> nat -> nat main :: nat list -> nat -> nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_4(x0, x1) x4 -> x4 x0 x1 2: mapplus_l(x2, x3, x4) x5 -> x2 (x3 x5) x4 3: mapplus(x2, x3) x4 -> mapplus_l(x2, x3, x4) 4: main_3(x0, x2, x5) x7 -> mapplus(x5, x7) x0 x2 5: cond_plus_x_y(0(), x4) -> x4 6: cond_plus_x_y(S(x5), x4) -> S(plus() x5 x4) 7: plus_x(x3) x4 -> cond_plus_x_y(x3, x4) 8: plus_1() x3 -> plus_x(x3) 9: plus() x6 -> plus_x(x6) 10: main_2(x0, x2) x4 -> main_4(x0, x2) mapplus(x4, plus()) 11: cond_map_f_xs(Nil(), x2) -> Nil() 12: cond_map_f_xs(Cons(x4, x5), x2) -> Cons(x2 x4, map() x2 x5) 13: map_f(x2) x3 -> cond_map_f_xs(x3, x2) 14: map_1() x2 -> map_f(x2) 15: map() x4 -> map_f(x4) 16: main(x0, x2) -> main_3(x0, x2, map()) plus() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat map_f :: (nat -> nat) -> nat list -> nat list mapplus_l :: ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list -> nat -> nat list mapplus :: ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list -> nat -> nat list plus_x :: nat -> nat -> nat map_1 :: (nat -> nat) -> nat list -> nat list plus_1 :: nat -> nat -> nat main_2 :: nat list -> nat -> ((nat -> nat) -> nat list -> nat list) -> nat list main_3 :: nat list -> nat -> ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list main_4 :: nat list -> nat -> (nat list -> nat -> nat list) -> nat list cond_map_f_xs :: nat list -> (nat -> nat) -> nat list cond_plus_x_y :: nat -> nat -> nat map :: (nat -> nat) -> nat list -> nat list plus :: nat -> nat -> nat main :: nat list -> nat -> nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 5: Inline WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_4(x0, x1) x4 -> x4 x0 x1 2: mapplus_l(x2, x3, x4) x5 -> x2 (x3 x5) x4 3: mapplus(x2, x3) x4 -> mapplus_l(x2, x3, x4) 4: main_3(x8, x5, x4) x6 -> mapplus_l(x4, x6, x8) x5 5: cond_plus_x_y(0(), x4) -> x4 6: cond_plus_x_y(S(x5), x4) -> S(plus() x5 x4) 7: plus_x(x3) x4 -> cond_plus_x_y(x3, x4) 8: plus_1() x3 -> plus_x(x3) 9: plus() x6 -> plus_x(x6) 10: main_2(x0, x2) x9 -> mapplus(x9, plus()) x0 x2 11: cond_map_f_xs(Nil(), x2) -> Nil() 12: cond_map_f_xs(Cons(x4, x5), x2) -> Cons(x2 x4, map() x2 x5) 13: map_f(x2) x3 -> cond_map_f_xs(x3, x2) 14: map_1() x2 -> map_f(x2) 15: map() x4 -> map_f(x4) 16: main(x0, x4) -> mapplus(map(), plus()) x0 x4 where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat map_f :: (nat -> nat) -> nat list -> nat list mapplus_l :: ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list -> nat -> nat list mapplus :: ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list -> nat -> nat list plus_x :: nat -> nat -> nat map_1 :: (nat -> nat) -> nat list -> nat list plus_1 :: nat -> nat -> nat main_2 :: nat list -> nat -> ((nat -> nat) -> nat list -> nat list) -> nat list main_3 :: nat list -> nat -> ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list main_4 :: nat list -> nat -> (nat list -> nat -> nat list) -> nat list cond_map_f_xs :: nat list -> (nat -> nat) -> nat list cond_plus_x_y :: nat -> nat -> nat map :: (nat -> nat) -> nat list -> nat list plus :: nat -> nat -> nat main :: nat list -> nat -> nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 6: Inline WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_4(x0, x1) x4 -> x4 x0 x1 2: mapplus_l(x2, x3, x4) x5 -> x2 (x3 x5) x4 3: mapplus(x2, x3) x4 -> mapplus_l(x2, x3, x4) 4: main_3(x8, x10, x4) x6 -> x4 (x6 x10) x8 5: cond_plus_x_y(0(), x4) -> x4 6: cond_plus_x_y(S(x5), x4) -> S(plus() x5 x4) 7: plus_x(x3) x4 -> cond_plus_x_y(x3, x4) 8: plus_1() x3 -> plus_x(x3) 9: plus() x6 -> plus_x(x6) 10: main_2(x8, x5) x4 -> mapplus_l(x4, plus(), x8) x5 11: cond_map_f_xs(Nil(), x2) -> Nil() 12: cond_map_f_xs(Cons(x4, x5), x2) -> Cons(x2 x4, map() x2 x5) 13: map_f(x2) x3 -> cond_map_f_xs(x3, x2) 14: map_1() x2 -> map_f(x2) 15: map() x4 -> map_f(x4) 16: main(x8, x9) -> mapplus_l(map(), plus(), x8) x9 where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat map_f :: (nat -> nat) -> nat list -> nat list mapplus_l :: ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list -> nat -> nat list mapplus :: ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list -> nat -> nat list plus_x :: nat -> nat -> nat map_1 :: (nat -> nat) -> nat list -> nat list plus_1 :: nat -> nat -> nat main_2 :: nat list -> nat -> ((nat -> nat) -> nat list -> nat list) -> nat list main_3 :: nat list -> nat -> ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list main_4 :: nat list -> nat -> (nat list -> nat -> nat list) -> nat list cond_map_f_xs :: nat list -> (nat -> nat) -> nat list cond_plus_x_y :: nat -> nat -> nat map :: (nat -> nat) -> nat list -> nat list plus :: nat -> nat -> nat main :: nat list -> nat -> nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 7: Inline WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_4(x0, x1) x4 -> x4 x0 x1 2: mapplus_l(x2, x3, x4) x5 -> x2 (x3 x5) x4 3: mapplus(x2, x3) x4 -> mapplus_l(x2, x3, x4) 4: main_3(x8, x10, x4) x6 -> x4 (x6 x10) x8 5: cond_plus_x_y(0(), x4) -> x4 6: cond_plus_x_y(S(x5), x4) -> S(plus() x5 x4) 7: plus_x(x3) x4 -> cond_plus_x_y(x3, x4) 8: plus_1() x3 -> plus_x(x3) 9: plus() x6 -> plus_x(x6) 10: main_2(x8, x10) x4 -> x4 (plus() x10) x8 11: cond_map_f_xs(Nil(), x2) -> Nil() 12: cond_map_f_xs(Cons(x4, x5), x2) -> Cons(x2 x4, map() x2 x5) 13: map_f(x2) x3 -> cond_map_f_xs(x3, x2) 14: map_1() x2 -> map_f(x2) 15: map() x4 -> map_f(x4) 16: main(x8, x10) -> map() (plus() x10) x8 where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat map_f :: (nat -> nat) -> nat list -> nat list mapplus_l :: ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list -> nat -> nat list mapplus :: ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list -> nat -> nat list plus_x :: nat -> nat -> nat map_1 :: (nat -> nat) -> nat list -> nat list plus_1 :: nat -> nat -> nat main_2 :: nat list -> nat -> ((nat -> nat) -> nat list -> nat list) -> nat list main_3 :: nat list -> nat -> ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list main_4 :: nat list -> nat -> (nat list -> nat -> nat list) -> nat list cond_map_f_xs :: nat list -> (nat -> nat) -> nat list cond_plus_x_y :: nat -> nat -> nat map :: (nat -> nat) -> nat list -> nat list plus :: nat -> nat -> nat main :: nat list -> nat -> nat list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 8: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_4(x0, x1) x4 -> x4 x0 x1 2: mapplus_l(x2, x3, x4) x5 -> x2 (x3 x5) x4 3: mapplus(x2, x3) x4 -> mapplus_l(x2, x3, x4) 4: main_3(x8, x10, x4) x6 -> x4 (x6 x10) x8 5: cond_plus_x_y(0(), x4) -> x4 6: cond_plus_x_y(S(x5), x4) -> S(plus() x5 x4) 7: plus_x(0()) x8 -> x8 8: plus_x(S(x10)) x8 -> S(plus() x10 x8) 9: plus_1() x3 -> plus_x(x3) 10: plus() x6 -> plus_x(x6) 11: main_2(x8, x10) x4 -> x4 (plus() x10) x8 12: cond_map_f_xs(Nil(), x2) -> Nil() 13: cond_map_f_xs(Cons(x4, x5), x2) -> Cons(x2 x4, map() x2 x5) 14: map_f(x4) Nil() -> Nil() 15: map_f(x4) Cons(x8, x10) -> Cons(x4 x8, map() x4 x10) 16: map_1() x2 -> map_f(x2) 17: map() x4 -> map_f(x4) 18: main(x8, x10) -> map() (plus() x10) x8 where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat map_f :: (nat -> nat) -> nat list -> nat list mapplus_l :: ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list -> nat -> nat list mapplus :: ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list -> nat -> nat list plus_x :: nat -> nat -> nat map_1 :: (nat -> nat) -> nat list -> nat list plus_1 :: nat -> nat -> nat main_2 :: nat list -> nat -> ((nat -> nat) -> nat list -> nat list) -> nat list main_3 :: nat list -> nat -> ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list main_4 :: nat list -> nat -> (nat list -> nat -> nat list) -> nat list cond_map_f_xs :: nat list -> (nat -> nat) -> nat list cond_plus_x_y :: nat -> nat -> nat map :: (nat -> nat) -> nat list -> nat list plus :: nat -> nat -> nat main :: nat list -> nat -> nat list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 9: NeededRules WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_4(x0, x1) x4 -> x4 x0 x1 2: mapplus_l(x2, x3, x4) x5 -> x2 (x3 x5) x4 3: mapplus(x2, x3) x4 -> mapplus_l(x2, x3, x4) 4: main_3(x8, x10, x4) x6 -> x4 (x6 x10) x8 7: plus_x(0()) x8 -> x8 8: plus_x(S(x10)) x8 -> S(plus() x10 x8) 9: plus_1() x3 -> plus_x(x3) 10: plus() x6 -> plus_x(x6) 11: main_2(x8, x10) x4 -> x4 (plus() x10) x8 14: map_f(x4) Nil() -> Nil() 15: map_f(x4) Cons(x8, x10) -> Cons(x4 x8, map() x4 x10) 16: map_1() x2 -> map_f(x2) 17: map() x4 -> map_f(x4) 18: main(x8, x10) -> map() (plus() x10) x8 where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat map_f :: (nat -> nat) -> nat list -> nat list mapplus_l :: ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list -> nat -> nat list mapplus :: ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list -> nat -> nat list plus_x :: nat -> nat -> nat map_1 :: (nat -> nat) -> nat list -> nat list plus_1 :: nat -> nat -> nat main_2 :: nat list -> nat -> ((nat -> nat) -> nat list -> nat list) -> nat list main_3 :: nat list -> nat -> ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list main_4 :: nat list -> nat -> (nat list -> nat -> nat list) -> nat list map :: (nat -> nat) -> nat list -> nat list plus :: nat -> nat -> nat main :: nat list -> nat -> nat list + Applied Processor: NeededRules + Details: none * Step 10: CFA WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_4(x0, x1) x4 -> x4 x0 x1 2: mapplus_l(x2, x3, x4) x5 -> x2 (x3 x5) x4 3: mapplus(x2, x3) x4 -> mapplus_l(x2, x3, x4) 4: main_3(x8, x10, x4) x6 -> x4 (x6 x10) x8 5: plus_x(0()) x8 -> x8 6: plus_x(S(x10)) x8 -> S(plus() x10 x8) 7: plus_1() x3 -> plus_x(x3) 8: plus() x6 -> plus_x(x6) 9: main_2(x8, x10) x4 -> x4 (plus() x10) x8 10: map_f(x4) Nil() -> Nil() 11: map_f(x4) Cons(x8, x10) -> Cons(x4 x8, map() x4 x10) 12: map_1() x2 -> map_f(x2) 13: map() x4 -> map_f(x4) 14: main(x8, x10) -> map() (plus() x10) x8 where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat map_f :: (nat -> nat) -> nat list -> nat list mapplus_l :: ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list -> nat -> nat list mapplus :: ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list -> nat -> nat list plus_x :: nat -> nat -> nat map_1 :: (nat -> nat) -> nat list -> nat list plus_1 :: nat -> nat -> nat main_2 :: nat list -> nat -> ((nat -> nat) -> nat list -> nat list) -> nat list main_3 :: nat list -> nat -> ((nat -> nat) -> nat list -> nat list) -> (nat -> nat -> nat) -> nat list main_4 :: nat list -> nat -> (nat list -> nat -> nat list) -> nat list map :: (nat -> nat) -> nat list -> nat list plus :: nat -> nat -> nat main :: nat list -> nat -> nat list + Applied Processor: CFA {cfaRefinement = } + Details: {X{*} -> Cons(X{*},X{*}) | Cons(X{*},X{*}) | Nil() | Nil() | S(X{*}) | S(X{*}) | 0() ,V{x4_10} -> V{x4_13} ,V{x4_11} -> V{x4_13} ,V{x4_13} -> V{x4_11} | R{8} ,V{x6_8} -> V{x10_6} | V{x10_14} ,V{x8_5} -> V{x8_6} | V{x8_11} ,V{x8_6} -> V{x8_6} | V{x8_11} ,V{x8_11} -> X{*} ,V{x8_14} -> X{*} ,V{x10_6} -> X{*} ,V{x10_11} -> X{*} ,V{x10_14} -> X{*} ,R{0} -> R{14} | main(X{*},X{*}) ,R{5} -> V{x8_5} ,R{6} -> S(R{6}) | S(R{5}) | S(@(R{8},V{x8_6})) | S(@(@(plus(),V{x10_6}),V{x8_6})) ,R{8} -> plus_x(V{x6_8}) ,R{10} -> Nil() ,R{11} -> Cons(R{6},R{10}) | Cons(R{5},R{10}) | Cons(R{6},R{11}) | Cons(R{5},R{11}) | Cons(@(V{x4_11},V{x8_11}),R{11}) | Cons(@(V{x4_11},V{x8_11}),R{10}) | Cons(R{6},@(R{13},V{x10_11})) | Cons(R{5},@(R{13},V{x10_11})) | Cons(@(V{x4_11},V{x8_11}),@(R{13},V{x10_11})) | Cons(R{6},@(@(map(),V{x4_11}),V{x10_11})) | Cons(R{5},@(@(map(),V{x4_11}),V{x10_11})) | Cons(@(V{x4_11},V{x8_11}),@(@(map(),V{x4_11}),V{x10_11})) ,R{13} -> map_f(V{x4_13}) ,R{14} -> R{11} | R{10} | @(R{13},V{x8_14}) | @(@(map(),R{8}),V{x8_14}) | @(@(map(),@(plus(),V{x10_14})),V{x8_14})} * Step 11: UncurryATRS WORST_CASE(?,O(n^2)) + Considered Problem: 5: plus_x(0()) x8 -> x8 6: plus_x(S(x2)) x1 -> S(plus() x2 x1) 8: plus() x6 -> plus_x(x6) 10: map_f(plus_x(x1)) Nil() -> Nil() 11: map_f(plus_x(x3)) Cons(x2, x1) -> Cons(plus_x(x3) x2, map() plus_x(x3) x1) 13: map() plus_x(x1) -> map_f(plus_x(x1)) 14: main(x2, x1) -> map() (plus() x1) x2 where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat map_f :: (nat -> nat) -> nat list -> nat list plus_x :: nat -> nat -> nat map :: (nat -> nat) -> nat list -> nat list plus :: nat -> nat -> nat main :: nat list -> nat -> nat list + Applied Processor: UncurryATRS + Details: none * Step 12: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: 1: plus_x#1(0(), x8) -> x8 2: plus_x#1(S(x2), x1) -> S(plus#2(x2, x1)) 3: plus#1(x6) -> plus_x(x6) 4: plus#2(x6, x7) -> plus_x#1(x6, x7) 5: map_f#1(plus_x(x1), Nil()) -> Nil() 6: map_f#1(plus_x(x3), Cons(x2, x1)) -> Cons(plus_x#1(x3, x2), map#2(plus_x(x3), x1)) 7: map#1(plus_x(x1)) -> map_f(plus_x(x1)) 8: map#2(plus_x(x1), x2) -> map_f#1(plus_x(x1), x2) 9: main(x2, x1) -> map#2(plus#1(x1), x2) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat main :: nat list -> nat -> nat list map#1 :: (nat -> nat) -> nat list -> nat list map#2 :: (nat -> nat) -> nat list -> nat list map_f :: (nat -> nat) -> nat list -> nat list map_f#1 :: (nat -> nat) -> nat list -> nat list 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 = DFA} + Details: none * Step 13: Inline WORST_CASE(?,O(n^2)) + Considered Problem: 1: plus_x#1(0(), x8) -> x8 2: plus_x#1(S(x2), x1) -> S(plus#2(x2, x1)) 3: plus#1(x6) -> plus_x(x6) 4: plus#2(x6, x7) -> plus_x#1(x6, x7) 5: map_f#1(plus_x(x1), Nil()) -> Nil() 6: map_f#1(plus_x(x3), Cons(x2, x1)) -> Cons(plus_x#1(x3, x2), map#2(plus_x(x3), x1)) 8: map#2(plus_x(x1), x2) -> map_f#1(plus_x(x1), x2) 9: main(x2, x1) -> map#2(plus#1(x1), x2) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat main :: nat list -> nat -> nat list map#2 :: (nat -> nat) -> nat list -> nat list map_f#1 :: (nat -> nat) -> nat list -> nat list 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 14: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: 1: plus_x#1(0(), x8) -> x8 2: plus_x#1(S(x12), x14) -> S(plus_x#1(x12, x14)) 3: plus#1(x6) -> plus_x(x6) 4: plus#2(x6, x7) -> plus_x#1(x6, x7) 5: map_f#1(plus_x(x1), Nil()) -> Nil() 6: map_f#1(plus_x(x3), Cons(x2, x1)) -> Cons(plus_x#1(x3, x2), map#2(plus_x(x3), x1)) 7: map#2(plus_x(x2), Nil()) -> Nil() 8: map#2(plus_x(x6), Cons(x4, x2)) -> Cons(plus_x#1(x6, x4), map#2(plus_x(x6), x2)) 9: main(x5, x12) -> map#2(plus_x(x12), x5) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat main :: nat list -> nat -> nat list map#2 :: (nat -> nat) -> nat list -> nat list map_f#1 :: (nat -> nat) -> nat list -> nat list 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 15: Compression WORST_CASE(?,O(n^2)) + Considered Problem: 1: plus_x#1(0(), x8) -> x8 2: plus_x#1(S(x12), x14) -> S(plus_x#1(x12, x14)) 7: map#2(plus_x(x2), Nil()) -> Nil() 8: map#2(plus_x(x6), Cons(x4, x2)) -> Cons(plus_x#1(x6, x4), map#2(plus_x(x6), x2)) 9: main(x5, x12) -> map#2(plus_x(x12), x5) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat main :: nat list -> nat -> nat list map#2 :: (nat -> nat) -> nat list -> nat list plus_x :: nat -> nat -> nat plus_x#1 :: nat -> nat -> nat + Applied Processor: Compression + Details: none * Step 16: ToTctProblem WORST_CASE(?,O(n^2)) + Considered Problem: 1: plus_x#1(0(), x8) -> x8 2: plus_x#1(S(x12), x14) -> S(plus_x#1(x12, x14)) 3: map#2(plus_x(x2), Nil()) -> Nil() 4: map#2(plus_x(x6), Cons(x4, x2)) -> Cons(plus_x#1(x6, x4), map#2(plus_x(x6), x2)) 5: main(x5, x12) -> map#2(plus_x(x12), x5) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat main :: nat list -> nat -> nat list map#2 :: (nat -> nat) -> nat list -> nat list plus_x :: nat -> nat -> nat plus_x#1 :: nat -> nat -> nat + Applied Processor: ToTctProblem + Details: none * Step 17: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: main(x5,x12) -> map#2(plus_x(x12),x5) map#2(plus_x(x2),Nil()) -> Nil() map#2(plus_x(x6),Cons(x4,x2)) -> Cons(plus_x#1(x6,x4),map#2(plus_x(x6),x2)) plus_x#1(0(),x8) -> x8 plus_x#1(S(x12),x14) -> S(plus_x#1(x12,x14)) - Signature: {main/2,map#2/2,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,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) = {1,2}, uargs(S) = {1} Following symbols are considered usable: {main,map#2,plus_x#1} TcT has computed the following interpretation: p(0) = [0] p(Cons) = [1] x1 + [1] x2 + [10] p(Nil) = [6] p(S) = [1] x1 + [0] p(main) = [3] x1 + [8] x2 + [10] p(map#2) = [2] x2 + [0] p(plus_x) = [0] p(plus_x#1) = [1] x2 + [6] Following rules are strictly oriented: main(x5,x12) = [8] x12 + [3] x5 + [10] > [2] x5 + [0] = map#2(plus_x(x12),x5) map#2(plus_x(x2),Nil()) = [12] > [6] = Nil() map#2(plus_x(x6),Cons(x4,x2)) = [2] x2 + [2] x4 + [20] > [2] x2 + [1] x4 + [16] = Cons(plus_x#1(x6,x4),map#2(plus_x(x6),x2)) plus_x#1(0(),x8) = [1] x8 + [6] > [1] x8 + [0] = x8 Following rules are (at-least) weakly oriented: plus_x#1(S(x12),x14) = [1] x14 + [6] >= [1] x14 + [6] = S(plus_x#1(x12,x14)) * Step 18: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: plus_x#1(S(x12),x14) -> S(plus_x#1(x12,x14)) - Weak TRS: main(x5,x12) -> map#2(plus_x(x12),x5) map#2(plus_x(x2),Nil()) -> Nil() map#2(plus_x(x6),Cons(x4,x2)) -> Cons(plus_x#1(x6,x4),map#2(plus_x(x6),x2)) plus_x#1(0(),x8) -> x8 - Signature: {main/2,map#2/2,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,plus_x/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,Cons,Nil,S} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(Cons) = {1,2}, uargs(S) = {1} Following symbols are considered usable: {main,map#2,plus_x#1} TcT has computed the following interpretation: p(0) = 2 p(Cons) = 1 + x1 + x2 p(Nil) = 0 p(S) = 2 + x1 p(main) = 2 + 7*x1 + 4*x1*x2 + 2*x2^2 p(map#2) = 2 + 4*x1*x2 + 2*x1^2 + 7*x2 p(plus_x) = x1 p(plus_x#1) = 6 + 4*x1 + 2*x1*x2 Following rules are strictly oriented: plus_x#1(S(x12),x14) = 14 + 4*x12 + 2*x12*x14 + 4*x14 > 8 + 4*x12 + 2*x12*x14 = S(plus_x#1(x12,x14)) Following rules are (at-least) weakly oriented: main(x5,x12) = 2 + 4*x12*x5 + 2*x12^2 + 7*x5 >= 2 + 4*x12*x5 + 2*x12^2 + 7*x5 = map#2(plus_x(x12),x5) map#2(plus_x(x2),Nil()) = 2 + 2*x2^2 >= 0 = Nil() map#2(plus_x(x6),Cons(x4,x2)) = 9 + 7*x2 + 4*x2*x6 + 7*x4 + 4*x4*x6 + 4*x6 + 2*x6^2 >= 9 + 7*x2 + 4*x2*x6 + 2*x4*x6 + 4*x6 + 2*x6^2 = Cons(plus_x#1(x6,x4),map#2(plus_x(x6),x2)) plus_x#1(0(),x8) = 14 + 4*x8 >= x8 = x8 * Step 19: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: main(x5,x12) -> map#2(plus_x(x12),x5) map#2(plus_x(x2),Nil()) -> Nil() map#2(plus_x(x6),Cons(x4,x2)) -> Cons(plus_x#1(x6,x4),map#2(plus_x(x6),x2)) plus_x#1(0(),x8) -> x8 plus_x#1(S(x12),x14) -> S(plus_x#1(x12,x14)) - Signature: {main/2,map#2/2,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,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^2))