WORST_CASE(?,O(n^1)) * Step 1: Desugar WORST_CASE(?,O(n^1)) + Considered Problem: type 'a list = Nil | Cons of 'a * 'a list;; type 'a tree = Leaf of 'a | Node of 'a tree * 'a tree;; let cons x xs = Cons(x,xs) ;; let comp f g x = f (g x) ;; let rec walk t = match t with | Leaf(x) -> cons x | Node(t1,t2) -> comp (walk t1) (walk t2) ;; let flatten t = walk t Nil ;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization WORST_CASE(?,O(n^1)) + Considered Problem: λt : 'a24 tree. (λcons : 'a24 -> 'a24 list -> 'a24 list. (λcomp : ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list. (λwalk : 'a24 tree -> 'a24 list -> 'a24 list. (λflatten : 'a24 tree -> 'a24 list. flatten t) (λt : 'a24 tree. walk t Nil)) (μwalk : 'a24 tree -> 'a24 list -> 'a24 list. λt : 'a24 tree. case t of | Leaf -> λx : 'a24. cons x | Node -> λt1 : 'a24 tree. λt2 : 'a24 tree. comp (walk t1) (walk t2))) (λf : 'a24 list -> 'a24 list. λg : 'a24 list -> 'a24 list. λx : 'a24 list. f (g x))) (λx : 'a24. λxs : 'a24 list. Cons(x,xs)) : 'a24 tree -> 'a24 list where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree + Applied Processor: Defunctionalization + Details: none * Step 3: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: flatten(x3) x4 -> x3 x4 Nil() 3: main_3(x0) x3 -> main_4(x0) flatten(x3) 4: cond_walk_t(Leaf(x4), x1, x2) -> x1 x4 5: cond_walk_t(Node(x4, x5), x1, x2) -> x2 (walk(x1, x2) x4) (walk(x1, x2) x5) 6: walk_1(x1, x2) x3 -> cond_walk_t(x3, x1, x2) 7: walk(x1, x2) x3 -> walk_1(x1, x2) x3 8: main_2(x0, x1) x2 -> main_3(x0) walk(x1, x2) 9: comp_f_g(x2, x3) x4 -> x2 (x3 x4) 10: comp_f(x2) x3 -> comp_f_g(x2, x3) 11: comp() x2 -> comp_f(x2) 12: main_1(x0) x1 -> main_2(x0, x1) comp() 13: cons_x(x1) x2 -> Cons(x1, x2) 14: cons() x1 -> cons_x(x1) 15: main(x0) -> main_1(x0) cons() where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons :: 'a24 -> 'a24 list -> 'a24 list comp_f :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list flatten :: ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons_x :: 'a24 -> 'a24 list -> 'a24 list main_1 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> 'a24 list walk_1 :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list main_2 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 list main_3 :: 'a24 tree -> ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 list main_4 :: 'a24 tree -> ('a24 tree -> 'a24 list) -> 'a24 list cond_walk_t :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 list -> 'a24 list walk :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list main :: 'a24 tree -> 'a24 list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: flatten(x3) x4 -> x3 x4 Nil() 3: main_3(x0) x7 -> flatten(x7) x0 4: cond_walk_t(Leaf(x4), x1, x2) -> x1 x4 5: cond_walk_t(Node(x4, x5), x1, x2) -> x2 (walk(x1, x2) x4) (walk(x1, x2) x5) 6: walk_1(x1, x2) x3 -> cond_walk_t(x3, x1, x2) 7: walk(x2, x4) x6 -> cond_walk_t(x6, x2, x4) 8: main_2(x0, x3) x5 -> main_4(x0) flatten(walk(x3, x5)) 9: comp_f_g(x2, x3) x4 -> x2 (x3 x4) 10: comp_f(x2) x3 -> comp_f_g(x2, x3) 11: comp() x2 -> comp_f(x2) 12: main_1(x0) x2 -> main_3(x0) walk(x2, comp()) 13: cons_x(x1) x2 -> Cons(x1, x2) 14: cons() x1 -> cons_x(x1) 15: main(x0) -> main_2(x0, cons()) comp() where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons :: 'a24 -> 'a24 list -> 'a24 list comp_f :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list flatten :: ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons_x :: 'a24 -> 'a24 list -> 'a24 list main_1 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> 'a24 list walk_1 :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list main_2 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 list main_3 :: 'a24 tree -> ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 list main_4 :: 'a24 tree -> ('a24 tree -> 'a24 list) -> 'a24 list cond_walk_t :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 list -> 'a24 list walk :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list main :: 'a24 tree -> 'a24 list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 5: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: flatten(x3) x4 -> x3 x4 Nil() 3: main_3(x8) x6 -> x6 x8 Nil() 4: cond_walk_t(Leaf(x4), x1, x2) -> x1 x4 5: cond_walk_t(Node(x4, x5), x1, x2) -> x2 (walk(x1, x2) x4) (walk(x1, x2) x5) 6: walk_1(x1, x2) x3 -> cond_walk_t(x3, x1, x2) 7: walk(x2, x4) x6 -> cond_walk_t(x6, x2, x4) 8: main_2(x0, x7) x11 -> flatten(walk(x7, x11)) x0 9: comp_f_g(x2, x3) x4 -> x2 (x3 x4) 10: comp_f(x2) x3 -> comp_f_g(x2, x3) 11: comp() x2 -> comp_f(x2) 12: main_1(x0) x5 -> flatten(walk(x5, comp())) x0 13: cons_x(x1) x2 -> Cons(x1, x2) 14: cons() x1 -> cons_x(x1) 15: main(x0) -> main_4(x0) flatten(walk(cons(), comp())) where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons :: 'a24 -> 'a24 list -> 'a24 list comp_f :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list flatten :: ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons_x :: 'a24 -> 'a24 list -> 'a24 list main_1 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> 'a24 list walk_1 :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list main_2 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 list main_3 :: 'a24 tree -> ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 list main_4 :: 'a24 tree -> ('a24 tree -> 'a24 list) -> 'a24 list cond_walk_t :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 list -> 'a24 list walk :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list main :: 'a24 tree -> 'a24 list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 6: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: flatten(x3) x4 -> x3 x4 Nil() 3: main_3(x8) x6 -> x6 x8 Nil() 4: cond_walk_t(Leaf(x4), x1, x2) -> x1 x4 5: cond_walk_t(Node(x4, x5), x1, x2) -> x2 (walk(x1, x2) x4) (walk(x1, x2) x5) 6: walk_1(x1, x2) x3 -> cond_walk_t(x3, x1, x2) 7: walk(x2, x4) x6 -> cond_walk_t(x6, x2, x4) 8: main_2(x8, x15) x23 -> walk(x15, x23) x8 Nil() 9: comp_f_g(x2, x3) x4 -> x2 (x3 x4) 10: comp_f(x2) x3 -> comp_f_g(x2, x3) 11: comp() x2 -> comp_f(x2) 12: main_1(x8) x11 -> walk(x11, comp()) x8 Nil() 13: cons_x(x1) x2 -> Cons(x1, x2) 14: cons() x1 -> cons_x(x1) 15: main(x0) -> flatten(walk(cons(), comp())) x0 where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons :: 'a24 -> 'a24 list -> 'a24 list comp_f :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list flatten :: ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons_x :: 'a24 -> 'a24 list -> 'a24 list main_1 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> 'a24 list walk_1 :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list main_2 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 list main_3 :: 'a24 tree -> ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 list main_4 :: 'a24 tree -> ('a24 tree -> 'a24 list) -> 'a24 list cond_walk_t :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 list -> 'a24 list walk :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list main :: 'a24 tree -> 'a24 list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 7: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: flatten(x3) x4 -> x3 x4 Nil() 3: main_3(x8) x6 -> x6 x8 Nil() 4: cond_walk_t(Leaf(x4), x1, x2) -> x1 x4 5: cond_walk_t(Node(x4, x5), x1, x2) -> x2 (walk(x1, x2) x4) (walk(x1, x2) x5) 6: walk_1(x1, x2) x3 -> cond_walk_t(x3, x1, x2) 7: walk(x2, x4) x6 -> cond_walk_t(x6, x2, x4) 8: main_2(x8, x15) x23 -> walk(x15, x23) x8 Nil() 9: comp_f_g(x2, x3) x4 -> x2 (x3 x4) 10: comp_f(x2) x3 -> comp_f_g(x2, x3) 11: comp() x2 -> comp_f(x2) 12: main_1(x8) x11 -> walk(x11, comp()) x8 Nil() 13: cons_x(x1) x2 -> Cons(x1, x2) 14: cons() x1 -> cons_x(x1) 15: main(x8) -> walk(cons(), comp()) x8 Nil() where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons :: 'a24 -> 'a24 list -> 'a24 list comp_f :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list flatten :: ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons_x :: 'a24 -> 'a24 list -> 'a24 list main_1 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> 'a24 list walk_1 :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list main_2 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 list main_3 :: 'a24 tree -> ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 list main_4 :: 'a24 tree -> ('a24 tree -> 'a24 list) -> 'a24 list cond_walk_t :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 list -> 'a24 list walk :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list main :: 'a24 tree -> 'a24 list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 8: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: flatten(x3) x4 -> x3 x4 Nil() 3: main_3(x8) x6 -> x6 x8 Nil() 4: cond_walk_t(Leaf(x4), x1, x2) -> x1 x4 5: cond_walk_t(Node(x4, x5), x1, x2) -> x2 (walk(x1, x2) x4) (walk(x1, x2) x5) 6: walk_1(x2, x4) Leaf(x8) -> x2 x8 7: walk_1(x2, x4) Node(x8, x10) -> x4 (walk(x2, x4) x8) (walk(x2, x4) x10) 8: walk(x2, x4) Leaf(x8) -> x2 x8 9: walk(x2, x4) Node(x8, x10) -> x4 (walk(x2, x4) x8) (walk(x2, x4) x10) 10: main_2(x8, x15) x23 -> walk(x15, x23) x8 Nil() 11: comp_f_g(x2, x3) x4 -> x2 (x3 x4) 12: comp_f(x2) x3 -> comp_f_g(x2, x3) 13: comp() x2 -> comp_f(x2) 14: main_1(x8) x11 -> walk(x11, comp()) x8 Nil() 15: cons_x(x1) x2 -> Cons(x1, x2) 16: cons() x1 -> cons_x(x1) 17: main(x8) -> walk(cons(), comp()) x8 Nil() where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons :: 'a24 -> 'a24 list -> 'a24 list comp_f :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list flatten :: ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons_x :: 'a24 -> 'a24 list -> 'a24 list main_1 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> 'a24 list walk_1 :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list main_2 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 list main_3 :: 'a24 tree -> ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 list main_4 :: 'a24 tree -> ('a24 tree -> 'a24 list) -> 'a24 list cond_walk_t :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 list -> 'a24 list walk :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list main :: 'a24 tree -> 'a24 list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 9: NeededRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: flatten(x3) x4 -> x3 x4 Nil() 3: main_3(x8) x6 -> x6 x8 Nil() 6: walk_1(x2, x4) Leaf(x8) -> x2 x8 7: walk_1(x2, x4) Node(x8, x10) -> x4 (walk(x2, x4) x8) (walk(x2, x4) x10) 8: walk(x2, x4) Leaf(x8) -> x2 x8 9: walk(x2, x4) Node(x8, x10) -> x4 (walk(x2, x4) x8) (walk(x2, x4) x10) 10: main_2(x8, x15) x23 -> walk(x15, x23) x8 Nil() 11: comp_f_g(x2, x3) x4 -> x2 (x3 x4) 12: comp_f(x2) x3 -> comp_f_g(x2, x3) 13: comp() x2 -> comp_f(x2) 14: main_1(x8) x11 -> walk(x11, comp()) x8 Nil() 15: cons_x(x1) x2 -> Cons(x1, x2) 16: cons() x1 -> cons_x(x1) 17: main(x8) -> walk(cons(), comp()) x8 Nil() where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons :: 'a24 -> 'a24 list -> 'a24 list comp_f :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list flatten :: ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons_x :: 'a24 -> 'a24 list -> 'a24 list main_1 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> 'a24 list walk_1 :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list main_2 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 list main_3 :: 'a24 tree -> ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 list main_4 :: 'a24 tree -> ('a24 tree -> 'a24 list) -> 'a24 list walk :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list main :: 'a24 tree -> 'a24 list + Applied Processor: NeededRules + Details: none * Step 10: CFA WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: flatten(x3) x4 -> x3 x4 Nil() 3: main_3(x8) x6 -> x6 x8 Nil() 4: walk_1(x2, x4) Leaf(x8) -> x2 x8 5: walk_1(x2, x4) Node(x8, x10) -> x4 (walk(x2, x4) x8) (walk(x2, x4) x10) 6: walk(x2, x4) Leaf(x8) -> x2 x8 7: walk(x2, x4) Node(x8, x10) -> x4 (walk(x2, x4) x8) (walk(x2, x4) x10) 8: main_2(x8, x15) x23 -> walk(x15, x23) x8 Nil() 9: comp_f_g(x2, x3) x4 -> x2 (x3 x4) 10: comp_f(x2) x3 -> comp_f_g(x2, x3) 11: comp() x2 -> comp_f(x2) 12: main_1(x8) x11 -> walk(x11, comp()) x8 Nil() 13: cons_x(x1) x2 -> Cons(x1, x2) 14: cons() x1 -> cons_x(x1) 15: main(x8) -> walk(cons(), comp()) x8 Nil() where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons :: 'a24 -> 'a24 list -> 'a24 list comp_f :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list flatten :: ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons_x :: 'a24 -> 'a24 list -> 'a24 list main_1 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> 'a24 list walk_1 :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list main_2 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 list main_3 :: 'a24 tree -> ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 list main_4 :: 'a24 tree -> ('a24 tree -> 'a24 list) -> 'a24 list walk :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list main :: 'a24 tree -> 'a24 list + Applied Processor: CFA {cfaRefinement = } + Details: {X{*} -> Nil() | Cons(X{*},X{*}) | Nil() | Nil() | Node(X{*},X{*}) | Leaf(X{*}) | Node(X{*},X{*}) | Leaf(X{*}) | Nil() | Nil() ,V{x1_13} -> V{x1_14} ,V{x1_14} -> V{x8_6} ,V{x2_6} -> V{x2_7} | cons() ,V{x2_7} -> V{x2_7} | cons() ,V{x2_9} -> V{x2_10} ,V{x2_10} -> V{x2_11} ,V{x2_11} -> R{7} | R{6} ,V{x2_13} -> R{9} | R{13} | V{x4_9} | Nil() ,V{x3_9} -> V{x3_10} ,V{x3_10} -> R{7} | R{6} ,V{x4_6} -> V{x4_7} | comp() ,V{x4_7} -> V{x4_7} | comp() ,V{x4_9} -> R{9} | R{13} | V{x4_9} | Nil() ,V{x8_6} -> X{*} ,V{x8_7} -> X{*} ,V{x8_15} -> X{*} ,V{x10_7} -> X{*} ,R{0} -> R{15} | main(X{*}) ,R{6} -> R{14} | @(V{x2_6},V{x8_6}) ,R{7} -> R{10} | @(R{11},R{7}) | @(R{11},R{6}) | @(R{11},@(walk(V{x2_7},V{x4_7}),V{x10_7})) | @(@(V{x4_7},R{7}),R{6}) | @(@(V{x4_7},R{6}),R{6}) | @(@(V{x4_7},R{7}),R{7}) | @(@(V{x4_7},R{6}),R{7}) | @(@(V{x4_7},@(walk(V{x2_7},V{x4_7}),V{x8_7})),R{7}) | @(@(V{x4_7},@(walk(V{x2_7},V{x4_7}),V{x8_7})),R{6}) | @(@(V{x4_7},R{7}),@(walk(V{x2_7},V{x4_7}),V{x10_7})) | @(@(V{x4_7},R{6}),@(walk(V{x2_7},V{x4_7}),V{x10_7})) | @(@(V{x4_7},@(walk(V{x2_7},V{x4_7}),V{x8_7})),@(walk(V{x2_7},V{x4_7}),V{x10_7})) ,R{9} -> R{13} | R{9} | @(V{x2_9},R{13}) | @(V{x2_9},R{9}) | @(V{x2_9},@(V{x3_9},V{x4_9})) ,R{10} -> comp_f_g(V{x2_10},V{x3_10}) ,R{11} -> comp_f(V{x2_11}) ,R{13} -> Cons(V{x1_13},V{x2_13}) ,R{14} -> cons_x(V{x1_14}) ,R{15} -> R{9} | R{13} | @(R{7},Nil()) | @(R{6},Nil()) | @(@(walk(cons(),comp()),V{x8_15}),Nil())} * Step 11: UncurryATRS WORST_CASE(?,O(n^1)) + Considered Problem: 6: walk(cons(), comp()) Leaf(x1) -> cons() x1 7: walk(cons(), comp()) Node(x2, x1) -> comp() (walk(cons(), comp()) x2) (walk(cons(), comp()) x1) 9: comp_f_g(comp_f_g(x4, x5), comp_f_g(x2, x3)) x1 -> comp_f_g(x4, x5) (comp_f_g(x2, x3) x1) 10: comp_f_g(comp_f_g(x3, x4), cons_x(x2)) x1 -> comp_f_g(x3, x4) (cons_x(x2) x1) 11: comp_f_g(cons_x(x4), comp_f_g(x2, x3)) x1 -> cons_x(x4) (comp_f_g(x2, x3) x1) 12: comp_f_g(cons_x(x3), cons_x(x2)) x1 -> cons_x(x3) (cons_x(x2) x1) 13: comp_f(x2) x3 -> comp_f_g(x2, x3) 14: comp() x2 -> comp_f(x2) 16: cons_x(x1) x2 -> Cons(x1, x2) 17: cons() x1 -> cons_x(x1) 18: main(x1) -> walk(cons(), comp()) x1 Nil() where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons :: 'a24 -> 'a24 list -> 'a24 list comp_f :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons_x :: 'a24 -> 'a24 list -> 'a24 list walk :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list main :: 'a24 tree -> 'a24 list + Applied Processor: UncurryATRS + Details: none * Step 12: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk#1(cons(), comp(), Leaf(x1)) -> cons#1(x1) 2: walk#2(cons(), comp(), Leaf(x1), x2) -> cons#2(x1, x2) 3: walk#1(cons(), comp(), Node(x2, x1)) -> comp#2(walk#1(cons(), comp(), x2), walk#1(cons(), comp(), x1)) 4: walk#2(cons(), comp(), Node(x2, x1), x3) -> comp#3(walk#1(cons(), comp(), x2), walk#1(cons(), comp(), x1) , x3) 5: comp_f_g#1(comp_f_g(x4, x5), comp_f_g(x2, x3), x1) -> comp_f_g#1(x4, x5, comp_f_g#1(x2, x3, x1)) 6: comp_f_g#1(comp_f_g(x3, x4), cons_x(x2), x1) -> comp_f_g#1(x3, x4, cons_x#1(x2, x1)) 7: comp_f_g#1(cons_x(x4), comp_f_g(x2, x3), x1) -> cons_x#1(x4, comp_f_g#1(x2, x3, x1)) 8: comp_f_g#1(cons_x(x3), cons_x(x2), x1) -> cons_x#1(x3, cons_x#1(x2, x1)) 9: comp_f#1(x2, x3) -> comp_f_g(x2, x3) 10: comp_f#2(x2, x3, x4) -> comp_f_g#1(x2, x3, x4) 11: comp#1(x2) -> comp_f(x2) 12: comp#2(x2, x3) -> comp_f#1(x2, x3) 13: comp#3(x2, x3, x4) -> comp_f#2(x2, x3, x4) 14: cons_x#1(x1, x2) -> Cons(x1, x2) 15: cons#1(x1) -> cons_x(x1) 16: cons#2(x1, x2) -> cons_x#1(x1, x2) 17: main(x1) -> walk#2(cons(), comp(), x1, Nil()) where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp#2 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp#3 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f#2 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f_g#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons :: 'a24 -> 'a24 list -> 'a24 list cons#1 :: 'a24 -> 'a24 list -> 'a24 list cons#2 :: 'a24 -> 'a24 list -> 'a24 list cons_x :: 'a24 -> 'a24 list -> 'a24 list cons_x#1 :: 'a24 -> 'a24 list -> 'a24 list main :: 'a24 tree -> 'a24 list walk#1 :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list walk#2 :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 13: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk#1(cons(), comp(), Leaf(x1)) -> cons#1(x1) 2: walk#2(cons(), comp(), Leaf(x1), x2) -> cons#2(x1, x2) 3: walk#1(cons(), comp(), Node(x2, x1)) -> comp#2(walk#1(cons(), comp(), x2), walk#1(cons(), comp(), x1)) 4: walk#2(cons(), comp(), Node(x2, x1), x3) -> comp#3(walk#1(cons(), comp(), x2), walk#1(cons(), comp(), x1) , x3) 5: comp_f_g#1(comp_f_g(x4, x5), comp_f_g(x2, x3), x1) -> comp_f_g#1(x4, x5, comp_f_g#1(x2, x3, x1)) 6: comp_f_g#1(comp_f_g(x3, x4), cons_x(x2), x1) -> comp_f_g#1(x3, x4, cons_x#1(x2, x1)) 7: comp_f_g#1(cons_x(x4), comp_f_g(x2, x3), x1) -> cons_x#1(x4, comp_f_g#1(x2, x3, x1)) 8: comp_f_g#1(cons_x(x3), cons_x(x2), x1) -> cons_x#1(x3, cons_x#1(x2, x1)) 9: comp_f#1(x2, x3) -> comp_f_g(x2, x3) 10: comp_f#2(x2, x3, x4) -> comp_f_g#1(x2, x3, x4) 12: comp#2(x2, x3) -> comp_f#1(x2, x3) 13: comp#3(x2, x3, x4) -> comp_f#2(x2, x3, x4) 14: cons_x#1(x1, x2) -> Cons(x1, x2) 15: cons#1(x1) -> cons_x(x1) 16: cons#2(x1, x2) -> cons_x#1(x1, x2) 17: main(x1) -> walk#2(cons(), comp(), x1, Nil()) where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp#2 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp#3 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f#2 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f_g#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons :: 'a24 -> 'a24 list -> 'a24 list cons#1 :: 'a24 -> 'a24 list -> 'a24 list cons#2 :: 'a24 -> 'a24 list -> 'a24 list cons_x :: 'a24 -> 'a24 list -> 'a24 list cons_x#1 :: 'a24 -> 'a24 list -> 'a24 list main :: 'a24 tree -> 'a24 list walk#1 :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list walk#2 :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 14: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk#1(cons(), comp(), Leaf(x2)) -> cons_x(x2) 2: walk#2(cons(), comp(), Leaf(x2), x4) -> cons_x#1(x2, x4) 3: walk#1(cons(), comp(), Node(x5, x3)) -> comp_f#1(walk#1(cons(), comp(), x5), walk#1(cons(), comp(), x3)) 4: walk#2(cons(), comp(), Node(x5, x3), x8) -> comp_f#2(walk#1(cons(), comp(), x5), walk#1(cons(), comp() , x3) , x8) 5: comp_f_g#1(comp_f_g(x4, x5), comp_f_g(x2, x3), x1) -> comp_f_g#1(x4, x5, comp_f_g#1(x2, x3, x1)) 6: comp_f_g#1(comp_f_g(x3, x4), cons_x(x2), x1) -> comp_f_g#1(x3, x4, cons_x#1(x2, x1)) 7: comp_f_g#1(cons_x(x4), comp_f_g(x2, x3), x1) -> cons_x#1(x4, comp_f_g#1(x2, x3, x1)) 8: comp_f_g#1(cons_x(x3), cons_x(x2), x1) -> cons_x#1(x3, cons_x#1(x2, x1)) 9: comp_f#1(x2, x3) -> comp_f_g(x2, x3) 10: comp_f#2(x2, x3, x4) -> comp_f_g#1(x2, x3, x4) 11: comp#2(x4, x6) -> comp_f_g(x4, x6) 12: comp#3(x4, x6, x8) -> comp_f_g#1(x4, x6, x8) 13: cons_x#1(x1, x2) -> Cons(x1, x2) 14: cons#1(x1) -> cons_x(x1) 15: cons#2(x1, x2) -> cons_x#1(x1, x2) 16: main(Leaf(x2)) -> cons#2(x2, Nil()) 17: main(Node(x4, x2)) -> comp#3(walk#1(cons(), comp(), x4), walk#1(cons(), comp(), x2), Nil()) where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp#2 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp#3 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f#2 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f_g#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons :: 'a24 -> 'a24 list -> 'a24 list cons#1 :: 'a24 -> 'a24 list -> 'a24 list cons#2 :: 'a24 -> 'a24 list -> 'a24 list cons_x :: 'a24 -> 'a24 list -> 'a24 list cons_x#1 :: 'a24 -> 'a24 list -> 'a24 list main :: 'a24 tree -> 'a24 list walk#1 :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list walk#2 :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 15: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk#1(cons(), comp(), Leaf(x2)) -> cons_x(x2) 3: walk#1(cons(), comp(), Node(x5, x3)) -> comp_f#1(walk#1(cons(), comp(), x5), walk#1(cons(), comp(), x3)) 5: comp_f_g#1(comp_f_g(x4, x5), comp_f_g(x2, x3), x1) -> comp_f_g#1(x4, x5, comp_f_g#1(x2, x3, x1)) 6: comp_f_g#1(comp_f_g(x3, x4), cons_x(x2), x1) -> comp_f_g#1(x3, x4, cons_x#1(x2, x1)) 7: comp_f_g#1(cons_x(x4), comp_f_g(x2, x3), x1) -> cons_x#1(x4, comp_f_g#1(x2, x3, x1)) 8: comp_f_g#1(cons_x(x3), cons_x(x2), x1) -> cons_x#1(x3, cons_x#1(x2, x1)) 9: comp_f#1(x2, x3) -> comp_f_g(x2, x3) 12: comp#3(x4, x6, x8) -> comp_f_g#1(x4, x6, x8) 13: cons_x#1(x1, x2) -> Cons(x1, x2) 15: cons#2(x1, x2) -> cons_x#1(x1, x2) 16: main(Leaf(x2)) -> cons#2(x2, Nil()) 17: main(Node(x4, x2)) -> comp#3(walk#1(cons(), comp(), x4), walk#1(cons(), comp(), x2), Nil()) where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp#3 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f_g#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons :: 'a24 -> 'a24 list -> 'a24 list cons#2 :: 'a24 -> 'a24 list -> 'a24 list cons_x :: 'a24 -> 'a24 list -> 'a24 list cons_x#1 :: 'a24 -> 'a24 list -> 'a24 list main :: 'a24 tree -> 'a24 list walk#1 :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 16: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk#1(cons(), comp(), Leaf(x2)) -> cons_x(x2) 2: walk#1(cons(), comp(), Node(x11, x7)) -> comp_f_g(walk#1(cons(), comp(), x11), walk#1(cons(), comp() , x7)) 3: comp_f_g#1(comp_f_g(x4, x5), comp_f_g(x2, x3), x1) -> comp_f_g#1(x4, x5, comp_f_g#1(x2, x3, x1)) 4: comp_f_g#1(comp_f_g(x3, x4), cons_x(x2), x1) -> comp_f_g#1(x3, x4, cons_x#1(x2, x1)) 5: comp_f_g#1(cons_x(x4), comp_f_g(x2, x3), x1) -> cons_x#1(x4, comp_f_g#1(x2, x3, x1)) 6: comp_f_g#1(cons_x(x3), cons_x(x2), x1) -> cons_x#1(x3, cons_x#1(x2, x1)) 7: comp_f#1(x2, x3) -> comp_f_g(x2, x3) 8: comp#3(x4, x6, x8) -> comp_f_g#1(x4, x6, x8) 9: cons_x#1(x1, x2) -> Cons(x1, x2) 10: cons#2(x1, x2) -> cons_x#1(x1, x2) 11: main(Leaf(x2)) -> cons_x#1(x2, Nil()) 12: main(Node(x9, x5)) -> comp_f_g#1(walk#1(cons(), comp(), x9), walk#1(cons(), comp(), x5), Nil()) where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp#3 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f_g#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons :: 'a24 -> 'a24 list -> 'a24 list cons#2 :: 'a24 -> 'a24 list -> 'a24 list cons_x :: 'a24 -> 'a24 list -> 'a24 list cons_x#1 :: 'a24 -> 'a24 list -> 'a24 list main :: 'a24 tree -> 'a24 list walk#1 :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 17: Compression WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk#1(cons(), comp(), Leaf(x2)) -> cons_x(x2) 2: walk#1(cons(), comp(), Node(x11, x7)) -> comp_f_g(walk#1(cons(), comp(), x11), walk#1(cons(), comp() , x7)) 3: comp_f_g#1(comp_f_g(x4, x5), comp_f_g(x2, x3), x1) -> comp_f_g#1(x4, x5, comp_f_g#1(x2, x3, x1)) 4: comp_f_g#1(comp_f_g(x3, x4), cons_x(x2), x1) -> comp_f_g#1(x3, x4, cons_x#1(x2, x1)) 5: comp_f_g#1(cons_x(x4), comp_f_g(x2, x3), x1) -> cons_x#1(x4, comp_f_g#1(x2, x3, x1)) 6: comp_f_g#1(cons_x(x3), cons_x(x2), x1) -> cons_x#1(x3, cons_x#1(x2, x1)) 9: cons_x#1(x1, x2) -> Cons(x1, x2) 11: main(Leaf(x2)) -> cons_x#1(x2, Nil()) 12: main(Node(x9, x5)) -> comp_f_g#1(walk#1(cons(), comp(), x9), walk#1(cons(), comp(), x5), Nil()) where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f_g#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons :: 'a24 -> 'a24 list -> 'a24 list cons_x :: 'a24 -> 'a24 list -> 'a24 list cons_x#1 :: 'a24 -> 'a24 list -> 'a24 list main :: 'a24 tree -> 'a24 list walk#1 :: ('a24 -> 'a24 list -> 'a24 list) -> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list -> 'a24 list + Applied Processor: Compression + Details: none * Step 18: ToTctProblem WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk#1(Leaf(x2)) -> cons_x(x2) 2: walk#1(Node(x11, x7)) -> comp_f_g(walk#1(x11), walk#1(x7)) 3: comp_f_g#1(comp_f_g(x4, x5), comp_f_g(x2, x3), x1) -> comp_f_g#1(x4, x5, comp_f_g#1(x2, x3, x1)) 4: comp_f_g#1(comp_f_g(x3, x4), cons_x(x2), x1) -> comp_f_g#1(x3, x4, cons_x#1(x2, x1)) 5: comp_f_g#1(cons_x(x4), comp_f_g(x2, x3), x1) -> cons_x#1(x4, comp_f_g#1(x2, x3, x1)) 6: comp_f_g#1(cons_x(x3), cons_x(x2), x1) -> cons_x#1(x3, cons_x#1(x2, x1)) 7: cons_x#1(x1, x2) -> Cons(x1, x2) 8: main(Leaf(x2)) -> cons_x#1(x2, Nil()) 9: main(Node(x9, x5)) -> comp_f_g#1(walk#1(x9), walk#1(x5), Nil()) where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list comp_f_g#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list cons_x :: 'a24 -> 'a24 list -> 'a24 list cons_x#1 :: 'a24 -> 'a24 list -> 'a24 list main :: 'a24 tree -> 'a24 list walk#1 :: 'a24 tree -> 'a24 list -> 'a24 list + Applied Processor: ToTctProblem + Details: none * Step 19: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: comp_f_g#1(comp_f_g(x3,x4),cons_x(x2),x1) -> comp_f_g#1(x3,x4,cons_x#1(x2,x1)) comp_f_g#1(comp_f_g(x4,x5),comp_f_g(x2,x3),x1) -> comp_f_g#1(x4,x5,comp_f_g#1(x2,x3,x1)) comp_f_g#1(cons_x(x3),cons_x(x2),x1) -> cons_x#1(x3,cons_x#1(x2,x1)) comp_f_g#1(cons_x(x4),comp_f_g(x2,x3),x1) -> cons_x#1(x4,comp_f_g#1(x2,x3,x1)) cons_x#1(x1,x2) -> Cons(x1,x2) main(Leaf(x2)) -> cons_x#1(x2,Nil()) main(Node(x9,x5)) -> comp_f_g#1(walk#1(x9),walk#1(x5),Nil()) walk#1(Leaf(x2)) -> cons_x(x2) walk#1(Node(x11,x7)) -> comp_f_g(walk#1(x11),walk#1(x7)) - Signature: {comp_f_g#1/3,cons_x#1/2,main/1,walk#1/1} / {Cons/2,Leaf/1,Nil/0,Node/2,comp_f_g/2,cons_x/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Leaf,Nil,Node} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(comp_f_g) = {1,2}, uargs(comp_f_g#1) = {1,2,3}, uargs(cons_x#1) = {2} Following symbols are considered usable: {comp_f_g#1,cons_x#1,main,walk#1} TcT has computed the following interpretation: p(Cons) = 0 p(Leaf) = 2 + x1 p(Nil) = 2 p(Node) = 3 + x1 + x2 p(comp_f_g) = 3 + x1 + x2 p(comp_f_g#1) = 2 + 2*x1 + 2*x2 + x3 p(cons_x) = x1 p(cons_x#1) = x2 p(main) = 2 + 3*x1 p(walk#1) = x1 Following rules are strictly oriented: comp_f_g#1(comp_f_g(x3,x4),cons_x(x2),x1) = 8 + x1 + 2*x2 + 2*x3 + 2*x4 > 2 + x1 + 2*x3 + 2*x4 = comp_f_g#1(x3,x4,cons_x#1(x2,x1)) comp_f_g#1(comp_f_g(x4,x5),comp_f_g(x2,x3),x1) = 14 + x1 + 2*x2 + 2*x3 + 2*x4 + 2*x5 > 4 + x1 + 2*x2 + 2*x3 + 2*x4 + 2*x5 = comp_f_g#1(x4,x5,comp_f_g#1(x2,x3,x1)) comp_f_g#1(cons_x(x3),cons_x(x2),x1) = 2 + x1 + 2*x2 + 2*x3 > x1 = cons_x#1(x3,cons_x#1(x2,x1)) comp_f_g#1(cons_x(x4),comp_f_g(x2,x3),x1) = 8 + x1 + 2*x2 + 2*x3 + 2*x4 > 2 + x1 + 2*x2 + 2*x3 = cons_x#1(x4,comp_f_g#1(x2,x3,x1)) main(Leaf(x2)) = 8 + 3*x2 > 2 = cons_x#1(x2,Nil()) main(Node(x9,x5)) = 11 + 3*x5 + 3*x9 > 4 + 2*x5 + 2*x9 = comp_f_g#1(walk#1(x9),walk#1(x5),Nil()) walk#1(Leaf(x2)) = 2 + x2 > x2 = cons_x(x2) Following rules are (at-least) weakly oriented: cons_x#1(x1,x2) = x2 >= 0 = Cons(x1,x2) walk#1(Node(x11,x7)) = 3 + x11 + x7 >= 3 + x11 + x7 = comp_f_g(walk#1(x11),walk#1(x7)) * Step 20: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: cons_x#1(x1,x2) -> Cons(x1,x2) walk#1(Node(x11,x7)) -> comp_f_g(walk#1(x11),walk#1(x7)) - Weak TRS: comp_f_g#1(comp_f_g(x3,x4),cons_x(x2),x1) -> comp_f_g#1(x3,x4,cons_x#1(x2,x1)) comp_f_g#1(comp_f_g(x4,x5),comp_f_g(x2,x3),x1) -> comp_f_g#1(x4,x5,comp_f_g#1(x2,x3,x1)) comp_f_g#1(cons_x(x3),cons_x(x2),x1) -> cons_x#1(x3,cons_x#1(x2,x1)) comp_f_g#1(cons_x(x4),comp_f_g(x2,x3),x1) -> cons_x#1(x4,comp_f_g#1(x2,x3,x1)) main(Leaf(x2)) -> cons_x#1(x2,Nil()) main(Node(x9,x5)) -> comp_f_g#1(walk#1(x9),walk#1(x5),Nil()) walk#1(Leaf(x2)) -> cons_x(x2) - Signature: {comp_f_g#1/3,cons_x#1/2,main/1,walk#1/1} / {Cons/2,Leaf/1,Nil/0,Node/2,comp_f_g/2,cons_x/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Leaf,Nil,Node} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(comp_f_g) = {1,2}, uargs(comp_f_g#1) = {1,2,3}, uargs(cons_x#1) = {2} Following symbols are considered usable: {comp_f_g#1,cons_x#1,main,walk#1} TcT has computed the following interpretation: p(Cons) = 1 p(Leaf) = 4 + x1 p(Nil) = 6 p(Node) = 7 + x1 + x2 p(comp_f_g) = x1 + x2 p(comp_f_g#1) = 2*x1 + 2*x2 + x3 p(cons_x) = 2 p(cons_x#1) = 3 + x2 p(main) = 1 + 2*x1 p(walk#1) = 1 + x1 Following rules are strictly oriented: cons_x#1(x1,x2) = 3 + x2 > 1 = Cons(x1,x2) walk#1(Node(x11,x7)) = 8 + x11 + x7 > 2 + x11 + x7 = comp_f_g(walk#1(x11),walk#1(x7)) Following rules are (at-least) weakly oriented: comp_f_g#1(comp_f_g(x3,x4),cons_x(x2),x1) = 4 + x1 + 2*x3 + 2*x4 >= 3 + x1 + 2*x3 + 2*x4 = comp_f_g#1(x3,x4,cons_x#1(x2,x1)) comp_f_g#1(comp_f_g(x4,x5),comp_f_g(x2,x3),x1) = x1 + 2*x2 + 2*x3 + 2*x4 + 2*x5 >= x1 + 2*x2 + 2*x3 + 2*x4 + 2*x5 = comp_f_g#1(x4,x5,comp_f_g#1(x2,x3,x1)) comp_f_g#1(cons_x(x3),cons_x(x2),x1) = 8 + x1 >= 6 + x1 = cons_x#1(x3,cons_x#1(x2,x1)) comp_f_g#1(cons_x(x4),comp_f_g(x2,x3),x1) = 4 + x1 + 2*x2 + 2*x3 >= 3 + x1 + 2*x2 + 2*x3 = cons_x#1(x4,comp_f_g#1(x2,x3,x1)) main(Leaf(x2)) = 9 + 2*x2 >= 9 = cons_x#1(x2,Nil()) main(Node(x9,x5)) = 15 + 2*x5 + 2*x9 >= 10 + 2*x5 + 2*x9 = comp_f_g#1(walk#1(x9),walk#1(x5),Nil()) walk#1(Leaf(x2)) = 5 + x2 >= 2 = cons_x(x2) * Step 21: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: comp_f_g#1(comp_f_g(x3,x4),cons_x(x2),x1) -> comp_f_g#1(x3,x4,cons_x#1(x2,x1)) comp_f_g#1(comp_f_g(x4,x5),comp_f_g(x2,x3),x1) -> comp_f_g#1(x4,x5,comp_f_g#1(x2,x3,x1)) comp_f_g#1(cons_x(x3),cons_x(x2),x1) -> cons_x#1(x3,cons_x#1(x2,x1)) comp_f_g#1(cons_x(x4),comp_f_g(x2,x3),x1) -> cons_x#1(x4,comp_f_g#1(x2,x3,x1)) cons_x#1(x1,x2) -> Cons(x1,x2) main(Leaf(x2)) -> cons_x#1(x2,Nil()) main(Node(x9,x5)) -> comp_f_g#1(walk#1(x9),walk#1(x5),Nil()) walk#1(Leaf(x2)) -> cons_x(x2) walk#1(Node(x11,x7)) -> comp_f_g(walk#1(x11),walk#1(x7)) - Signature: {comp_f_g#1/3,cons_x#1/2,main/1,walk#1/1} / {Cons/2,Leaf/1,Nil/0,Node/2,comp_f_g/2,cons_x/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Leaf,Nil,Node} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))