WORST_CASE(?,O(n^1)) * Step 1: Desugar WORST_CASE(?,O(n^1)) + Considered Problem: (* Richard Bird: Introduction to functional programming using Haskell, Section 7.2 *) type 'a list = Nil | Cons of 'a * 'a list ;; let rec foldl f z xs = match xs with | Nil -> z | Cons(x,xs') -> foldl f (f z x) xs' ;; let prefix xs x = Cons(x,xs);; let rev l = foldl prefix Nil l;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization WORST_CASE(?,O(n^1)) + Considered Problem: λl : 'a5 list. (λfoldl : ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list. (λprefix : 'a5 list -> 'a5 -> 'a5 list. (λrev : 'a5 list -> 'a5 list. rev l) (λl : 'a5 list. foldl prefix Nil l)) (λxs : 'a5 list. λx : 'a5. Cons(x,xs))) (μfoldl : ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list. λf : 'a5 list -> 'a5 -> 'a5 list. λz : 'a5 list. λxs : 'a5 list. case xs of | Nil -> z | Cons -> λx : 'a5. λxs' : 'a5 list. foldl f (f z x) xs') : 'a5 list -> 'a5 list where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list + Applied Processor: Defunctionalization + Details: none * Step 3: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: rev(x1, x2) x3 -> x1 x2 Nil() x3 3: main_2(x0, x1) x2 -> main_3(x0) rev(x1, x2) 4: prefix_xs(x2) x3 -> Cons(x3, x2) 5: prefix() x2 -> prefix_xs(x2) 6: main_1(x0) x1 -> main_2(x0, x1) prefix() 7: cond_foldl_f_z_xs(Nil(), x1, x2) -> x2 8: cond_foldl_f_z_xs(Cons(x4, x5), x1, x2) -> foldl() x1 (x1 x2 x4) x5 9: foldl_f_z(x1, x2) x3 -> cond_foldl_f_z_xs(x3, x1, x2) 10: foldl_f(x1) x2 -> foldl_f_z(x1, x2) 11: foldl_1() x1 -> foldl_f(x1) 12: foldl() x0 -> foldl_1() x0 13: main(x0) -> main_1(x0) foldl() where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list foldl_f :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list prefix :: 'a5 list -> 'a5 -> 'a5 list rev :: (('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list) -> ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list prefix_xs :: 'a5 list -> 'a5 -> 'a5 list foldl_f_z :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list foldl_1 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main_1 :: 'a5 list -> (('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list) -> 'a5 list main_2 :: 'a5 list -> (('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list) -> ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list main_3 :: 'a5 list -> ('a5 list -> 'a5 list) -> 'a5 list cond_foldl_f_z_xs :: 'a5 list -> ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list foldl :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main :: 'a5 list -> 'a5 list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: rev(x1, x2) x3 -> x1 x2 Nil() x3 3: main_2(x0, x3) x5 -> rev(x3, x5) x0 4: prefix_xs(x2) x3 -> Cons(x3, x2) 5: prefix() x2 -> prefix_xs(x2) 6: main_1(x0) x2 -> main_3(x0) rev(x2, prefix()) 7: cond_foldl_f_z_xs(Nil(), x1, x2) -> x2 8: cond_foldl_f_z_xs(Cons(x4, x5), x1, x2) -> foldl() x1 (x1 x2 x4) x5 9: foldl_f_z(x1, x2) x3 -> cond_foldl_f_z_xs(x3, x1, x2) 10: foldl_f(x1) x2 -> foldl_f_z(x1, x2) 11: foldl_1() x1 -> foldl_f(x1) 12: foldl() x2 -> foldl_f(x2) 13: main(x0) -> main_2(x0, foldl()) prefix() where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list foldl_f :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list prefix :: 'a5 list -> 'a5 -> 'a5 list rev :: (('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list) -> ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list prefix_xs :: 'a5 list -> 'a5 -> 'a5 list foldl_f_z :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list foldl_1 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main_1 :: 'a5 list -> (('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list) -> 'a5 list main_2 :: 'a5 list -> (('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list) -> ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list main_3 :: 'a5 list -> ('a5 list -> 'a5 list) -> 'a5 list cond_foldl_f_z_xs :: 'a5 list -> ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list foldl :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main :: 'a5 list -> 'a5 list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 5: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: rev(x1, x2) x3 -> x1 x2 Nil() x3 3: main_2(x6, x2) x4 -> x2 x4 Nil() x6 4: prefix_xs(x2) x3 -> Cons(x3, x2) 5: prefix() x2 -> prefix_xs(x2) 6: main_1(x0) x5 -> rev(x5, prefix()) x0 7: cond_foldl_f_z_xs(Nil(), x1, x2) -> x2 8: cond_foldl_f_z_xs(Cons(x4, x5), x1, x2) -> foldl() x1 (x1 x2 x4) x5 9: foldl_f_z(x1, x2) x3 -> cond_foldl_f_z_xs(x3, x1, x2) 10: foldl_f(x1) x2 -> foldl_f_z(x1, x2) 11: foldl_1() x1 -> foldl_f(x1) 12: foldl() x2 -> foldl_f(x2) 13: main(x0) -> rev(foldl(), prefix()) x0 where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list foldl_f :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list prefix :: 'a5 list -> 'a5 -> 'a5 list rev :: (('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list) -> ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list prefix_xs :: 'a5 list -> 'a5 -> 'a5 list foldl_f_z :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list foldl_1 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main_1 :: 'a5 list -> (('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list) -> 'a5 list main_2 :: 'a5 list -> (('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list) -> ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list main_3 :: 'a5 list -> ('a5 list -> 'a5 list) -> 'a5 list cond_foldl_f_z_xs :: 'a5 list -> ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list foldl :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main :: 'a5 list -> 'a5 list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 6: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: rev(x1, x2) x3 -> x1 x2 Nil() x3 3: main_2(x6, x2) x4 -> x2 x4 Nil() x6 4: prefix_xs(x2) x3 -> Cons(x3, x2) 5: prefix() x2 -> prefix_xs(x2) 6: main_1(x6) x2 -> x2 prefix() Nil() x6 7: cond_foldl_f_z_xs(Nil(), x1, x2) -> x2 8: cond_foldl_f_z_xs(Cons(x4, x5), x1, x2) -> foldl() x1 (x1 x2 x4) x5 9: foldl_f_z(x1, x2) x3 -> cond_foldl_f_z_xs(x3, x1, x2) 10: foldl_f(x1) x2 -> foldl_f_z(x1, x2) 11: foldl_1() x1 -> foldl_f(x1) 12: foldl() x2 -> foldl_f(x2) 13: main(x6) -> foldl() prefix() Nil() x6 where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list foldl_f :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list prefix :: 'a5 list -> 'a5 -> 'a5 list rev :: (('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list) -> ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list prefix_xs :: 'a5 list -> 'a5 -> 'a5 list foldl_f_z :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list foldl_1 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main_1 :: 'a5 list -> (('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list) -> 'a5 list main_2 :: 'a5 list -> (('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list) -> ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list main_3 :: 'a5 list -> ('a5 list -> 'a5 list) -> 'a5 list cond_foldl_f_z_xs :: 'a5 list -> ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list foldl :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main :: 'a5 list -> 'a5 list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 7: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: rev(x1, x2) x3 -> x1 x2 Nil() x3 3: main_2(x6, x2) x4 -> x2 x4 Nil() x6 4: prefix_xs(x2) x3 -> Cons(x3, x2) 5: prefix() x2 -> prefix_xs(x2) 6: main_1(x6) x2 -> x2 prefix() Nil() x6 7: cond_foldl_f_z_xs(Nil(), x1, x2) -> x2 8: cond_foldl_f_z_xs(Cons(x4, x5), x1, x2) -> foldl() x1 (x1 x2 x4) x5 9: foldl_f_z(x2, x4) Nil() -> x4 10: foldl_f_z(x2, x4) Cons(x8, x10) -> foldl() x2 (x2 x4 x8) x10 11: foldl_f(x1) x2 -> foldl_f_z(x1, x2) 12: foldl_1() x1 -> foldl_f(x1) 13: foldl() x2 -> foldl_f(x2) 14: main(x6) -> foldl() prefix() Nil() x6 where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list foldl_f :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list prefix :: 'a5 list -> 'a5 -> 'a5 list rev :: (('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list) -> ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list prefix_xs :: 'a5 list -> 'a5 -> 'a5 list foldl_f_z :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list foldl_1 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main_1 :: 'a5 list -> (('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list) -> 'a5 list main_2 :: 'a5 list -> (('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list) -> ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list main_3 :: 'a5 list -> ('a5 list -> 'a5 list) -> 'a5 list cond_foldl_f_z_xs :: 'a5 list -> ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list foldl :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main :: 'a5 list -> 'a5 list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 8: NeededRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: rev(x1, x2) x3 -> x1 x2 Nil() x3 3: main_2(x6, x2) x4 -> x2 x4 Nil() x6 4: prefix_xs(x2) x3 -> Cons(x3, x2) 5: prefix() x2 -> prefix_xs(x2) 6: main_1(x6) x2 -> x2 prefix() Nil() x6 9: foldl_f_z(x2, x4) Nil() -> x4 10: foldl_f_z(x2, x4) Cons(x8, x10) -> foldl() x2 (x2 x4 x8) x10 11: foldl_f(x1) x2 -> foldl_f_z(x1, x2) 12: foldl_1() x1 -> foldl_f(x1) 13: foldl() x2 -> foldl_f(x2) 14: main(x6) -> foldl() prefix() Nil() x6 where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list foldl_f :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list prefix :: 'a5 list -> 'a5 -> 'a5 list rev :: (('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list) -> ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list prefix_xs :: 'a5 list -> 'a5 -> 'a5 list foldl_f_z :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list foldl_1 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main_1 :: 'a5 list -> (('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list) -> 'a5 list main_2 :: 'a5 list -> (('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list) -> ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list main_3 :: 'a5 list -> ('a5 list -> 'a5 list) -> 'a5 list foldl :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main :: 'a5 list -> 'a5 list + Applied Processor: NeededRules + Details: none * Step 9: CFA WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: rev(x1, x2) x3 -> x1 x2 Nil() x3 3: main_2(x6, x2) x4 -> x2 x4 Nil() x6 4: prefix_xs(x2) x3 -> Cons(x3, x2) 5: prefix() x2 -> prefix_xs(x2) 6: main_1(x6) x2 -> x2 prefix() Nil() x6 7: foldl_f_z(x2, x4) Nil() -> x4 8: foldl_f_z(x2, x4) Cons(x8, x10) -> foldl() x2 (x2 x4 x8) x10 9: foldl_f(x1) x2 -> foldl_f_z(x1, x2) 10: foldl_1() x1 -> foldl_f(x1) 11: foldl() x2 -> foldl_f(x2) 12: main(x6) -> foldl() prefix() Nil() x6 where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list foldl_f :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list prefix :: 'a5 list -> 'a5 -> 'a5 list rev :: (('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list) -> ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list prefix_xs :: 'a5 list -> 'a5 -> 'a5 list foldl_f_z :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list foldl_1 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main_1 :: 'a5 list -> (('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list) -> 'a5 list main_2 :: 'a5 list -> (('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list) -> ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list main_3 :: 'a5 list -> ('a5 list -> 'a5 list) -> 'a5 list foldl :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main :: 'a5 list -> 'a5 list + Applied Processor: CFA {cfaRefinement = } + Details: {X{*} -> Nil() | Cons(X{*},X{*}) | Nil() | Nil() | Cons(X{*},X{*}) | Nil() | Nil() ,V{x1_9} -> V{x2_11} ,V{x2_4} -> V{x2_5} ,V{x2_5} -> V{x4_8} ,V{x2_7} -> V{x1_9} ,V{x2_8} -> V{x1_9} ,V{x2_9} -> R{4} | Nil() ,V{x2_11} -> V{x2_8} | prefix() ,V{x3_4} -> V{x8_8} ,V{x4_7} -> V{x2_9} ,V{x4_8} -> V{x2_9} ,V{x6_12} -> X{*} ,V{x8_8} -> X{*} ,V{x10_8} -> X{*} ,R{0} -> R{12} | main(X{*}) ,R{4} -> Cons(V{x3_4},V{x2_4}) ,R{5} -> prefix_xs(V{x2_5}) ,R{7} -> V{x4_7} ,R{8} -> R{8} | R{7} | @(R{9},V{x10_8}) | @(@(R{11},R{4}),V{x10_8}) | @(@(@(foldl(),V{x2_8}),R{4}),V{x10_8}) | @(@(R{11},@(R{5},V{x8_8})),V{x10_8}) | @(@(@(foldl(),V{x2_8}),@(R{5},V{x8_8})),V{x10_8}) | @(@(R{11},@(@(V{x2_8},V{x4_8}),V{x8_8})),V{x10_8}) | @(@(@(foldl(),V{x2_8}),@(@(V{x2_8},V{x4_8}),V{x8_8})),V{x10_8}) ,R{9} -> foldl_f_z(V{x1_9},V{x2_9}) ,R{11} -> foldl_f(V{x2_11}) ,R{12} -> R{8} | R{7} | @(R{9},V{x6_12}) | @(@(R{11},Nil()),V{x6_12}) | @(@(@(foldl(),prefix()),Nil()),V{x6_12})} * Step 10: UncurryATRS WORST_CASE(?,O(n^1)) + Considered Problem: 4: prefix_xs(x2) x3 -> Cons(x3, x2) 5: prefix() x2 -> prefix_xs(x2) 7: foldl_f_z(prefix(), x1) Nil() -> x1 8: foldl_f_z(prefix(), x3) Cons(x2, x1) -> foldl() prefix() (prefix() x3 x2) x1 9: foldl_f(prefix()) x1 -> foldl_f_z(prefix(), x1) 11: foldl() prefix() -> foldl_f(prefix()) 12: main(x1) -> foldl() prefix() Nil() x1 where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list foldl_f :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list prefix :: 'a5 list -> 'a5 -> 'a5 list prefix_xs :: 'a5 list -> 'a5 -> 'a5 list foldl_f_z :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list foldl :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main :: 'a5 list -> 'a5 list + Applied Processor: UncurryATRS + Details: none * Step 11: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: prefix_xs#1(x2, x3) -> Cons(x3, x2) 2: prefix#1(x2) -> prefix_xs(x2) 3: prefix#2(x2, x3) -> prefix_xs#1(x2, x3) 4: foldl_f_z#1(prefix(), x1, Nil()) -> x1 5: foldl_f_z#1(prefix(), x3, Cons(x2, x1)) -> foldl#3(prefix(), prefix#2(x3, x2), x1) 6: foldl_f#1(prefix(), x1) -> foldl_f_z(prefix(), x1) 7: foldl_f#2(prefix(), x1, x2) -> foldl_f_z#1(prefix(), x1, x2) 8: foldl#1(prefix()) -> foldl_f(prefix()) 9: foldl#2(prefix(), x0) -> foldl_f#1(prefix(), x0) 10: foldl#3(prefix(), x0, x1) -> foldl_f#2(prefix(), x0, x1) 11: main(x1) -> foldl#3(prefix(), Nil(), x1) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list foldl#1 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list foldl#2 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list foldl#3 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list foldl_f :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list foldl_f#1 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list foldl_f#2 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list foldl_f_z :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list foldl_f_z#1 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main :: 'a5 list -> 'a5 list prefix :: 'a5 list -> 'a5 -> 'a5 list prefix#1 :: 'a5 list -> 'a5 -> 'a5 list prefix#2 :: 'a5 list -> 'a5 -> 'a5 list prefix_xs :: 'a5 list -> 'a5 -> 'a5 list prefix_xs#1 :: 'a5 list -> 'a5 -> 'a5 list + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 12: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: prefix_xs#1(x2, x3) -> Cons(x3, x2) 3: prefix#2(x2, x3) -> prefix_xs#1(x2, x3) 4: foldl_f_z#1(prefix(), x1, Nil()) -> x1 5: foldl_f_z#1(prefix(), x3, Cons(x2, x1)) -> foldl#3(prefix(), prefix#2(x3, x2), x1) 7: foldl_f#2(prefix(), x1, x2) -> foldl_f_z#1(prefix(), x1, x2) 10: foldl#3(prefix(), x0, x1) -> foldl_f#2(prefix(), x0, x1) 11: main(x1) -> foldl#3(prefix(), Nil(), x1) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list foldl#3 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list foldl_f#2 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list foldl_f_z#1 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main :: 'a5 list -> 'a5 list prefix :: 'a5 list -> 'a5 -> 'a5 list prefix#2 :: 'a5 list -> 'a5 -> 'a5 list prefix_xs#1 :: 'a5 list -> 'a5 -> 'a5 list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 13: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: prefix_xs#1(x2, x3) -> Cons(x3, x2) 2: prefix#2(x4, x6) -> Cons(x6, x4) 3: foldl_f_z#1(prefix(), x1, Nil()) -> x1 4: foldl_f_z#1(prefix(), x4, Cons(x6, x3)) -> foldl#3(prefix(), prefix_xs#1(x4, x6), x3) 5: foldl_f#2(prefix(), x2, Nil()) -> x2 6: foldl_f#2(prefix(), x6, Cons(x4, x2)) -> foldl#3(prefix(), prefix#2(x6, x4), x2) 7: foldl#3(prefix(), x2, x4) -> foldl_f_z#1(prefix(), x2, x4) 8: main(x1) -> foldl#3(prefix(), Nil(), x1) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list foldl#3 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list foldl_f#2 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list foldl_f_z#1 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main :: 'a5 list -> 'a5 list prefix :: 'a5 list -> 'a5 -> 'a5 list prefix#2 :: 'a5 list -> 'a5 -> 'a5 list prefix_xs#1 :: 'a5 list -> 'a5 -> 'a5 list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 14: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: prefix_xs#1(x2, x3) -> Cons(x3, x2) 3: foldl_f_z#1(prefix(), x1, Nil()) -> x1 4: foldl_f_z#1(prefix(), x4, Cons(x6, x3)) -> foldl#3(prefix(), prefix_xs#1(x4, x6), x3) 7: foldl#3(prefix(), x2, x4) -> foldl_f_z#1(prefix(), x2, x4) 8: main(x1) -> foldl#3(prefix(), Nil(), x1) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list foldl#3 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list foldl_f_z#1 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main :: 'a5 list -> 'a5 list prefix :: 'a5 list -> 'a5 -> 'a5 list prefix_xs#1 :: 'a5 list -> 'a5 -> 'a5 list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 15: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: prefix_xs#1(x2, x3) -> Cons(x3, x2) 2: foldl_f_z#1(prefix(), x1, Nil()) -> x1 3: foldl_f_z#1(prefix(), x4, Cons(x6, x7)) -> foldl#3(prefix(), Cons(x6, x4), x7) 4: foldl#3(prefix(), x2, Nil()) -> x2 5: foldl#3(prefix(), x8, Cons(x12, x6)) -> foldl#3(prefix(), prefix_xs#1(x8, x12), x6) 6: main(x1) -> foldl#3(prefix(), Nil(), x1) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list foldl#3 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list foldl_f_z#1 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main :: 'a5 list -> 'a5 list prefix :: 'a5 list -> 'a5 -> 'a5 list prefix_xs#1 :: 'a5 list -> 'a5 -> 'a5 list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 16: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: prefix_xs#1(x2, x3) -> Cons(x3, x2) 4: foldl#3(prefix(), x2, Nil()) -> x2 5: foldl#3(prefix(), x8, Cons(x12, x6)) -> foldl#3(prefix(), prefix_xs#1(x8, x12), x6) 6: main(x1) -> foldl#3(prefix(), Nil(), x1) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list foldl#3 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main :: 'a5 list -> 'a5 list prefix :: 'a5 list -> 'a5 -> 'a5 list prefix_xs#1 :: 'a5 list -> 'a5 -> 'a5 list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 17: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: prefix_xs#1(x2, x3) -> Cons(x3, x2) 2: foldl#3(prefix(), x2, Nil()) -> x2 3: foldl#3(prefix(), x4, Cons(x6, x13)) -> foldl#3(prefix(), Cons(x6, x4), x13) 4: main(x1) -> foldl#3(prefix(), Nil(), x1) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list foldl#3 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main :: 'a5 list -> 'a5 list prefix :: 'a5 list -> 'a5 -> 'a5 list prefix_xs#1 :: 'a5 list -> 'a5 -> 'a5 list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 18: Compression WORST_CASE(?,O(n^1)) + Considered Problem: 2: foldl#3(prefix(), x2, Nil()) -> x2 3: foldl#3(prefix(), x4, Cons(x6, x13)) -> foldl#3(prefix(), Cons(x6, x4), x13) 4: main(x1) -> foldl#3(prefix(), Nil(), x1) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list foldl#3 :: ('a5 list -> 'a5 -> 'a5 list) -> 'a5 list -> 'a5 list -> 'a5 list main :: 'a5 list -> 'a5 list prefix :: 'a5 list -> 'a5 -> 'a5 list + Applied Processor: Compression + Details: none * Step 19: ToTctProblem WORST_CASE(?,O(n^1)) + Considered Problem: 1: foldl#3(x2, Nil()) -> x2 2: foldl#3(x4, Cons(x6, x13)) -> foldl#3(Cons(x6, x4), x13) 3: main(x1) -> foldl#3(Nil(), x1) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list foldl#3 :: 'a5 list -> 'a5 list -> 'a5 list main :: 'a5 list -> 'a5 list + Applied Processor: ToTctProblem + Details: none * Step 20: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: foldl#3(x2,Nil()) -> x2 foldl#3(x4,Cons(x6,x13)) -> foldl#3(Cons(x6,x4),x13) main(x1) -> foldl#3(Nil(),x1) - Signature: {foldl#3/2,main/1} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil} + 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: none Following symbols are considered usable: {foldl#3,main} TcT has computed the following interpretation: p(Cons) = [0] p(Nil) = [0] p(foldl#3) = [2] x1 + [0] p(main) = [1] Following rules are strictly oriented: main(x1) = [1] > [0] = foldl#3(Nil(),x1) Following rules are (at-least) weakly oriented: foldl#3(x2,Nil()) = [2] x2 + [0] >= [1] x2 + [0] = x2 foldl#3(x4,Cons(x6,x13)) = [2] x4 + [0] >= [0] = foldl#3(Cons(x6,x4),x13) * Step 21: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: foldl#3(x2,Nil()) -> x2 foldl#3(x4,Cons(x6,x13)) -> foldl#3(Cons(x6,x4),x13) - Weak TRS: main(x1) -> foldl#3(Nil(),x1) - Signature: {foldl#3/2,main/1} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil} + 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: none Following symbols are considered usable: {foldl#3,main} TcT has computed the following interpretation: p(Cons) = 1 + x2 p(Nil) = 0 p(foldl#3) = 8*x1 + 9*x2 p(main) = 9*x1 Following rules are strictly oriented: foldl#3(x4,Cons(x6,x13)) = 9 + 9*x13 + 8*x4 > 8 + 9*x13 + 8*x4 = foldl#3(Cons(x6,x4),x13) Following rules are (at-least) weakly oriented: foldl#3(x2,Nil()) = 8*x2 >= x2 = x2 main(x1) = 9*x1 >= 9*x1 = foldl#3(Nil(),x1) * Step 22: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: foldl#3(x2,Nil()) -> x2 - Weak TRS: foldl#3(x4,Cons(x6,x13)) -> foldl#3(Cons(x6,x4),x13) main(x1) -> foldl#3(Nil(),x1) - Signature: {foldl#3/2,main/1} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil} + 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: none Following symbols are considered usable: {foldl#3,main} TcT has computed the following interpretation: p(Cons) = x2 p(Nil) = 0 p(foldl#3) = 4 + 8*x1 p(main) = 4 Following rules are strictly oriented: foldl#3(x2,Nil()) = 4 + 8*x2 > x2 = x2 Following rules are (at-least) weakly oriented: foldl#3(x4,Cons(x6,x13)) = 4 + 8*x4 >= 4 + 8*x4 = foldl#3(Cons(x6,x4),x13) main(x1) = 4 >= 4 = foldl#3(Nil(),x1) * Step 23: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: foldl#3(x2,Nil()) -> x2 foldl#3(x4,Cons(x6,x13)) -> foldl#3(Cons(x6,x4),x13) main(x1) -> foldl#3(Nil(),x1) - Signature: {foldl#3/2,main/1} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))