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 ;; type 'a closure = Lam1 of 'a closure * 'a closure | Lam2 | Lam3 of 'a ;; let rec apply c a = match c with | Lam1(f,g) -> apply f (apply g a) | Lam2 -> a | Lam3(x) -> Cons(x,a) ;; let comp f g = Lam1(f,g) ;; let rev2 l = let rec walk xyz = match xyz with | Nil()-> Lam2 | Cons(x,xs) -> comp (walk xs) Lam3(x) in apply (walk l) Nil ;; let main = rev2 (Cons(S(0),Cons(S(S(0)),Cons(S(S(S(0))),Nil)))) ;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization WORST_CASE(?,O(n^1)) + Considered Problem: (λapply : nat closure -> nat list -> nat list. (λcomp : nat closure -> nat closure -> nat closure. (λrev2 : nat list -> nat list. (λmain : nat list. main) (rev2 Cons(S(0),Cons(S(S(0)),Cons(S(S(S(0))),Nil))))) (λl : nat list. (λwalk : nat list -> nat closure. apply (walk l) Nil) (μwalk : nat list -> nat closure. λxyz : nat list. case xyz of | Nil -> Lam2 | Cons -> λx : nat. λxs : nat list. comp (walk xs) Lam3(x)))) (λf : nat closure. λg : nat closure. Lam1(f,g))) (μapply : nat closure -> nat list -> nat list. λc : nat closure. λa : nat list. case c of | Lam1 -> λf : nat closure. λg : nat closure. apply f (apply g a) | Lam2 -> a | Lam3 -> λx : nat. Cons(x,a)) : nat list where 0 :: nat Cons :: 'a -> 'a list -> 'a list False :: bool Lam1 :: 'a closure -> 'a closure -> 'a closure Lam2 :: 'a closure Lam3 :: 'a -> 'a closure 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() x3 -> x3 2: main_2() x2 -> main_3() (x2 Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))) 3: rev2_l(x0, x2) x3 -> x0 (x3 x2) Nil() 4: cond_walk_xyz(Nil(), x1) -> Lam2() 5: cond_walk_xyz(Cons(x4, x5), x1) -> x1 (walk(x1) x5) Lam3(x4) 6: walk_1(x1) x3 -> cond_walk_xyz(x3, x1) 7: walk(x1) x2 -> walk_1(x1) x2 8: rev2(x0, x1) x2 -> rev2_l(x0, x2) walk(x1) 9: main_1(x0) x1 -> main_2() rev2(x0, x1) 10: comp_f(x1) x2 -> Lam1(x1, x2) 11: comp() x1 -> comp_f(x1) 12: main() x0 -> main_1(x0) comp() 13: cond_apply_c_a(Lam1(x2, x3), x1) -> apply() x2 (apply() x3 x1) 14: cond_apply_c_a(Lam2(), x1) -> x1 15: cond_apply_c_a(Lam3(x2), x1) -> Cons(x2, x1) 16: apply_c(x0) x1 -> cond_apply_c_a(x0, x1) 17: apply_1() x0 -> apply_c(x0) 18: apply() x0 -> apply_1() x0 19: main() -> main() apply() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Lam1 :: 'a closure -> 'a closure -> 'a closure Lam2 :: 'a closure Lam3 :: 'a -> 'a closure Nil :: 'a list S :: nat -> nat apply_c :: nat closure -> nat list -> nat list comp :: nat closure -> nat closure -> nat closure comp_f :: nat closure -> nat closure -> nat closure rev2_l :: (nat closure -> nat list -> nat list) -> nat list -> (nat list -> nat closure) -> nat list main :: (nat closure -> nat list -> nat list) -> nat list rev2 :: (nat closure -> nat list -> nat list) -> (nat closure -> nat closure -> nat closure) -> nat list -> nat list apply_1 :: nat closure -> nat list -> nat list main_1 :: (nat closure -> nat list -> nat list) -> (nat closure -> nat closure -> nat closure) -> nat list walk_1 :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure main_2 :: (nat list -> nat list) -> nat list main_3 :: nat list -> nat list cond_apply_c_a :: nat closure -> nat list -> nat list cond_walk_xyz :: nat list -> (nat closure -> nat closure -> nat closure) -> nat closure apply :: nat closure -> nat list -> nat list walk :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure main :: nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3() x3 -> x3 2: main_2() x5 -> x5 Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) 3: rev2_l(x0, x2) x3 -> x0 (x3 x2) Nil() 4: cond_walk_xyz(Nil(), x1) -> Lam2() 5: cond_walk_xyz(Cons(x4, x5), x1) -> x1 (walk(x1) x5) Lam3(x4) 6: walk_1(x1) x3 -> cond_walk_xyz(x3, x1) 7: walk(x2) x6 -> cond_walk_xyz(x6, x2) 8: rev2(x0, x3) x4 -> x0 (walk(x3) x4) Nil() 9: main_1(x1) x3 -> main_3() (rev2(x1, x3) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))) 10: comp_f(x1) x2 -> Lam1(x1, x2) 11: comp() x1 -> comp_f(x1) 12: main() x0 -> main_2() rev2(x0, comp()) 13: cond_apply_c_a(Lam1(x2, x3), x1) -> apply() x2 (apply() x3 x1) 14: cond_apply_c_a(Lam2(), x1) -> x1 15: cond_apply_c_a(Lam3(x2), x1) -> Cons(x2, x1) 16: apply_c(x0) x1 -> cond_apply_c_a(x0, x1) 17: apply_1() x0 -> apply_c(x0) 18: apply() x0 -> apply_c(x0) 19: main() -> main_1(apply()) comp() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Lam1 :: 'a closure -> 'a closure -> 'a closure Lam2 :: 'a closure Lam3 :: 'a -> 'a closure Nil :: 'a list S :: nat -> nat apply_c :: nat closure -> nat list -> nat list comp :: nat closure -> nat closure -> nat closure comp_f :: nat closure -> nat closure -> nat closure rev2_l :: (nat closure -> nat list -> nat list) -> nat list -> (nat list -> nat closure) -> nat list main :: (nat closure -> nat list -> nat list) -> nat list rev2 :: (nat closure -> nat list -> nat list) -> (nat closure -> nat closure -> nat closure) -> nat list -> nat list apply_1 :: nat closure -> nat list -> nat list main_1 :: (nat closure -> nat list -> nat list) -> (nat closure -> nat closure -> nat closure) -> nat list walk_1 :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure main_2 :: (nat list -> nat list) -> nat list main_3 :: nat list -> nat list cond_apply_c_a :: nat closure -> nat list -> nat list cond_walk_xyz :: nat list -> (nat closure -> nat closure -> nat closure) -> nat closure apply :: nat closure -> nat list -> nat list walk :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure main :: nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 5: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3() x3 -> x3 2: main_2() x5 -> x5 Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) 3: rev2_l(x0, x2) x3 -> x0 (x3 x2) Nil() 4: cond_walk_xyz(Nil(), x1) -> Lam2() 5: cond_walk_xyz(Cons(x4, x5), x1) -> x1 (walk(x1) x5) Lam3(x4) 6: walk_1(x1) x3 -> cond_walk_xyz(x3, x1) 7: walk(x2) x6 -> cond_walk_xyz(x6, x2) 8: rev2(x0, x3) x4 -> x0 (walk(x3) x4) Nil() 9: main_1(x3) x7 -> rev2(x3, x7) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) 10: comp_f(x1) x2 -> Lam1(x1, x2) 11: comp() x1 -> comp_f(x1) 12: main() x1 -> rev2(x1, comp()) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) 13: cond_apply_c_a(Lam1(x2, x3), x1) -> apply() x2 (apply() x3 x1) 14: cond_apply_c_a(Lam2(), x1) -> x1 15: cond_apply_c_a(Lam3(x2), x1) -> Cons(x2, x1) 16: apply_c(x0) x1 -> cond_apply_c_a(x0, x1) 17: apply_1() x0 -> apply_c(x0) 18: apply() x0 -> apply_c(x0) 19: main() -> main_3() (rev2(apply(), comp()) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Lam1 :: 'a closure -> 'a closure -> 'a closure Lam2 :: 'a closure Lam3 :: 'a -> 'a closure Nil :: 'a list S :: nat -> nat apply_c :: nat closure -> nat list -> nat list comp :: nat closure -> nat closure -> nat closure comp_f :: nat closure -> nat closure -> nat closure rev2_l :: (nat closure -> nat list -> nat list) -> nat list -> (nat list -> nat closure) -> nat list main :: (nat closure -> nat list -> nat list) -> nat list rev2 :: (nat closure -> nat list -> nat list) -> (nat closure -> nat closure -> nat closure) -> nat list -> nat list apply_1 :: nat closure -> nat list -> nat list main_1 :: (nat closure -> nat list -> nat list) -> (nat closure -> nat closure -> nat closure) -> nat list walk_1 :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure main_2 :: (nat list -> nat list) -> nat list main_3 :: nat list -> nat list cond_apply_c_a :: nat closure -> nat list -> nat list cond_walk_xyz :: nat list -> (nat closure -> nat closure -> nat closure) -> nat closure apply :: nat closure -> nat list -> nat list walk :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure main :: nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 6: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3() x3 -> x3 2: main_2() x5 -> x5 Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) 3: rev2_l(x0, x2) x3 -> x0 (x3 x2) Nil() 4: cond_walk_xyz(Nil(), x1) -> Lam2() 5: cond_walk_xyz(Cons(x4, x5), x1) -> x1 (walk(x1) x5) Lam3(x4) 6: walk_1(x1) x3 -> cond_walk_xyz(x3, x1) 7: walk(x2) x6 -> cond_walk_xyz(x6, x2) 8: rev2(x0, x3) x4 -> x0 (walk(x3) x4) Nil() 9: main_1(x0) x6 -> x0 (walk(x6) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))) Nil() 10: comp_f(x1) x2 -> Lam1(x1, x2) 11: comp() x1 -> comp_f(x1) 12: main() x0 -> x0 (walk(comp()) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))) Nil() 13: cond_apply_c_a(Lam1(x2, x3), x1) -> apply() x2 (apply() x3 x1) 14: cond_apply_c_a(Lam2(), x1) -> x1 15: cond_apply_c_a(Lam3(x2), x1) -> Cons(x2, x1) 16: apply_c(x0) x1 -> cond_apply_c_a(x0, x1) 17: apply_1() x0 -> apply_c(x0) 18: apply() x0 -> apply_c(x0) 19: main() -> rev2(apply(), comp()) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Lam1 :: 'a closure -> 'a closure -> 'a closure Lam2 :: 'a closure Lam3 :: 'a -> 'a closure Nil :: 'a list S :: nat -> nat apply_c :: nat closure -> nat list -> nat list comp :: nat closure -> nat closure -> nat closure comp_f :: nat closure -> nat closure -> nat closure rev2_l :: (nat closure -> nat list -> nat list) -> nat list -> (nat list -> nat closure) -> nat list main :: (nat closure -> nat list -> nat list) -> nat list rev2 :: (nat closure -> nat list -> nat list) -> (nat closure -> nat closure -> nat closure) -> nat list -> nat list apply_1 :: nat closure -> nat list -> nat list main_1 :: (nat closure -> nat list -> nat list) -> (nat closure -> nat closure -> nat closure) -> nat list walk_1 :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure main_2 :: (nat list -> nat list) -> nat list main_3 :: nat list -> nat list cond_apply_c_a :: nat closure -> nat list -> nat list cond_walk_xyz :: nat list -> (nat closure -> nat closure -> nat closure) -> nat closure apply :: nat closure -> nat list -> nat list walk :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure main :: nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 7: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3() x3 -> x3 2: main_2() x5 -> x5 Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) 3: rev2_l(x0, x2) x3 -> x0 (x3 x2) Nil() 4: cond_walk_xyz(Nil(), x1) -> Lam2() 5: cond_walk_xyz(Cons(x4, x5), x1) -> x1 (walk(x1) x5) Lam3(x4) 6: walk_1(x1) x3 -> cond_walk_xyz(x3, x1) 7: walk(x2) x6 -> cond_walk_xyz(x6, x2) 8: rev2(x0, x3) x4 -> x0 (walk(x3) x4) Nil() 9: main_1(x0) x6 -> x0 (walk(x6) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))) Nil() 10: comp_f(x1) x2 -> Lam1(x1, x2) 11: comp() x1 -> comp_f(x1) 12: main() x0 -> x0 (walk(comp()) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))) Nil() 13: cond_apply_c_a(Lam1(x2, x3), x1) -> apply() x2 (apply() x3 x1) 14: cond_apply_c_a(Lam2(), x1) -> x1 15: cond_apply_c_a(Lam3(x2), x1) -> Cons(x2, x1) 16: apply_c(x0) x1 -> cond_apply_c_a(x0, x1) 17: apply_1() x0 -> apply_c(x0) 18: apply() x0 -> apply_c(x0) 19: main() -> apply() (walk(comp()) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))) Nil() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Lam1 :: 'a closure -> 'a closure -> 'a closure Lam2 :: 'a closure Lam3 :: 'a -> 'a closure Nil :: 'a list S :: nat -> nat apply_c :: nat closure -> nat list -> nat list comp :: nat closure -> nat closure -> nat closure comp_f :: nat closure -> nat closure -> nat closure rev2_l :: (nat closure -> nat list -> nat list) -> nat list -> (nat list -> nat closure) -> nat list main :: (nat closure -> nat list -> nat list) -> nat list rev2 :: (nat closure -> nat list -> nat list) -> (nat closure -> nat closure -> nat closure) -> nat list -> nat list apply_1 :: nat closure -> nat list -> nat list main_1 :: (nat closure -> nat list -> nat list) -> (nat closure -> nat closure -> nat closure) -> nat list walk_1 :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure main_2 :: (nat list -> nat list) -> nat list main_3 :: nat list -> nat list cond_apply_c_a :: nat closure -> nat list -> nat list cond_walk_xyz :: nat list -> (nat closure -> nat closure -> nat closure) -> nat closure apply :: nat closure -> nat list -> nat list walk :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure main :: nat list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 8: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3() x3 -> x3 2: main_2() x5 -> x5 Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) 3: rev2_l(x0, x2) x3 -> x0 (x3 x2) Nil() 4: cond_walk_xyz(Nil(), x1) -> Lam2() 5: cond_walk_xyz(Cons(x4, x5), x1) -> x1 (walk(x1) x5) Lam3(x4) 6: walk_1(x2) Nil() -> Lam2() 7: walk_1(x2) Cons(x8, x10) -> x2 (walk(x2) x10) Lam3(x8) 8: walk(x2) Nil() -> Lam2() 9: walk(x2) Cons(x8, x10) -> x2 (walk(x2) x10) Lam3(x8) 10: rev2(x0, x3) x4 -> x0 (walk(x3) x4) Nil() 11: main_1(x0) x6 -> x0 (walk(x6) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))) Nil() 12: comp_f(x1) x2 -> Lam1(x1, x2) 13: comp() x1 -> comp_f(x1) 14: main() x0 -> x0 (walk(comp()) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))) Nil() 15: cond_apply_c_a(Lam1(x2, x3), x1) -> apply() x2 (apply() x3 x1) 16: cond_apply_c_a(Lam2(), x1) -> x1 17: cond_apply_c_a(Lam3(x2), x1) -> Cons(x2, x1) 18: apply_c(Lam1(x4, x6)) x2 -> apply() x4 (apply() x6 x2) 19: apply_c(Lam2()) x2 -> x2 20: apply_c(Lam3(x4)) x2 -> Cons(x4, x2) 21: apply_1() x0 -> apply_c(x0) 22: apply() x0 -> apply_c(x0) 23: main() -> apply() (walk(comp()) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))) Nil() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Lam1 :: 'a closure -> 'a closure -> 'a closure Lam2 :: 'a closure Lam3 :: 'a -> 'a closure Nil :: 'a list S :: nat -> nat apply_c :: nat closure -> nat list -> nat list comp :: nat closure -> nat closure -> nat closure comp_f :: nat closure -> nat closure -> nat closure rev2_l :: (nat closure -> nat list -> nat list) -> nat list -> (nat list -> nat closure) -> nat list main :: (nat closure -> nat list -> nat list) -> nat list rev2 :: (nat closure -> nat list -> nat list) -> (nat closure -> nat closure -> nat closure) -> nat list -> nat list apply_1 :: nat closure -> nat list -> nat list main_1 :: (nat closure -> nat list -> nat list) -> (nat closure -> nat closure -> nat closure) -> nat list walk_1 :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure main_2 :: (nat list -> nat list) -> nat list main_3 :: nat list -> nat list cond_apply_c_a :: nat closure -> nat list -> nat list cond_walk_xyz :: nat list -> (nat closure -> nat closure -> nat closure) -> nat closure apply :: nat closure -> nat list -> nat list walk :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure main :: nat list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 9: NeededRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3() x3 -> x3 2: main_2() x5 -> x5 Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) 3: rev2_l(x0, x2) x3 -> x0 (x3 x2) Nil() 6: walk_1(x2) Nil() -> Lam2() 7: walk_1(x2) Cons(x8, x10) -> x2 (walk(x2) x10) Lam3(x8) 8: walk(x2) Nil() -> Lam2() 9: walk(x2) Cons(x8, x10) -> x2 (walk(x2) x10) Lam3(x8) 10: rev2(x0, x3) x4 -> x0 (walk(x3) x4) Nil() 11: main_1(x0) x6 -> x0 (walk(x6) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))) Nil() 12: comp_f(x1) x2 -> Lam1(x1, x2) 13: comp() x1 -> comp_f(x1) 14: main() x0 -> x0 (walk(comp()) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))) Nil() 18: apply_c(Lam1(x4, x6)) x2 -> apply() x4 (apply() x6 x2) 19: apply_c(Lam2()) x2 -> x2 20: apply_c(Lam3(x4)) x2 -> Cons(x4, x2) 21: apply_1() x0 -> apply_c(x0) 22: apply() x0 -> apply_c(x0) 23: main() -> apply() (walk(comp()) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))) Nil() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Lam1 :: 'a closure -> 'a closure -> 'a closure Lam2 :: 'a closure Lam3 :: 'a -> 'a closure Nil :: 'a list S :: nat -> nat apply_c :: nat closure -> nat list -> nat list comp :: nat closure -> nat closure -> nat closure comp_f :: nat closure -> nat closure -> nat closure rev2_l :: (nat closure -> nat list -> nat list) -> nat list -> (nat list -> nat closure) -> nat list main :: (nat closure -> nat list -> nat list) -> nat list rev2 :: (nat closure -> nat list -> nat list) -> (nat closure -> nat closure -> nat closure) -> nat list -> nat list apply_1 :: nat closure -> nat list -> nat list main_1 :: (nat closure -> nat list -> nat list) -> (nat closure -> nat closure -> nat closure) -> nat list walk_1 :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure main_2 :: (nat list -> nat list) -> nat list main_3 :: nat list -> nat list apply :: nat closure -> nat list -> nat list walk :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure main :: nat list + Applied Processor: NeededRules + Details: none * Step 10: CFA WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3() x3 -> x3 2: main_2() x5 -> x5 Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) 3: rev2_l(x0, x2) x3 -> x0 (x3 x2) Nil() 4: walk_1(x2) Nil() -> Lam2() 5: walk_1(x2) Cons(x8, x10) -> x2 (walk(x2) x10) Lam3(x8) 6: walk(x2) Nil() -> Lam2() 7: walk(x2) Cons(x8, x10) -> x2 (walk(x2) x10) Lam3(x8) 8: rev2(x0, x3) x4 -> x0 (walk(x3) x4) Nil() 9: main_1(x0) x6 -> x0 (walk(x6) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))) Nil() 10: comp_f(x1) x2 -> Lam1(x1, x2) 11: comp() x1 -> comp_f(x1) 12: main() x0 -> x0 (walk(comp()) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))) Nil() 13: apply_c(Lam1(x4, x6)) x2 -> apply() x4 (apply() x6 x2) 14: apply_c(Lam2()) x2 -> x2 15: apply_c(Lam3(x4)) x2 -> Cons(x4, x2) 16: apply_1() x0 -> apply_c(x0) 17: apply() x0 -> apply_c(x0) 18: main() -> apply() (walk(comp()) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))) Nil() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Lam1 :: 'a closure -> 'a closure -> 'a closure Lam2 :: 'a closure Lam3 :: 'a -> 'a closure Nil :: 'a list S :: nat -> nat apply_c :: nat closure -> nat list -> nat list comp :: nat closure -> nat closure -> nat closure comp_f :: nat closure -> nat closure -> nat closure rev2_l :: (nat closure -> nat list -> nat list) -> nat list -> (nat list -> nat closure) -> nat list main :: (nat closure -> nat list -> nat list) -> nat list rev2 :: (nat closure -> nat list -> nat list) -> (nat closure -> nat closure -> nat closure) -> nat list -> nat list apply_1 :: nat closure -> nat list -> nat list main_1 :: (nat closure -> nat list -> nat list) -> (nat closure -> nat closure -> nat closure) -> nat list walk_1 :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure main_2 :: (nat list -> nat list) -> nat list main_3 :: nat list -> nat list apply :: nat closure -> nat list -> nat list walk :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure main :: nat list + Applied Processor: CFA {cfaRefinement = } + Details: {X{*} -> Nil() | Nil() | 0() | S(X{*}) | S(X{*}) | S(X{*}) | Cons(X{*},X{*}) | 0() | S(X{*}) | S(X{*}) | Cons(X{*},X{*}) | 0() | S(X{*}) | Cons(X{*},X{*}) | Cons(X{*},X{*}) | Lam3(X{*}) | Lam2() | Lam1(X{*},X{*}) | Nil() | Nil() | 0() | S(X{*}) | S(X{*}) | S(X{*}) | Cons(X{*},X{*}) | 0() | S(X{*}) | S(X{*}) | Cons(X{*},X{*}) | 0() | S(X{*}) | Cons(X{*},X{*}) | Lam1(X{*},X{*}) | Nil() | Nil() | 0() | S(X{*}) | S(X{*}) | S(X{*}) | Cons(X{*},X{*}) | 0() | S(X{*}) | S(X{*}) | Cons(X{*},X{*}) | 0() | S(X{*}) | Cons(X{*},X{*}) | Nil() | Lam3(X{*}) | Cons(X{*},X{*}) | Lam2() | Nil() | Lam3(X{*}) | Cons(X{*},X{*}) | Lam2() | Nil() | Nil() | Nil() | 0() | S(X{*}) | S(X{*}) | S(X{*}) | Cons(X{*},X{*}) | 0() | S(X{*}) | S(X{*}) | Cons(X{*},X{*}) | 0() | S(X{*}) | Cons(X{*},X{*}) ,V{x0_17} -> V{x6_13} | V{x4_13} | R{7} ,V{x1_10} -> V{x1_11} ,V{x1_11} -> R{7} | R{6} ,V{x2_6} -> V{x2_7} ,V{x2_7} -> V{x2_7} | comp() ,V{x2_10} -> Lam3(V{x8_7}) ,V{x2_13} -> R{13} | R{15} | R{14} | V{x2_13} | Nil() ,V{x2_14} -> R{13} | R{15} | R{14} | V{x2_13} | Nil() ,V{x2_15} -> R{13} | R{15} | R{14} | V{x2_13} | Nil() ,V{x4_13} -> V{x1_10} ,V{x4_15} -> V{x8_7} ,V{x6_13} -> V{x2_10} ,V{x8_7} -> S(S(S(0()))) | S(S(0())) | S(0()) ,V{x10_7} -> Nil() | Cons(S(S(S(0()))),Nil()) | Cons(S(S(0())),Cons(S(S(S(0()))),Nil())) ,R{0} -> R{18} | main() ,R{6} -> Lam2() ,R{7} -> R{10} | @(R{11},Lam3(V{x8_7})) | @(@(V{x2_7},R{6}),Lam3(V{x8_7})) | @(@(V{x2_7},R{7}),Lam3(V{x8_7})) | @(@(V{x2_7},@(walk(V{x2_7}),V{x10_7})),Lam3(V{x8_7})) ,R{10} -> Lam1(V{x1_10},V{x2_10}) ,R{11} -> comp_f(V{x1_11}) ,R{13} -> R{15} | R{14} | R{13} | @(R{17},R{13}) | @(R{17},R{14}) | @(R{17},R{15}) | @(@(apply(),V{x4_13}),R{15}) | @(@(apply(),V{x4_13}),R{14}) | @(@(apply(),V{x4_13}),R{13}) | @(R{17},@(R{17},V{x2_13})) | @(@(apply(),V{x4_13}),@(R{17},V{x2_13})) | @(R{17},@(@(apply(),V{x6_13}),V{x2_13})) | @(@(apply(),V{x4_13}),@(@(apply(),V{x6_13}),V{x2_13})) ,R{14} -> V{x2_14} ,R{15} -> Cons(V{x4_15},V{x2_15}) ,R{17} -> apply_c(V{x0_17}) ,R{18} -> R{15} | R{14} | R{13} | @(R{17},Nil()) | @(@(apply(),R{7}),Nil()) | @(@(apply(),@(walk(comp()),Cons(S(0()),Cons(S(S(0())),Cons(S(S(S(0()))),Nil()))))),Nil())} * Step 11: UncurryATRS WORST_CASE(?,O(n^1)) + Considered Problem: 6: walk(comp()) Nil() -> Lam2() 7: walk(comp()) Cons(x2, x1) -> comp() (walk(comp()) x1) Lam3(x2) 10: comp_f(x2) Lam3(x1) -> Lam1(x2, Lam3(x1)) 11: comp() x1 -> comp_f(x1) 13: apply_c(Lam1(x3, Lam3(x2))) x1 -> apply() x3 (apply() Lam3(x2) x1) 14: apply_c(Lam2()) x2 -> x2 15: apply_c(Lam3(x4)) x2 -> Cons(x4, x2) 17: apply() x0 -> apply_c(x0) 18: main() -> apply() (walk(comp()) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))) Nil() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Lam1 :: 'a closure -> 'a closure -> 'a closure Lam2 :: 'a closure Lam3 :: 'a -> 'a closure Nil :: 'a list S :: nat -> nat apply_c :: nat closure -> nat list -> nat list comp :: nat closure -> nat closure -> nat closure comp_f :: nat closure -> nat closure -> nat closure apply :: nat closure -> nat list -> nat list walk :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure main :: nat list + Applied Processor: UncurryATRS + Details: none * Step 12: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk#1(comp(), Nil()) -> Lam2() 2: walk#1(comp(), Cons(x2, x1)) -> comp#2(walk#1(comp(), x1), Lam3(x2)) 3: comp_f#1(x2, Lam3(x1)) -> Lam1(x2, Lam3(x1)) 4: comp#1(x1) -> comp_f(x1) 5: comp#2(x1, x2) -> comp_f#1(x1, x2) 6: apply_c#1(Lam1(x3, Lam3(x2)), x1) -> apply#2(x3, apply#2(Lam3(x2), x1)) 7: apply_c#1(Lam2(), x2) -> x2 8: apply_c#1(Lam3(x4), x2) -> Cons(x4, x2) 9: apply#1(x0) -> apply_c(x0) 10: apply#2(x0, x1) -> apply_c#1(x0, x1) 11: main() -> apply#2(walk#1(comp(), Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))), Nil()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Lam1 :: 'a closure -> 'a closure -> 'a closure Lam2 :: 'a closure Lam3 :: 'a -> 'a closure Nil :: 'a list S :: nat -> nat apply#1 :: nat closure -> nat list -> nat list apply#2 :: nat closure -> nat list -> nat list apply_c :: nat closure -> nat list -> nat list apply_c#1 :: nat closure -> nat list -> nat list comp :: nat closure -> nat closure -> nat closure comp#1 :: nat closure -> nat closure -> nat closure comp#2 :: nat closure -> nat closure -> nat closure comp_f :: nat closure -> nat closure -> nat closure comp_f#1 :: nat closure -> nat closure -> nat closure main :: nat list walk#1 :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 13: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk#1(comp(), Nil()) -> Lam2() 2: walk#1(comp(), Cons(x2, x1)) -> comp#2(walk#1(comp(), x1), Lam3(x2)) 3: comp_f#1(x2, Lam3(x1)) -> Lam1(x2, Lam3(x1)) 5: comp#2(x1, x2) -> comp_f#1(x1, x2) 6: apply_c#1(Lam1(x3, Lam3(x2)), x1) -> apply#2(x3, apply#2(Lam3(x2), x1)) 7: apply_c#1(Lam2(), x2) -> x2 8: apply_c#1(Lam3(x4), x2) -> Cons(x4, x2) 10: apply#2(x0, x1) -> apply_c#1(x0, x1) 11: main() -> apply#2(walk#1(comp(), Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))), Nil()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Lam1 :: 'a closure -> 'a closure -> 'a closure Lam2 :: 'a closure Lam3 :: 'a -> 'a closure Nil :: 'a list S :: nat -> nat apply#2 :: nat closure -> nat list -> nat list apply_c#1 :: nat closure -> nat list -> nat list comp :: nat closure -> nat closure -> nat closure comp#2 :: nat closure -> nat closure -> nat closure comp_f#1 :: nat closure -> nat closure -> nat closure main :: nat list walk#1 :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 14: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk#1(comp(), Nil()) -> Lam2() 2: walk#1(comp(), Cons(x5, x3)) -> comp_f#1(walk#1(comp(), x3), Lam3(x5)) 3: comp_f#1(x2, Lam3(x1)) -> Lam1(x2, Lam3(x1)) 4: comp#2(x4, Lam3(x2)) -> Lam1(x4, Lam3(x2)) 5: apply_c#1(Lam1(x3, Lam3(x2)), x1) -> apply#2(x3, apply#2(Lam3(x2), x1)) 6: apply_c#1(Lam2(), x2) -> x2 7: apply_c#1(Lam3(x4), x2) -> Cons(x4, x2) 8: apply#2(Lam1(x6, Lam3(x4)), x2) -> apply#2(x6, apply#2(Lam3(x4), x2)) 9: apply#2(Lam2(), x4) -> x4 10: apply#2(Lam3(x8), x4) -> Cons(x8, x4) 11: main() -> apply#2(walk#1(comp(), Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))), Nil()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Lam1 :: 'a closure -> 'a closure -> 'a closure Lam2 :: 'a closure Lam3 :: 'a -> 'a closure Nil :: 'a list S :: nat -> nat apply#2 :: nat closure -> nat list -> nat list apply_c#1 :: nat closure -> nat list -> nat list comp :: nat closure -> nat closure -> nat closure comp#2 :: nat closure -> nat closure -> nat closure comp_f#1 :: nat closure -> nat closure -> nat closure main :: nat list walk#1 :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 15: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk#1(comp(), Nil()) -> Lam2() 2: walk#1(comp(), Cons(x5, x3)) -> comp_f#1(walk#1(comp(), x3), Lam3(x5)) 3: comp_f#1(x2, Lam3(x1)) -> Lam1(x2, Lam3(x1)) 8: apply#2(Lam1(x6, Lam3(x4)), x2) -> apply#2(x6, apply#2(Lam3(x4), x2)) 9: apply#2(Lam2(), x4) -> x4 10: apply#2(Lam3(x8), x4) -> Cons(x8, x4) 11: main() -> apply#2(walk#1(comp(), Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))), Nil()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Lam1 :: 'a closure -> 'a closure -> 'a closure Lam2 :: 'a closure Lam3 :: 'a -> 'a closure Nil :: 'a list S :: nat -> nat apply#2 :: nat closure -> nat list -> nat list comp :: nat closure -> nat closure -> nat closure comp_f#1 :: nat closure -> nat closure -> nat closure main :: nat list walk#1 :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 16: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk#1(comp(), Nil()) -> Lam2() 2: walk#1(comp(), Cons(x2, x7)) -> Lam1(walk#1(comp(), x7), Lam3(x2)) 3: comp_f#1(x2, Lam3(x1)) -> Lam1(x2, Lam3(x1)) 4: apply#2(Lam1(x13, Lam3(x16)), x8) -> apply#2(x13, Cons(x16, x8)) 5: apply#2(Lam2(), x4) -> x4 6: apply#2(Lam3(x8), x4) -> Cons(x8, x4) 7: main() -> apply#2(walk#1(comp(), Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))), Nil()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Lam1 :: 'a closure -> 'a closure -> 'a closure Lam2 :: 'a closure Lam3 :: 'a -> 'a closure Nil :: 'a list S :: nat -> nat apply#2 :: nat closure -> nat list -> nat list comp :: nat closure -> nat closure -> nat closure comp_f#1 :: nat closure -> nat closure -> nat closure main :: nat list walk#1 :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 17: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk#1(comp(), Nil()) -> Lam2() 2: walk#1(comp(), Cons(x2, x7)) -> Lam1(walk#1(comp(), x7), Lam3(x2)) 4: apply#2(Lam1(x13, Lam3(x16)), x8) -> apply#2(x13, Cons(x16, x8)) 5: apply#2(Lam2(), x4) -> x4 6: apply#2(Lam3(x8), x4) -> Cons(x8, x4) 7: main() -> apply#2(walk#1(comp(), Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))), Nil()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Lam1 :: 'a closure -> 'a closure -> 'a closure Lam2 :: 'a closure Lam3 :: 'a -> 'a closure Nil :: 'a list S :: nat -> nat apply#2 :: nat closure -> nat list -> nat list comp :: nat closure -> nat closure -> nat closure main :: nat list walk#1 :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 18: Compression WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk#1(comp(), Nil()) -> Lam2() 2: walk#1(comp(), Cons(x2, x7)) -> Lam1(walk#1(comp(), x7), Lam3(x2)) 3: apply#2(Lam1(x13, Lam3(x16)), x8) -> apply#2(x13, Cons(x16, x8)) 4: apply#2(Lam2(), x4) -> x4 6: main() -> apply#2(walk#1(comp(), Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))), Nil()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Lam1 :: 'a closure -> 'a closure -> 'a closure Lam2 :: 'a closure Lam3 :: 'a -> 'a closure Nil :: 'a list S :: nat -> nat apply#2 :: nat closure -> nat list -> nat list comp :: nat closure -> nat closure -> nat closure main :: nat list walk#1 :: (nat closure -> nat closure -> nat closure) -> nat list -> nat closure + Applied Processor: Compression + Details: none * Step 19: ToTctProblem WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk#1(Nil()) -> Lam2() 2: walk#1(Cons(x2, x7)) -> Lam1(walk#1(x7), Lam3(x2)) 3: apply#2(Lam1(x13, Lam3(x16)), x8) -> apply#2(x13, Cons(x16, x8)) 4: apply#2(Lam2(), x4) -> x4 5: main() -> apply#2(walk#1(Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))), Nil()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Lam1 :: 'a closure -> 'a closure -> 'a closure Lam2 :: 'a closure Lam3 :: 'a -> 'a closure Nil :: 'a list S :: nat -> nat apply#2 :: nat closure -> nat list -> nat list main :: nat list walk#1 :: nat list -> nat closure + Applied Processor: ToTctProblem + Details: none * Step 20: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: apply#2(Lam1(x13,Lam3(x16)),x8) -> apply#2(x13,Cons(x16,x8)) apply#2(Lam2(),x4) -> x4 main() -> apply#2(walk#1(Cons(S(0()),Cons(S(S(0())),Cons(S(S(S(0()))),Nil())))),Nil()) walk#1(Cons(x2,x7)) -> Lam1(walk#1(x7),Lam3(x2)) walk#1(Nil()) -> Lam2() - Signature: {apply#2/2,main/0,walk#1/1} / {0/0,Cons/2,Lam1/2,Lam2/0,Lam3/1,Nil/0,S/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,Cons,Lam1,Lam2,Lam3,Nil,S} + Applied Processor: Ara {minDegree = 1, maxDegree = 2, araTimeout = 3, araRuleShifting = Nothing} + Details: Signatures used: ---------------- F (TrsFun "0") :: [] -(0)-> "A"(15) F (TrsFun "Cons") :: ["A"(0) x "A"(3)] -(3)-> "A"(3) F (TrsFun "Cons") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "Lam1") :: ["A"(1) x "A"(1)] -(0)-> "A"(1) F (TrsFun "Lam2") :: [] -(0)-> "A"(1) F (TrsFun "Lam2") :: [] -(0)-> "A"(7) F (TrsFun "Lam3") :: ["A"(0)] -(1)-> "A"(1) F (TrsFun "Nil") :: [] -(0)-> "A"(3) F (TrsFun "Nil") :: [] -(0)-> "A"(15) F (TrsFun "Nil") :: [] -(0)-> "A"(7) F (TrsFun "S") :: ["A"(0)] -(0)-> "A"(15) F (TrsFun "apply#2") :: ["A"(1) x "A"(0)] -(1)-> "A"(0) F (TrsFun "main") :: [] -(16)-> "A"(0) F (TrsFun "walk#1") :: ["A"(3)] -(4)-> "A"(1) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "F (TrsFun \"0\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"Cons\")_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "F (TrsFun \"Lam1\")_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1) "F (TrsFun \"Lam2\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"Lam3\")_A" :: ["A"(0)] -(1)-> "A"(1) "F (TrsFun \"Nil\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"S\")_A" :: ["A"(0)] -(0)-> "A"(1) WORST_CASE(?,O(n^1))