WORST_CASE(?,O(n^1)) * Step 1: Desugar WORST_CASE(?,O(n^1)) + Considered Problem: let comp f g x = f (g x) ;; type 'a list = Nil | Cons of 'a * 'a list ;; (* rev :: list -> list *) let rev l = (* walk :: list -> (list -> list) *) let rec walk xs = match xs with | Nil -> (fun x -> x) | Cons(x,xs') -> comp (walk xs') (fun ys -> Cons(x,ys)) in walk l Nil ;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization WORST_CASE(?,O(n^1)) + Considered Problem: λl : 'l list. (λcomp : ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list. (λrev : 'l list -> 'l list. rev l) (λl : 'l list. (λwalk : 'l list -> 'l list -> 'l list. walk l Nil) (μwalk : 'l list -> 'l list -> 'l list. λxs : 'l list. case xs of | Nil -> λx : 'l list. x | Cons -> λx : 'l. λxs' : 'l list. comp (walk xs') (λys : 'l list. Cons(x,ys))))) (λf : 'l list -> 'l list. λg : 'l list -> 'l list. λx : 'l list. f (g x)) : 'l list -> 'l 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_2(x0) x2 -> x2 x0 2: rev_l(x2) x3 -> x3 x2 Nil() 3: walk_xs() x4 -> x4 4: walk_xs_3(x4) x6 -> Cons(x4, x6) 5: cond_walk_xs(Nil(), x1) -> walk_xs() 6: cond_walk_xs(Cons(x4, x5), x1) -> x1 (walk(x1) x5) walk_xs_3(x4) 7: walk_1(x1) x3 -> cond_walk_xs(x3, x1) 8: walk(x1) x2 -> walk_1(x1) x2 9: rev(x1) x2 -> rev_l(x2) walk(x1) 10: main_1(x0) x1 -> main_2(x0) rev(x1) 11: comp_f_g(x1, x2) x3 -> x1 (x2 x3) 12: comp_f(x1) x2 -> comp_f_g(x1, x2) 13: comp() x1 -> comp_f(x1) 14: main(x0) -> main_1(x0) comp() where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list comp :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list rev_l :: 'l list -> ('l list -> 'l list -> 'l list) -> 'l list rev :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list walk_xs :: 'l list -> 'l list main_1 :: 'l list -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list walk_1 :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list main_2 :: 'l list -> ('l list -> 'l list) -> 'l list walk_xs_3 :: 'l -> 'l list -> 'l list cond_walk_xs :: 'l list -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list walk :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list main :: 'l list -> 'l list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_2(x0) x2 -> x2 x0 2: rev_l(x2) x3 -> x3 x2 Nil() 3: walk_xs() x4 -> x4 4: walk_xs_3(x4) x6 -> Cons(x4, x6) 5: cond_walk_xs(Nil(), x1) -> walk_xs() 6: cond_walk_xs(Cons(x4, x5), x1) -> x1 (walk(x1) x5) walk_xs_3(x4) 7: walk_1(x1) x3 -> cond_walk_xs(x3, x1) 8: walk(x2) x6 -> cond_walk_xs(x6, x2) 9: rev(x3) x4 -> walk(x3) x4 Nil() 10: main_1(x0) x3 -> rev(x3) x0 11: comp_f_g(x1, x2) x3 -> x1 (x2 x3) 12: comp_f(x1) x2 -> comp_f_g(x1, x2) 13: comp() x1 -> comp_f(x1) 14: main(x0) -> main_2(x0) rev(comp()) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list comp :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list rev_l :: 'l list -> ('l list -> 'l list -> 'l list) -> 'l list rev :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list walk_xs :: 'l list -> 'l list main_1 :: 'l list -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list walk_1 :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list main_2 :: 'l list -> ('l list -> 'l list) -> 'l list walk_xs_3 :: 'l -> 'l list -> 'l list cond_walk_xs :: 'l list -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list walk :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list main :: 'l list -> 'l list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 5: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_2(x0) x2 -> x2 x0 2: rev_l(x2) x3 -> x3 x2 Nil() 3: walk_xs() x4 -> x4 4: walk_xs_3(x4) x6 -> Cons(x4, x6) 5: cond_walk_xs(Nil(), x1) -> walk_xs() 6: cond_walk_xs(Cons(x4, x5), x1) -> x1 (walk(x1) x5) walk_xs_3(x4) 7: walk_1(x1) x3 -> cond_walk_xs(x3, x1) 8: walk(x2) x6 -> cond_walk_xs(x6, x2) 9: rev(x3) x4 -> walk(x3) x4 Nil() 10: main_1(x8) x6 -> walk(x6) x8 Nil() 11: comp_f_g(x1, x2) x3 -> x1 (x2 x3) 12: comp_f(x1) x2 -> comp_f_g(x1, x2) 13: comp() x1 -> comp_f(x1) 14: main(x0) -> rev(comp()) x0 where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list comp :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list rev_l :: 'l list -> ('l list -> 'l list -> 'l list) -> 'l list rev :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list walk_xs :: 'l list -> 'l list main_1 :: 'l list -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list walk_1 :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list main_2 :: 'l list -> ('l list -> 'l list) -> 'l list walk_xs_3 :: 'l -> 'l list -> 'l list cond_walk_xs :: 'l list -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list walk :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list main :: 'l list -> 'l list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 6: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_2(x0) x2 -> x2 x0 2: rev_l(x2) x3 -> x3 x2 Nil() 3: walk_xs() x4 -> x4 4: walk_xs_3(x4) x6 -> Cons(x4, x6) 5: cond_walk_xs(Nil(), x1) -> walk_xs() 6: cond_walk_xs(Cons(x4, x5), x1) -> x1 (walk(x1) x5) walk_xs_3(x4) 7: walk_1(x1) x3 -> cond_walk_xs(x3, x1) 8: walk(x2) x6 -> cond_walk_xs(x6, x2) 9: rev(x3) x4 -> walk(x3) x4 Nil() 10: main_1(x8) x6 -> walk(x6) x8 Nil() 11: comp_f_g(x1, x2) x3 -> x1 (x2 x3) 12: comp_f(x1) x2 -> comp_f_g(x1, x2) 13: comp() x1 -> comp_f(x1) 14: main(x8) -> walk(comp()) x8 Nil() where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list comp :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list rev_l :: 'l list -> ('l list -> 'l list -> 'l list) -> 'l list rev :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list walk_xs :: 'l list -> 'l list main_1 :: 'l list -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list walk_1 :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list main_2 :: 'l list -> ('l list -> 'l list) -> 'l list walk_xs_3 :: 'l -> 'l list -> 'l list cond_walk_xs :: 'l list -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list walk :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list main :: 'l list -> 'l list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 7: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_2(x0) x2 -> x2 x0 2: rev_l(x2) x3 -> x3 x2 Nil() 3: walk_xs() x4 -> x4 4: walk_xs_3(x4) x6 -> Cons(x4, x6) 5: cond_walk_xs(Nil(), x1) -> walk_xs() 6: cond_walk_xs(Cons(x4, x5), x1) -> x1 (walk(x1) x5) walk_xs_3(x4) 7: walk_1(x2) Nil() -> walk_xs() 8: walk_1(x2) Cons(x8, x10) -> x2 (walk(x2) x10) walk_xs_3(x8) 9: walk(x2) Nil() -> walk_xs() 10: walk(x2) Cons(x8, x10) -> x2 (walk(x2) x10) walk_xs_3(x8) 11: rev(x3) x4 -> walk(x3) x4 Nil() 12: main_1(x8) x6 -> walk(x6) x8 Nil() 13: comp_f_g(x1, x2) x3 -> x1 (x2 x3) 14: comp_f(x1) x2 -> comp_f_g(x1, x2) 15: comp() x1 -> comp_f(x1) 16: main(x8) -> walk(comp()) x8 Nil() where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list comp :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list rev_l :: 'l list -> ('l list -> 'l list -> 'l list) -> 'l list rev :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list walk_xs :: 'l list -> 'l list main_1 :: 'l list -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list walk_1 :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list main_2 :: 'l list -> ('l list -> 'l list) -> 'l list walk_xs_3 :: 'l -> 'l list -> 'l list cond_walk_xs :: 'l list -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list walk :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list main :: 'l list -> 'l list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 8: NeededRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_2(x0) x2 -> x2 x0 2: rev_l(x2) x3 -> x3 x2 Nil() 3: walk_xs() x4 -> x4 4: walk_xs_3(x4) x6 -> Cons(x4, x6) 7: walk_1(x2) Nil() -> walk_xs() 8: walk_1(x2) Cons(x8, x10) -> x2 (walk(x2) x10) walk_xs_3(x8) 9: walk(x2) Nil() -> walk_xs() 10: walk(x2) Cons(x8, x10) -> x2 (walk(x2) x10) walk_xs_3(x8) 11: rev(x3) x4 -> walk(x3) x4 Nil() 12: main_1(x8) x6 -> walk(x6) x8 Nil() 13: comp_f_g(x1, x2) x3 -> x1 (x2 x3) 14: comp_f(x1) x2 -> comp_f_g(x1, x2) 15: comp() x1 -> comp_f(x1) 16: main(x8) -> walk(comp()) x8 Nil() where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list comp :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list rev_l :: 'l list -> ('l list -> 'l list -> 'l list) -> 'l list rev :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list walk_xs :: 'l list -> 'l list main_1 :: 'l list -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list walk_1 :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list main_2 :: 'l list -> ('l list -> 'l list) -> 'l list walk_xs_3 :: 'l -> 'l list -> 'l list walk :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list main :: 'l list -> 'l list + Applied Processor: NeededRules + Details: none * Step 9: CFA WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_2(x0) x2 -> x2 x0 2: rev_l(x2) x3 -> x3 x2 Nil() 3: walk_xs() x4 -> x4 4: walk_xs_3(x4) x6 -> Cons(x4, x6) 5: walk_1(x2) Nil() -> walk_xs() 6: walk_1(x2) Cons(x8, x10) -> x2 (walk(x2) x10) walk_xs_3(x8) 7: walk(x2) Nil() -> walk_xs() 8: walk(x2) Cons(x8, x10) -> x2 (walk(x2) x10) walk_xs_3(x8) 9: rev(x3) x4 -> walk(x3) x4 Nil() 10: main_1(x8) x6 -> walk(x6) x8 Nil() 11: comp_f_g(x1, x2) x3 -> x1 (x2 x3) 12: comp_f(x1) x2 -> comp_f_g(x1, x2) 13: comp() x1 -> comp_f(x1) 14: main(x8) -> walk(comp()) x8 Nil() where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list comp :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list rev_l :: 'l list -> ('l list -> 'l list -> 'l list) -> 'l list rev :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list walk_xs :: 'l list -> 'l list main_1 :: 'l list -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list walk_1 :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list main_2 :: 'l list -> ('l list -> 'l list) -> 'l list walk_xs_3 :: 'l -> 'l list -> 'l list walk :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list main :: 'l list -> 'l list + Applied Processor: CFA {cfaRefinement = } + Details: {X{*} -> Nil() | Nil() | Nil() | Cons(X{*},X{*}) | Nil() | Cons(X{*},X{*}) | Nil() | Cons(X{*},X{*}) | Nil() ,V{x1_11} -> V{x1_12} ,V{x1_12} -> V{x1_13} ,V{x1_13} -> R{8} | R{7} ,V{x2_7} -> V{x2_8} | comp() ,V{x2_8} -> V{x2_8} | comp() ,V{x2_11} -> V{x2_12} ,V{x2_12} -> walk_xs_3(V{x8_8}) ,V{x3_11} -> R{4} | Nil() ,V{x4_3} -> R{4} | Nil() ,V{x4_4} -> V{x8_8} ,V{x6_4} -> V{x3_11} ,V{x8_8} -> X{*} ,V{x8_14} -> X{*} ,V{x10_8} -> X{*} ,R{0} -> R{14} | main(X{*}) ,R{3} -> V{x4_3} ,R{4} -> Cons(V{x4_4},V{x6_4}) ,R{7} -> walk_xs() ,R{8} -> R{12} | @(R{13},walk_xs_3(V{x8_8})) | @(@(V{x2_8},R{8}),walk_xs_3(V{x8_8})) | @(@(V{x2_8},R{7}),walk_xs_3(V{x8_8})) | @(@(V{x2_8},@(walk(V{x2_8}),V{x10_8})),walk_xs_3(V{x8_8})) ,R{11} -> R{11} | R{3} | @(V{x1_11},R{4}) | @(V{x1_11},@(V{x2_11},V{x3_11})) ,R{12} -> comp_f_g(V{x1_12},V{x2_12}) ,R{13} -> comp_f(V{x1_13}) ,R{14} -> R{11} | R{3} | @(R{8},Nil()) | @(R{7},Nil()) | @(@(walk(comp()),V{x8_14}),Nil())} * Step 10: UncurryATRS WORST_CASE(?,O(n^1)) + Considered Problem: 3: walk_xs() x4 -> x4 4: walk_xs_3(x4) x6 -> Cons(x4, x6) 7: walk(comp()) Nil() -> walk_xs() 8: walk(comp()) Cons(x2, x1) -> comp() (walk(comp()) x1) walk_xs_3(x2) 11: comp_f_g(comp_f_g(x3, x4), walk_xs_3(x2)) x1 -> comp_f_g(x3, x4) (walk_xs_3(x2) x1) 12: comp_f_g(walk_xs(), walk_xs_3(x2)) x1 -> walk_xs() (walk_xs_3(x2) x1) 13: comp_f(x2) walk_xs_3(x1) -> comp_f_g(x2, walk_xs_3(x1)) 14: comp() x1 -> comp_f(x1) 15: main(x1) -> walk(comp()) x1 Nil() where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list comp :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list walk_xs :: 'l list -> 'l list walk_xs_3 :: 'l -> 'l list -> 'l list walk :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list main :: 'l list -> 'l list + Applied Processor: UncurryATRS + Details: none * Step 11: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk_xs#1(x4) -> x4 2: walk_xs_3#1(x4, x6) -> Cons(x4, x6) 3: walk#1(comp(), Nil()) -> walk_xs() 4: walk#2(comp(), Nil(), x0) -> walk_xs#1(x0) 5: walk#1(comp(), Cons(x2, x1)) -> comp#2(walk#1(comp(), x1), walk_xs_3(x2)) 6: walk#2(comp(), Cons(x2, x1), x3) -> comp#3(walk#1(comp(), x1), walk_xs_3(x2), x3) 7: comp_f_g#1(comp_f_g(x3, x4), walk_xs_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xs_3#1(x2, x1)) 8: comp_f_g#1(walk_xs(), walk_xs_3(x2), x1) -> walk_xs#1(walk_xs_3#1(x2, x1)) 9: comp_f#1(x2, walk_xs_3(x1)) -> comp_f_g(x2, walk_xs_3(x1)) 10: comp_f#2(x2, walk_xs_3(x1), x3) -> comp_f_g#1(x2, walk_xs_3(x1), x3) 11: comp#1(x1) -> comp_f(x1) 12: comp#2(x1, x2) -> comp_f#1(x1, x2) 13: comp#3(x1, x2, x3) -> comp_f#2(x1, x2, x3) 14: main(x1) -> walk#2(comp(), x1, Nil()) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list comp :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp#1 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp#2 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp#3 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f#1 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f#2 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g#1 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list main :: 'l list -> 'l list walk#1 :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list walk#2 :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list walk_xs :: 'l list -> 'l list walk_xs#1 :: 'l list -> 'l list walk_xs_3 :: 'l -> 'l list -> 'l list walk_xs_3#1 :: 'l -> 'l list -> 'l list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 12: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk_xs#1(x4) -> x4 2: walk_xs_3#1(x4, x6) -> Cons(x4, x6) 3: walk#1(comp(), Nil()) -> walk_xs() 4: walk#2(comp(), Nil(), x8) -> x8 5: walk#1(comp(), Cons(x2, x1)) -> comp#2(walk#1(comp(), x1), walk_xs_3(x2)) 6: walk#2(comp(), Cons(x2, x1), x3) -> comp#3(walk#1(comp(), x1), walk_xs_3(x2), x3) 7: comp_f_g#1(comp_f_g(x3, x4), walk_xs_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xs_3#1(x2, x1)) 8: comp_f_g#1(walk_xs(), walk_xs_3(x5), x3) -> walk_xs_3#1(x5, x3) 9: comp_f#1(x2, walk_xs_3(x1)) -> comp_f_g(x2, walk_xs_3(x1)) 10: comp_f#2(x2, walk_xs_3(x1), x3) -> comp_f_g#1(x2, walk_xs_3(x1), x3) 11: comp#1(x1) -> comp_f(x1) 12: comp#2(x1, x2) -> comp_f#1(x1, x2) 13: comp#3(x1, x2, x3) -> comp_f#2(x1, x2, x3) 14: main(x1) -> walk#2(comp(), x1, Nil()) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list comp :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp#1 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp#2 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp#3 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f#1 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f#2 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g#1 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list main :: 'l list -> 'l list walk#1 :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list walk#2 :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list walk_xs :: 'l list -> 'l list walk_xs#1 :: 'l list -> 'l list walk_xs_3 :: 'l -> 'l list -> 'l list walk_xs_3#1 :: 'l -> 'l list -> 'l list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 13: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 2: walk_xs_3#1(x4, x6) -> Cons(x4, x6) 3: walk#1(comp(), Nil()) -> walk_xs() 4: walk#2(comp(), Nil(), x8) -> x8 5: walk#1(comp(), Cons(x2, x1)) -> comp#2(walk#1(comp(), x1), walk_xs_3(x2)) 6: walk#2(comp(), Cons(x2, x1), x3) -> comp#3(walk#1(comp(), x1), walk_xs_3(x2), x3) 7: comp_f_g#1(comp_f_g(x3, x4), walk_xs_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xs_3#1(x2, x1)) 8: comp_f_g#1(walk_xs(), walk_xs_3(x5), x3) -> walk_xs_3#1(x5, x3) 9: comp_f#1(x2, walk_xs_3(x1)) -> comp_f_g(x2, walk_xs_3(x1)) 10: comp_f#2(x2, walk_xs_3(x1), x3) -> comp_f_g#1(x2, walk_xs_3(x1), x3) 12: comp#2(x1, x2) -> comp_f#1(x1, x2) 13: comp#3(x1, x2, x3) -> comp_f#2(x1, x2, x3) 14: main(x1) -> walk#2(comp(), x1, Nil()) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list comp :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp#2 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp#3 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f#1 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f#2 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g#1 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list main :: 'l list -> 'l list walk#1 :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list walk#2 :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list walk_xs :: 'l list -> 'l list walk_xs_3 :: 'l -> 'l list -> 'l list walk_xs_3#1 :: 'l -> 'l list -> 'l list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 14: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk_xs_3#1(x4, x6) -> Cons(x4, x6) 2: walk#1(comp(), Nil()) -> walk_xs() 3: walk#2(comp(), Nil(), x8) -> x8 4: walk#1(comp(), Cons(x5, x3)) -> comp_f#1(walk#1(comp(), x3), walk_xs_3(x5)) 5: walk#2(comp(), Cons(x5, x3), x6) -> comp_f#2(walk#1(comp(), x3), walk_xs_3(x5), x6) 6: comp_f_g#1(comp_f_g(x3, x4), walk_xs_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xs_3#1(x2, x1)) 7: comp_f_g#1(walk_xs(), walk_xs_3(x5), x3) -> walk_xs_3#1(x5, x3) 8: comp_f#1(x2, walk_xs_3(x1)) -> comp_f_g(x2, walk_xs_3(x1)) 9: comp_f#2(x2, walk_xs_3(x1), x3) -> comp_f_g#1(x2, walk_xs_3(x1), x3) 10: comp#2(x4, walk_xs_3(x2)) -> comp_f_g(x4, walk_xs_3(x2)) 11: comp#3(x4, walk_xs_3(x2), x6) -> comp_f_g#1(x4, walk_xs_3(x2), x6) 12: main(Nil()) -> Nil() 13: main(Cons(x4, x2)) -> comp#3(walk#1(comp(), x2), walk_xs_3(x4), Nil()) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list comp :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp#2 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp#3 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f#1 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f#2 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g#1 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list main :: 'l list -> 'l list walk#1 :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list walk#2 :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list walk_xs :: 'l list -> 'l list walk_xs_3 :: 'l -> 'l list -> 'l list walk_xs_3#1 :: 'l -> 'l list -> 'l list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 15: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk_xs_3#1(x4, x6) -> Cons(x4, x6) 2: walk#1(comp(), Nil()) -> walk_xs() 4: walk#1(comp(), Cons(x5, x3)) -> comp_f#1(walk#1(comp(), x3), walk_xs_3(x5)) 6: comp_f_g#1(comp_f_g(x3, x4), walk_xs_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xs_3#1(x2, x1)) 7: comp_f_g#1(walk_xs(), walk_xs_3(x5), x3) -> walk_xs_3#1(x5, x3) 8: comp_f#1(x2, walk_xs_3(x1)) -> comp_f_g(x2, walk_xs_3(x1)) 11: comp#3(x4, walk_xs_3(x2), x6) -> comp_f_g#1(x4, walk_xs_3(x2), x6) 12: main(Nil()) -> Nil() 13: main(Cons(x4, x2)) -> comp#3(walk#1(comp(), x2), walk_xs_3(x4), Nil()) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list comp :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp#3 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f#1 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g#1 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list main :: 'l list -> 'l list walk#1 :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list walk_xs :: 'l list -> 'l list walk_xs_3 :: 'l -> 'l list -> 'l list walk_xs_3#1 :: 'l -> 'l list -> 'l list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 16: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk_xs_3#1(x4, x6) -> Cons(x4, x6) 2: walk#1(comp(), Nil()) -> walk_xs() 3: walk#1(comp(), Cons(x2, x7)) -> comp_f_g(walk#1(comp(), x7), walk_xs_3(x2)) 4: comp_f_g#1(comp_f_g(x3, x4), walk_xs_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xs_3#1(x2, x1)) 5: comp_f_g#1(walk_xs(), walk_xs_3(x5), x3) -> walk_xs_3#1(x5, x3) 6: comp_f#1(x2, walk_xs_3(x1)) -> comp_f_g(x2, walk_xs_3(x1)) 7: comp#3(x4, walk_xs_3(x2), x6) -> comp_f_g#1(x4, walk_xs_3(x2), x6) 8: main(Nil()) -> Nil() 9: main(Cons(x4, x5)) -> comp_f_g#1(walk#1(comp(), x5), walk_xs_3(x4), Nil()) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list comp :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp#3 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f#1 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g#1 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list main :: 'l list -> 'l list walk#1 :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list walk_xs :: 'l list -> 'l list walk_xs_3 :: 'l -> 'l list -> 'l list walk_xs_3#1 :: 'l -> 'l list -> 'l list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 17: Compression WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk_xs_3#1(x4, x6) -> Cons(x4, x6) 2: walk#1(comp(), Nil()) -> walk_xs() 3: walk#1(comp(), Cons(x2, x7)) -> comp_f_g(walk#1(comp(), x7), walk_xs_3(x2)) 4: comp_f_g#1(comp_f_g(x3, x4), walk_xs_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xs_3#1(x2, x1)) 5: comp_f_g#1(walk_xs(), walk_xs_3(x5), x3) -> walk_xs_3#1(x5, x3) 8: main(Nil()) -> Nil() 9: main(Cons(x4, x5)) -> comp_f_g#1(walk#1(comp(), x5), walk_xs_3(x4), Nil()) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list comp :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g#1 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list main :: 'l list -> 'l list walk#1 :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list -> 'l list walk_xs :: 'l list -> 'l list walk_xs_3 :: 'l -> 'l list -> 'l list walk_xs_3#1 :: 'l -> 'l list -> 'l list + Applied Processor: Compression + Details: none * Step 18: ToTctProblem WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk_xs_3#1(x4, x6) -> Cons(x4, x6) 2: walk#1(Nil()) -> walk_xs() 3: walk#1(Cons(x2, x7)) -> comp_f_g(walk#1(x7), walk_xs_3(x2)) 4: comp_f_g#1(comp_f_g(x3, x4), walk_xs_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xs_3#1(x2, x1)) 5: comp_f_g#1(walk_xs(), walk_xs_3(x5), x3) -> walk_xs_3#1(x5, x3) 6: main(Nil()) -> Nil() 7: main(Cons(x4, x5)) -> comp_f_g#1(walk#1(x5), walk_xs_3(x4), Nil()) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list comp_f_g :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list comp_f_g#1 :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list main :: 'l list -> 'l list walk#1 :: 'l list -> 'l list -> 'l list walk_xs :: 'l list -> 'l list walk_xs_3 :: 'l -> 'l list -> 'l list walk_xs_3#1 :: 'l -> 'l list -> 'l list + Applied Processor: ToTctProblem + Details: none * Step 19: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: comp_f_g#1(comp_f_g(x3,x4),walk_xs_3(x2),x1) -> comp_f_g#1(x3,x4,walk_xs_3#1(x2,x1)) comp_f_g#1(walk_xs(),walk_xs_3(x5),x3) -> walk_xs_3#1(x5,x3) main(Cons(x4,x5)) -> comp_f_g#1(walk#1(x5),walk_xs_3(x4),Nil()) main(Nil()) -> Nil() walk#1(Cons(x2,x7)) -> comp_f_g(walk#1(x7),walk_xs_3(x2)) walk#1(Nil()) -> walk_xs() walk_xs_3#1(x4,x6) -> Cons(x4,x6) - Signature: {comp_f_g#1/3,main/1,walk#1/1,walk_xs_3#1/2} / {Cons/2,Nil/0,comp_f_g/2,walk_xs/0,walk_xs_3/1} - 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"(15) x "A"(15)] -(15)-> "A"(15) F (TrsFun "Cons") :: ["A"(14) x "A"(14)] -(14)-> "A"(14) F (TrsFun "Cons") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "Nil") :: [] -(0)-> "A"(15) F (TrsFun "Nil") :: [] -(0)-> "A"(14) F (TrsFun "Nil") :: [] -(0)-> "A"(7) F (TrsFun "comp_f_g") :: ["A"(8) x "A"(8)] -(0)-> "A"(8) F (TrsFun "comp_f_g#1") :: ["A"(8) x "A"(8) x "A"(0)] -(15)-> "A"(0) F (TrsFun "main") :: ["A"(15)] -(13)-> "A"(0) F (TrsFun "walk#1") :: ["A"(14)] -(2)-> "A"(8) F (TrsFun "walk_xs") :: [] -(0)-> "A"(8) F (TrsFun "walk_xs") :: [] -(0)-> "A"(15) F (TrsFun "walk_xs_3") :: ["A"(8)] -(8)-> "A"(8) F (TrsFun "walk_xs_3") :: ["A"(12)] -(12)-> "A"(12) F (TrsFun "walk_xs_3#1") :: ["A"(0) x "A"(0)] -(1)-> "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) "F (TrsFun \"comp_f_g\")_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "F (TrsFun \"walk_xs\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"walk_xs_3\")_A" :: ["A"(0)] -(1)-> "A"(1) WORST_CASE(?,O(n^1))