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: Ara 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: Ara {minDegree = 1, maxDegree = 2, araTimeout = 3, araRuleShifting = Nothing} + Details: Signatures used: ---------------- F (TrsFun "Cons") :: ["A"(7) x "A"(7)] -(7)-> "A"(7) F (TrsFun "Cons") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "Nil") :: [] -(0)-> "A"(7) F (TrsFun "Nil") :: [] -(0)-> "A"(0) F (TrsFun "foldl#3") :: ["A"(0) x "A"(7)] -(12)-> "A"(0) F (TrsFun "main") :: ["A"(14)] -(15)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "F (TrsFun \"Cons\")_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "F (TrsFun \"Nil\")_A" :: [] -(0)-> "A"(1) WORST_CASE(?,O(n^1))