WORST_CASE(?,O(n^1)) * Step 1: Desugar WORST_CASE(?,O(n^1)) + Considered Problem: let rec leqNat y x = match y with | 0 -> True | S(y') -> (match x with | S(x') -> leqNat x' y' | 0 -> False) ;; let rec eqNat x y = match y with | 0 -> (match x with | 0 -> True | S(x') -> False) | S(y') -> (match x with | S(x') -> eqNat x' y' | 0 -> False) ;; let rec geqNat x y = match y with | 0 -> True | S(y') -> (match x with | 0 -> False | S(x') -> geqNat x' y') ;; let rec ltNat x y = match y with | 0 -> False | S(y') -> (match x with | 0 -> True | S(x') -> ltNat x' y') ;; let rec gtNat x y = match x with | 0 -> False | S(x') -> (match y with | 0 -> True | S(y') -> gtNat x' y') ;; let ifz n th el = match n with | 0 -> th 0 | S(x) -> el x ;; let ite b th el = match b with | True()-> th | False()-> el ;; let minus n m = let rec minus' m n = match m with | 0 -> 0 | S(x) -> (match n with | 0 -> m | S(y) -> minus' x y) in Pair(minus' n m,m) ;; let rec plus n m = match m with | 0 -> n | S(x) -> S(plus n x) ;; type ('a,'b,'c) triple = Triple of 'a * 'b * 'c ;; let rec div_mod n m = match (minus n m) with | Pair(res,m) -> (match res with | 0 -> Triple (0,n,m) | S(x) -> (match (div_mod res m) with | Triple(a,rest,unusedM) -> Triple(plus S(0) a,rest,m))) ;; let rec mult n m = match n with | 0 -> 0 | S(x) -> S(plus (mult x m) m) ;; type bool = True | False ;; type 'a option = None | Some of 'a ;; type 'a list = Nil | Cons of 'a * 'a list ;; type nat = 0 | S of nat ;; type Unit = Unit ;; type ('a,'b) pair = Pair of 'a * 'b (* let comp f g = fun z -> f (g z) * * let rec walk xs = * match xs with * | Nil -> (fun z -> z) * | Cons(x,ys) -> comp (walk ys) (fun z -> Cons(x,z)) * * let rev l = walk l Nil * * let main l = rev l *) ;; let comp f g = fun z -> f (g z);; let rec walk xs = match xs with | Nil()-> (fun z -> z) | Cons(x,ys) -> comp (walk ys) (fun z -> Cons(x,z));; let reverse xs = walk xs Nil ;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization WORST_CASE(?,O(n^1)) + Considered Problem: λxs : 'l list. (λcomp : ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list. (λwalk : 'l list -> 'l list -> 'l list. (λreverse : 'l list -> 'l list. reverse xs) (λxs : 'l list. walk xs Nil)) (μwalk : 'l list -> 'l list -> 'l list. λxs : 'l list. case xs of | Nil -> λz : 'l list. z | Cons -> λx : 'l. λys : 'l list. comp (walk ys) (λz : 'l list. Cons(x,z)))) (λf : 'l list -> 'l list. λg : 'l list -> 'l list. λz : 'l list. f (g z)) : 'l list -> 'l list where 0 :: nat Cons :: 'a -> 'a list -> 'a list False :: bool Nil :: 'a list None :: 'a option Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Some :: 'a -> 'a option Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple True :: bool Unit :: Unit + Applied Processor: Defunctionalization + Details: none * Step 3: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: reverse(x2) x3 -> x2 x3 Nil() 3: main_2(x0) x2 -> main_3(x0) reverse(x2) 4: walk_xs() x3 -> x3 5: walk_xs_3(x3) x5 -> Cons(x3, x5) 6: cond_walk_xs(Nil(), x1) -> walk_xs() 7: cond_walk_xs(Cons(x3, x4), x1) -> x1 (walk(x1) x4) walk_xs_3(x3) 8: walk_1(x1) x2 -> cond_walk_xs(x2, x1) 9: walk(x1) x2 -> walk_1(x1) x2 10: main_1(x0) x1 -> main_2(x0) walk(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 reverse :: ('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) -> 'l list main_3 :: '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_3(x0) x3 -> x3 x0 2: reverse(x2) x3 -> x2 x3 Nil() 3: main_2(x0) x5 -> reverse(x5) x0 4: walk_xs() x3 -> x3 5: walk_xs_3(x3) x5 -> Cons(x3, x5) 6: cond_walk_xs(Nil(), x1) -> walk_xs() 7: cond_walk_xs(Cons(x3, x4), x1) -> x1 (walk(x1) x4) walk_xs_3(x3) 8: walk_1(x1) x2 -> cond_walk_xs(x2, x1) 9: walk(x2) x4 -> cond_walk_xs(x4, x2) 10: main_1(x0) x3 -> main_3(x0) reverse(walk(x3)) 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) walk(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 reverse :: ('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) -> 'l list main_3 :: '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_3(x0) x3 -> x3 x0 2: reverse(x2) x3 -> x2 x3 Nil() 3: main_2(x6) x4 -> x4 x6 Nil() 4: walk_xs() x3 -> x3 5: walk_xs_3(x3) x5 -> Cons(x3, x5) 6: cond_walk_xs(Nil(), x1) -> walk_xs() 7: cond_walk_xs(Cons(x3, x4), x1) -> x1 (walk(x1) x4) walk_xs_3(x3) 8: walk_1(x1) x2 -> cond_walk_xs(x2, x1) 9: walk(x2) x4 -> cond_walk_xs(x4, x2) 10: main_1(x0) x7 -> reverse(walk(x7)) 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) -> reverse(walk(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 reverse :: ('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) -> 'l list main_3 :: '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_3(x0) x3 -> x3 x0 2: reverse(x2) x3 -> x2 x3 Nil() 3: main_2(x6) x4 -> x4 x6 Nil() 4: walk_xs() x3 -> x3 5: walk_xs_3(x3) x5 -> Cons(x3, x5) 6: cond_walk_xs(Nil(), x1) -> walk_xs() 7: cond_walk_xs(Cons(x3, x4), x1) -> x1 (walk(x1) x4) walk_xs_3(x3) 8: walk_1(x1) x2 -> cond_walk_xs(x2, x1) 9: walk(x2) x4 -> cond_walk_xs(x4, x2) 10: main_1(x6) x15 -> walk(x15) x6 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(x6) -> walk(comp()) x6 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 reverse :: ('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) -> 'l list main_3 :: '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_3(x0) x3 -> x3 x0 2: reverse(x2) x3 -> x2 x3 Nil() 3: main_2(x6) x4 -> x4 x6 Nil() 4: walk_xs() x3 -> x3 5: walk_xs_3(x3) x5 -> Cons(x3, x5) 6: cond_walk_xs(Nil(), x1) -> walk_xs() 7: cond_walk_xs(Cons(x3, x4), x1) -> x1 (walk(x1) x4) walk_xs_3(x3) 8: walk_1(x2) Nil() -> walk_xs() 9: walk_1(x2) Cons(x6, x8) -> x2 (walk(x2) x8) walk_xs_3(x6) 10: walk(x2) Nil() -> walk_xs() 11: walk(x2) Cons(x6, x8) -> x2 (walk(x2) x8) walk_xs_3(x6) 12: main_1(x6) x15 -> walk(x15) x6 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(x6) -> walk(comp()) x6 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 reverse :: ('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) -> 'l list main_3 :: '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_3(x0) x3 -> x3 x0 2: reverse(x2) x3 -> x2 x3 Nil() 3: main_2(x6) x4 -> x4 x6 Nil() 4: walk_xs() x3 -> x3 5: walk_xs_3(x3) x5 -> Cons(x3, x5) 8: walk_1(x2) Nil() -> walk_xs() 9: walk_1(x2) Cons(x6, x8) -> x2 (walk(x2) x8) walk_xs_3(x6) 10: walk(x2) Nil() -> walk_xs() 11: walk(x2) Cons(x6, x8) -> x2 (walk(x2) x8) walk_xs_3(x6) 12: main_1(x6) x15 -> walk(x15) x6 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(x6) -> walk(comp()) x6 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 reverse :: ('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) -> 'l list main_3 :: '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_3(x0) x3 -> x3 x0 2: reverse(x2) x3 -> x2 x3 Nil() 3: main_2(x6) x4 -> x4 x6 Nil() 4: walk_xs() x3 -> x3 5: walk_xs_3(x3) x5 -> Cons(x3, x5) 6: walk_1(x2) Nil() -> walk_xs() 7: walk_1(x2) Cons(x6, x8) -> x2 (walk(x2) x8) walk_xs_3(x6) 8: walk(x2) Nil() -> walk_xs() 9: walk(x2) Cons(x6, x8) -> x2 (walk(x2) x8) walk_xs_3(x6) 10: main_1(x6) x15 -> walk(x15) x6 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(x6) -> walk(comp()) x6 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 reverse :: ('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) -> 'l list main_3 :: '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() | Cons(X{*},X{*}) | Nil() | Cons(X{*},X{*}) | Nil() | Cons(X{*},X{*}) | Nil() | Nil() ,V{x1_11} -> V{x1_12} ,V{x1_12} -> V{x1_13} ,V{x1_13} -> R{9} | R{8} ,V{x2_8} -> V{x2_9} | comp() ,V{x2_9} -> V{x2_9} | comp() ,V{x2_11} -> V{x2_12} ,V{x2_12} -> walk_xs_3(V{x6_9}) ,V{x3_4} -> R{5} | Nil() ,V{x3_5} -> V{x6_9} ,V{x3_11} -> R{5} | Nil() ,V{x5_5} -> V{x3_11} ,V{x6_9} -> X{*} ,V{x6_14} -> X{*} ,V{x8_9} -> X{*} ,R{0} -> R{14} | main(X{*}) ,R{4} -> V{x3_4} ,R{5} -> Cons(V{x3_5},V{x5_5}) ,R{8} -> walk_xs() ,R{9} -> R{12} | @(R{13},walk_xs_3(V{x6_9})) | @(@(V{x2_9},R{9}),walk_xs_3(V{x6_9})) | @(@(V{x2_9},R{8}),walk_xs_3(V{x6_9})) | @(@(V{x2_9},@(walk(V{x2_9}),V{x8_9})),walk_xs_3(V{x6_9})) ,R{11} -> R{11} | R{4} | @(V{x1_11},R{5}) | @(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{4} | @(R{9},Nil()) | @(R{8},Nil()) | @(@(walk(comp()),V{x6_14}),Nil())} * Step 10: UncurryATRS WORST_CASE(?,O(n^1)) + Considered Problem: 4: walk_xs() x3 -> x3 5: walk_xs_3(x3) x5 -> Cons(x3, x5) 8: walk(comp()) Nil() -> walk_xs() 9: 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(x3) -> x3 2: walk_xs_3#1(x3, x5) -> Cons(x3, x5) 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(x3) -> x3 2: walk_xs_3#1(x3, x5) -> Cons(x3, x5) 3: walk#1(comp(), Nil()) -> walk_xs() 4: walk#2(comp(), Nil(), x6) -> x6 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(x3, x5) -> Cons(x3, x5) 3: walk#1(comp(), Nil()) -> walk_xs() 4: walk#2(comp(), Nil(), x6) -> x6 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(x3, x5) -> Cons(x3, x5) 2: walk#1(comp(), Nil()) -> walk_xs() 3: walk#2(comp(), Nil(), x6) -> x6 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(x3, x5) -> Cons(x3, x5) 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(x3, x5) -> Cons(x3, x5) 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(x3, x5) -> Cons(x3, x5) 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(x3, x5) -> Cons(x3, x5) 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(x3,x5) -> Cons(x3,x5) - 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 = 5, 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))