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 rev1 l = let rec walk xyz = match xyz with | Nil -> (fun ys -> ys) | Cons(x,xs) -> comp (walk xs) (fun ys -> Cons(x,ys)) in walk l Nil ;; 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 main = rev1 (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: (λcomp : (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list. (λrev1 : nat list -> nat list. (λmain : nat list. main) (rev1 Cons(S(0),Cons(S(S(0)),Cons(S(S(S(0))),Nil))))) (λl : nat list. (λwalk : nat list -> nat list -> nat list. walk l Nil) (μwalk : nat list -> nat list -> nat list. λxyz : nat list. case xyz of | Nil -> λys : nat list. ys | Cons -> λx : nat. λxs : nat list. comp (walk xs) (λys : nat list. Cons(x,ys))))) (λf : nat list -> nat list. λg : nat list -> nat list. λz : nat list. f (g z)) : 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_2() x2 -> x2 2: main_1() x1 -> main_2() (x1 Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))) 3: rev1_l(x1) x2 -> x2 x1 Nil() 4: walk_xyz() x3 -> x3 5: walk_xyz_3(x3) x5 -> Cons(x3, x5) 6: cond_walk_xyz(Nil(), x0) -> walk_xyz() 7: cond_walk_xyz(Cons(x3, x4), x0) -> x0 (walk(x0) x4) walk_xyz_3(x3) 8: walk_1(x0) x2 -> cond_walk_xyz(x2, x0) 9: walk(x0) x1 -> walk_1(x0) x1 10: rev1(x0) x1 -> rev1_l(x1) walk(x0) 11: main() x0 -> main_1() rev1(x0) 12: comp_f_g(x0, x1) x2 -> x0 (x1 x2) 13: comp_f(x0) x1 -> comp_f_g(x0, x1) 14: comp() x0 -> comp_f(x0) 15: main() -> main() comp() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f_g :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list rev1_l :: nat list -> (nat list -> nat list -> nat list) -> nat list main :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list rev1 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list walk_xyz :: nat list -> nat list main_1 :: (nat list -> nat list) -> nat list walk_1 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list main_2 :: nat list -> nat list walk_xyz_3 :: nat -> nat list -> nat list cond_walk_xyz :: nat list -> ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list walk :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list main :: nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_2() x2 -> x2 2: main_1() x3 -> x3 Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) 3: rev1_l(x1) x2 -> x2 x1 Nil() 4: walk_xyz() x3 -> x3 5: walk_xyz_3(x3) x5 -> Cons(x3, x5) 6: cond_walk_xyz(Nil(), x0) -> walk_xyz() 7: cond_walk_xyz(Cons(x3, x4), x0) -> x0 (walk(x0) x4) walk_xyz_3(x3) 8: walk_1(x0) x2 -> cond_walk_xyz(x2, x0) 9: walk(x0) x4 -> cond_walk_xyz(x4, x0) 10: rev1(x1) x2 -> walk(x1) x2 Nil() 11: main() x1 -> main_2() (rev1(x1) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil())))) 12: comp_f_g(x0, x1) x2 -> x0 (x1 x2) 13: comp_f(x0) x1 -> comp_f_g(x0, x1) 14: comp() x0 -> comp_f(x0) 15: main() -> main_1() rev1(comp()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f_g :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list rev1_l :: nat list -> (nat list -> nat list -> nat list) -> nat list main :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list rev1 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list walk_xyz :: nat list -> nat list main_1 :: (nat list -> nat list) -> nat list walk_1 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list main_2 :: nat list -> nat list walk_xyz_3 :: nat -> nat list -> nat list cond_walk_xyz :: nat list -> ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list walk :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list main :: nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 5: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_2() x2 -> x2 2: main_1() x3 -> x3 Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) 3: rev1_l(x1) x2 -> x2 x1 Nil() 4: walk_xyz() x3 -> x3 5: walk_xyz_3(x3) x5 -> Cons(x3, x5) 6: cond_walk_xyz(Nil(), x0) -> walk_xyz() 7: cond_walk_xyz(Cons(x3, x4), x0) -> x0 (walk(x0) x4) walk_xyz_3(x3) 8: walk_1(x0) x2 -> cond_walk_xyz(x2, x0) 9: walk(x0) x4 -> cond_walk_xyz(x4, x0) 10: rev1(x1) x2 -> walk(x1) x2 Nil() 11: main() x3 -> rev1(x3) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) 12: comp_f_g(x0, x1) x2 -> x0 (x1 x2) 13: comp_f(x0) x1 -> comp_f_g(x0, x1) 14: comp() x0 -> comp_f(x0) 15: main() -> rev1(comp()) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f_g :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list rev1_l :: nat list -> (nat list -> nat list -> nat list) -> nat list main :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list rev1 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list walk_xyz :: nat list -> nat list main_1 :: (nat list -> nat list) -> nat list walk_1 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list main_2 :: nat list -> nat list walk_xyz_3 :: nat -> nat list -> nat list cond_walk_xyz :: nat list -> ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list walk :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list main :: nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 6: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_2() x2 -> x2 2: main_1() x3 -> x3 Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) 3: rev1_l(x1) x2 -> x2 x1 Nil() 4: walk_xyz() x3 -> x3 5: walk_xyz_3(x3) x5 -> Cons(x3, x5) 6: cond_walk_xyz(Nil(), x0) -> walk_xyz() 7: cond_walk_xyz(Cons(x3, x4), x0) -> x0 (walk(x0) x4) walk_xyz_3(x3) 8: walk_1(x0) x2 -> cond_walk_xyz(x2, x0) 9: walk(x0) x4 -> cond_walk_xyz(x4, x0) 10: rev1(x1) x2 -> walk(x1) x2 Nil() 11: main() x2 -> walk(x2) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) Nil() 12: comp_f_g(x0, x1) x2 -> x0 (x1 x2) 13: comp_f(x0) x1 -> comp_f_g(x0, x1) 14: comp() x0 -> comp_f(x0) 15: main() -> 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 Nil :: 'a list S :: nat -> nat comp :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f_g :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list rev1_l :: nat list -> (nat list -> nat list -> nat list) -> nat list main :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list rev1 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list walk_xyz :: nat list -> nat list main_1 :: (nat list -> nat list) -> nat list walk_1 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list main_2 :: nat list -> nat list walk_xyz_3 :: nat -> nat list -> nat list cond_walk_xyz :: nat list -> ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list walk :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list main :: nat list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 7: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_2() x2 -> x2 2: main_1() x3 -> x3 Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) 3: rev1_l(x1) x2 -> x2 x1 Nil() 4: walk_xyz() x3 -> x3 5: walk_xyz_3(x3) x5 -> Cons(x3, x5) 6: cond_walk_xyz(Nil(), x0) -> walk_xyz() 7: cond_walk_xyz(Cons(x3, x4), x0) -> x0 (walk(x0) x4) walk_xyz_3(x3) 8: walk_1(x0) Nil() -> walk_xyz() 9: walk_1(x0) Cons(x6, x8) -> x0 (walk(x0) x8) walk_xyz_3(x6) 10: walk(x0) Nil() -> walk_xyz() 11: walk(x0) Cons(x6, x8) -> x0 (walk(x0) x8) walk_xyz_3(x6) 12: rev1(x1) x2 -> walk(x1) x2 Nil() 13: main() x2 -> walk(x2) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) Nil() 14: comp_f_g(x0, x1) x2 -> x0 (x1 x2) 15: comp_f(x0) x1 -> comp_f_g(x0, x1) 16: comp() x0 -> comp_f(x0) 17: main() -> 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 Nil :: 'a list S :: nat -> nat comp :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f_g :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list rev1_l :: nat list -> (nat list -> nat list -> nat list) -> nat list main :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list rev1 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list walk_xyz :: nat list -> nat list main_1 :: (nat list -> nat list) -> nat list walk_1 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list main_2 :: nat list -> nat list walk_xyz_3 :: nat -> nat list -> nat list cond_walk_xyz :: nat list -> ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list walk :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list main :: nat list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 8: NeededRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_2() x2 -> x2 2: main_1() x3 -> x3 Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) 3: rev1_l(x1) x2 -> x2 x1 Nil() 4: walk_xyz() x3 -> x3 5: walk_xyz_3(x3) x5 -> Cons(x3, x5) 8: walk_1(x0) Nil() -> walk_xyz() 9: walk_1(x0) Cons(x6, x8) -> x0 (walk(x0) x8) walk_xyz_3(x6) 10: walk(x0) Nil() -> walk_xyz() 11: walk(x0) Cons(x6, x8) -> x0 (walk(x0) x8) walk_xyz_3(x6) 12: rev1(x1) x2 -> walk(x1) x2 Nil() 13: main() x2 -> walk(x2) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) Nil() 14: comp_f_g(x0, x1) x2 -> x0 (x1 x2) 15: comp_f(x0) x1 -> comp_f_g(x0, x1) 16: comp() x0 -> comp_f(x0) 17: main() -> 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 Nil :: 'a list S :: nat -> nat comp :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f_g :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list rev1_l :: nat list -> (nat list -> nat list -> nat list) -> nat list main :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list rev1 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list walk_xyz :: nat list -> nat list main_1 :: (nat list -> nat list) -> nat list walk_1 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list main_2 :: nat list -> nat list walk_xyz_3 :: nat -> nat list -> nat list walk :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list main :: nat list + Applied Processor: NeededRules + Details: none * Step 9: CFA WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_2() x2 -> x2 2: main_1() x3 -> x3 Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) 3: rev1_l(x1) x2 -> x2 x1 Nil() 4: walk_xyz() x3 -> x3 5: walk_xyz_3(x3) x5 -> Cons(x3, x5) 6: walk_1(x0) Nil() -> walk_xyz() 7: walk_1(x0) Cons(x6, x8) -> x0 (walk(x0) x8) walk_xyz_3(x6) 8: walk(x0) Nil() -> walk_xyz() 9: walk(x0) Cons(x6, x8) -> x0 (walk(x0) x8) walk_xyz_3(x6) 10: rev1(x1) x2 -> walk(x1) x2 Nil() 11: main() x2 -> walk(x2) Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))) Nil() 12: comp_f_g(x0, x1) x2 -> x0 (x1 x2) 13: comp_f(x0) x1 -> comp_f_g(x0, x1) 14: comp() x0 -> comp_f(x0) 15: main() -> 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 Nil :: 'a list S :: nat -> nat comp :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f_g :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list rev1_l :: nat list -> (nat list -> nat list -> nat list) -> nat list main :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list rev1 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list walk_xyz :: nat list -> nat list main_1 :: (nat list -> nat list) -> nat list walk_1 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list main_2 :: nat list -> nat list walk_xyz_3 :: nat -> nat list -> nat list walk :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list 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{*}) | 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() | Cons(X{*},X{*}) | Nil() | Cons(X{*},X{*}) | Nil() | Cons(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{*}) ,V{x0_8} -> V{x0_9} ,V{x0_9} -> V{x0_9} | comp() ,V{x0_12} -> V{x0_13} ,V{x0_13} -> V{x0_14} ,V{x0_14} -> R{9} | R{8} ,V{x1_12} -> V{x1_13} ,V{x1_13} -> walk_xyz_3(V{x6_9}) ,V{x2_12} -> R{5} | Nil() ,V{x3_4} -> R{5} ,V{x3_5} -> V{x6_9} ,V{x5_5} -> V{x2_12} ,V{x6_9} -> S(S(S(0()))) | S(S(0())) | S(0()) ,V{x8_9} -> Nil() | Cons(S(S(S(0()))),Nil()) | Cons(S(S(0())),Cons(S(S(S(0()))),Nil())) ,R{0} -> R{15} | main() ,R{4} -> V{x3_4} ,R{5} -> Cons(V{x3_5},V{x5_5}) ,R{8} -> walk_xyz() ,R{9} -> R{13} | @(R{14},walk_xyz_3(V{x6_9})) | @(@(V{x0_9},R{8}),walk_xyz_3(V{x6_9})) | @(@(V{x0_9},R{9}),walk_xyz_3(V{x6_9})) | @(@(V{x0_9},@(walk(V{x0_9}),V{x8_9})),walk_xyz_3(V{x6_9})) ,R{12} -> R{12} | R{4} | @(V{x0_12},R{5}) | @(V{x0_12},@(V{x1_12},V{x2_12})) ,R{13} -> comp_f_g(V{x0_13},V{x1_13}) ,R{14} -> comp_f(V{x0_14}) ,R{15} -> R{12} | @(R{9},Nil()) | @(@(walk(comp()),Cons(S(0()),Cons(S(S(0())),Cons(S(S(S(0()))),Nil())))),Nil())} * Step 10: UncurryATRS WORST_CASE(?,O(n^1)) + Considered Problem: 4: walk_xyz() Cons(x1, x2) -> Cons(x1, x2) 5: walk_xyz_3(x3) x5 -> Cons(x3, x5) 8: walk(comp()) Nil() -> walk_xyz() 9: walk(comp()) Cons(x2, x1) -> comp() (walk(comp()) x1) walk_xyz_3(x2) 12: comp_f_g(comp_f_g(x3, x4), walk_xyz_3(x2)) x1 -> comp_f_g(x3, x4) (walk_xyz_3(x2) x1) 13: comp_f_g(walk_xyz(), walk_xyz_3(x2)) x1 -> walk_xyz() (walk_xyz_3(x2) x1) 14: comp_f(x2) walk_xyz_3(x1) -> comp_f_g(x2, walk_xyz_3(x1)) 15: comp() x0 -> comp_f(x0) 16: main() -> 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 Nil :: 'a list S :: nat -> nat comp :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f_g :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list walk_xyz :: nat list -> nat list walk_xyz_3 :: nat -> nat list -> nat list walk :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list main :: nat list + Applied Processor: UncurryATRS + Details: none * Step 11: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk_xyz#1(Cons(x1, x2)) -> Cons(x1, x2) 2: walk_xyz_3#1(x3, x5) -> Cons(x3, x5) 3: walk#1(comp(), Nil()) -> walk_xyz() 4: walk#2(comp(), Nil(), x0) -> walk_xyz#1(x0) 5: walk#1(comp(), Cons(x2, x1)) -> comp#2(walk#1(comp(), x1), walk_xyz_3(x2)) 6: walk#2(comp(), Cons(x2, x1), x3) -> comp#3(walk#1(comp(), x1), walk_xyz_3(x2), x3) 7: comp_f_g#1(comp_f_g(x3, x4), walk_xyz_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xyz_3#1(x2, x1)) 8: comp_f_g#1(walk_xyz(), walk_xyz_3(x2), x1) -> walk_xyz#1(walk_xyz_3#1(x2, x1)) 9: comp_f#1(x2, walk_xyz_3(x1)) -> comp_f_g(x2, walk_xyz_3(x1)) 10: comp_f#2(x2, walk_xyz_3(x1), x3) -> comp_f_g#1(x2, walk_xyz_3(x1), x3) 11: comp#1(x0) -> comp_f(x0) 12: comp#2(x0, x1) -> comp_f#1(x0, x1) 13: comp#3(x0, x1, x2) -> comp_f#2(x0, x1, x2) 14: main() -> walk#2(comp(), Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))), Nil()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp#1 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp#2 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp#3 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f#1 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f#2 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f_g :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f_g#1 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list main :: nat list walk#1 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list walk#2 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list walk_xyz :: nat list -> nat list walk_xyz#1 :: nat list -> nat list walk_xyz_3 :: nat -> nat list -> nat list walk_xyz_3#1 :: nat -> nat list -> nat list + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 12: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk_xyz#1(Cons(x1, x2)) -> Cons(x1, x2) 2: walk_xyz_3#1(x3, x5) -> Cons(x3, x5) 3: walk#1(comp(), Nil()) -> walk_xyz() 5: walk#1(comp(), Cons(x2, x1)) -> comp#2(walk#1(comp(), x1), walk_xyz_3(x2)) 6: walk#2(comp(), Cons(x2, x1), x3) -> comp#3(walk#1(comp(), x1), walk_xyz_3(x2), x3) 7: comp_f_g#1(comp_f_g(x3, x4), walk_xyz_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xyz_3#1(x2, x1)) 8: comp_f_g#1(walk_xyz(), walk_xyz_3(x2), x1) -> walk_xyz#1(walk_xyz_3#1(x2, x1)) 9: comp_f#1(x2, walk_xyz_3(x1)) -> comp_f_g(x2, walk_xyz_3(x1)) 10: comp_f#2(x2, walk_xyz_3(x1), x3) -> comp_f_g#1(x2, walk_xyz_3(x1), x3) 12: comp#2(x0, x1) -> comp_f#1(x0, x1) 13: comp#3(x0, x1, x2) -> comp_f#2(x0, x1, x2) 14: main() -> walk#2(comp(), Cons(S(0()), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))), Nil()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp#2 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp#3 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f#1 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f#2 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f_g :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f_g#1 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list main :: nat list walk#1 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list walk#2 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list walk_xyz :: nat list -> nat list walk_xyz#1 :: nat list -> nat list walk_xyz_3 :: nat -> nat list -> nat list walk_xyz_3#1 :: nat -> nat list -> nat list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 13: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk_xyz#1(Cons(x1, x2)) -> Cons(x1, x2) 2: walk_xyz_3#1(x3, x5) -> Cons(x3, x5) 3: walk#1(comp(), Nil()) -> walk_xyz() 4: walk#1(comp(), Cons(x5, x3)) -> comp_f#1(walk#1(comp(), x3), walk_xyz_3(x5)) 5: walk#2(comp(), Cons(x5, x3), x4) -> comp_f#2(walk#1(comp(), x3), walk_xyz_3(x5), x4) 6: comp_f_g#1(comp_f_g(x3, x4), walk_xyz_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xyz_3#1(x2, x1)) 7: comp_f_g#1(walk_xyz(), walk_xyz_3(x2), x1) -> walk_xyz#1(walk_xyz_3#1(x2, x1)) 8: comp_f#1(x2, walk_xyz_3(x1)) -> comp_f_g(x2, walk_xyz_3(x1)) 9: comp_f#2(x2, walk_xyz_3(x1), x3) -> comp_f_g#1(x2, walk_xyz_3(x1), x3) 10: comp#2(x4, walk_xyz_3(x2)) -> comp_f_g(x4, walk_xyz_3(x2)) 11: comp#3(x4, walk_xyz_3(x2), x6) -> comp_f_g#1(x4, walk_xyz_3(x2), x6) 12: main() -> comp#3(walk#1(comp(), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))), walk_xyz_3(S(0())), Nil()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp#2 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp#3 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f#1 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f#2 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f_g :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f_g#1 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list main :: nat list walk#1 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list walk#2 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list walk_xyz :: nat list -> nat list walk_xyz#1 :: nat list -> nat list walk_xyz_3 :: nat -> nat list -> nat list walk_xyz_3#1 :: nat -> nat list -> nat list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 14: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk_xyz#1(Cons(x1, x2)) -> Cons(x1, x2) 2: walk_xyz_3#1(x3, x5) -> Cons(x3, x5) 3: walk#1(comp(), Nil()) -> walk_xyz() 4: walk#1(comp(), Cons(x5, x3)) -> comp_f#1(walk#1(comp(), x3), walk_xyz_3(x5)) 6: comp_f_g#1(comp_f_g(x3, x4), walk_xyz_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xyz_3#1(x2, x1)) 7: comp_f_g#1(walk_xyz(), walk_xyz_3(x2), x1) -> walk_xyz#1(walk_xyz_3#1(x2, x1)) 8: comp_f#1(x2, walk_xyz_3(x1)) -> comp_f_g(x2, walk_xyz_3(x1)) 11: comp#3(x4, walk_xyz_3(x2), x6) -> comp_f_g#1(x4, walk_xyz_3(x2), x6) 12: main() -> comp#3(walk#1(comp(), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))), walk_xyz_3(S(0())), Nil()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp#3 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f#1 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f_g :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f_g#1 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list main :: nat list walk#1 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list walk_xyz :: nat list -> nat list walk_xyz#1 :: nat list -> nat list walk_xyz_3 :: nat -> nat list -> nat list walk_xyz_3#1 :: nat -> nat list -> nat list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 15: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk_xyz#1(Cons(x1, x2)) -> Cons(x1, x2) 2: walk_xyz_3#1(x3, x5) -> Cons(x3, x5) 3: walk#1(comp(), Nil()) -> walk_xyz() 4: walk#1(comp(), Cons(x2, x7)) -> comp_f_g(walk#1(comp(), x7), walk_xyz_3(x2)) 5: comp_f_g#1(comp_f_g(x3, x4), walk_xyz_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xyz_3#1(x2, x1)) 6: comp_f_g#1(walk_xyz(), walk_xyz_3(x2), x1) -> walk_xyz#1(walk_xyz_3#1(x2, x1)) 7: comp_f#1(x2, walk_xyz_3(x1)) -> comp_f_g(x2, walk_xyz_3(x1)) 8: comp#3(x4, walk_xyz_3(x2), x6) -> comp_f_g#1(x4, walk_xyz_3(x2), x6) 9: main() -> comp_f_g#1(walk#1(comp(), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))), walk_xyz_3(S(0())) , Nil()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp#3 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f#1 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f_g :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f_g#1 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list main :: nat list walk#1 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list walk_xyz :: nat list -> nat list walk_xyz#1 :: nat list -> nat list walk_xyz_3 :: nat -> nat list -> nat list walk_xyz_3#1 :: nat -> nat list -> nat list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 16: Compression WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk_xyz#1(Cons(x1, x2)) -> Cons(x1, x2) 2: walk_xyz_3#1(x3, x5) -> Cons(x3, x5) 3: walk#1(comp(), Nil()) -> walk_xyz() 4: walk#1(comp(), Cons(x2, x7)) -> comp_f_g(walk#1(comp(), x7), walk_xyz_3(x2)) 5: comp_f_g#1(comp_f_g(x3, x4), walk_xyz_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xyz_3#1(x2, x1)) 6: comp_f_g#1(walk_xyz(), walk_xyz_3(x2), x1) -> walk_xyz#1(walk_xyz_3#1(x2, x1)) 9: main() -> comp_f_g#1(walk#1(comp(), Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))), walk_xyz_3(S(0())) , Nil()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f_g :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f_g#1 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list main :: nat list walk#1 :: ((nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list) -> nat list -> nat list -> nat list walk_xyz :: nat list -> nat list walk_xyz#1 :: nat list -> nat list walk_xyz_3 :: nat -> nat list -> nat list walk_xyz_3#1 :: nat -> nat list -> nat list + Applied Processor: Compression + Details: none * Step 17: ToTctProblem WORST_CASE(?,O(n^1)) + Considered Problem: 1: walk_xyz#1(Cons(x1, x2)) -> Cons(x1, x2) 2: walk_xyz_3#1(x3, x5) -> Cons(x3, x5) 3: walk#1(Nil()) -> walk_xyz() 4: walk#1(Cons(x2, x7)) -> comp_f_g(walk#1(x7), walk_xyz_3(x2)) 5: comp_f_g#1(comp_f_g(x3, x4), walk_xyz_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xyz_3#1(x2, x1)) 6: comp_f_g#1(walk_xyz(), walk_xyz_3(x2), x1) -> walk_xyz#1(walk_xyz_3#1(x2, x1)) 7: main() -> comp_f_g#1(walk#1(Cons(S(S(0())), Cons(S(S(S(0()))), Nil()))), walk_xyz_3(S(0())), Nil()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat comp_f_g :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list comp_f_g#1 :: (nat list -> nat list) -> (nat list -> nat list) -> nat list -> nat list main :: nat list walk#1 :: nat list -> nat list -> nat list walk_xyz :: nat list -> nat list walk_xyz#1 :: nat list -> nat list walk_xyz_3 :: nat -> nat list -> nat list walk_xyz_3#1 :: nat -> nat list -> nat list + Applied Processor: ToTctProblem + Details: none * Step 18: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: comp_f_g#1(comp_f_g(x3,x4),walk_xyz_3(x2),x1) -> comp_f_g#1(x3,x4,walk_xyz_3#1(x2,x1)) comp_f_g#1(walk_xyz(),walk_xyz_3(x2),x1) -> walk_xyz#1(walk_xyz_3#1(x2,x1)) main() -> comp_f_g#1(walk#1(Cons(S(S(0())),Cons(S(S(S(0()))),Nil()))),walk_xyz_3(S(0())),Nil()) walk#1(Cons(x2,x7)) -> comp_f_g(walk#1(x7),walk_xyz_3(x2)) walk#1(Nil()) -> walk_xyz() walk_xyz#1(Cons(x1,x2)) -> Cons(x1,x2) walk_xyz_3#1(x3,x5) -> Cons(x3,x5) - Signature: {comp_f_g#1/3,main/0,walk#1/1,walk_xyz#1/1,walk_xyz_3#1/2} / {0/0,Cons/2,Nil/0,S/1,comp_f_g/2,walk_xyz/0 ,walk_xyz_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,Cons,Nil,S} + 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}, uargs(comp_f_g#1) = {1,3}, uargs(walk_xyz#1) = {1} Following symbols are considered usable: {comp_f_g#1,main,walk#1,walk_xyz#1,walk_xyz_3#1} TcT has computed the following interpretation: p(0) = 1 p(Cons) = x2 p(Nil) = 0 p(S) = 0 p(comp_f_g) = x1 p(comp_f_g#1) = x1 + 4*x3 p(main) = 15 p(walk#1) = 8 + 4*x1 p(walk_xyz) = 0 p(walk_xyz#1) = x1 p(walk_xyz_3) = 0 p(walk_xyz_3#1) = x2 Following rules are strictly oriented: main() = 15 > 8 = comp_f_g#1(walk#1(Cons(S(S(0())),Cons(S(S(S(0()))),Nil()))),walk_xyz_3(S(0())),Nil()) walk#1(Nil()) = 8 > 0 = walk_xyz() Following rules are (at-least) weakly oriented: comp_f_g#1(comp_f_g(x3,x4),walk_xyz_3(x2),x1) = 4*x1 + x3 >= 4*x1 + x3 = comp_f_g#1(x3,x4,walk_xyz_3#1(x2,x1)) comp_f_g#1(walk_xyz(),walk_xyz_3(x2),x1) = 4*x1 >= x1 = walk_xyz#1(walk_xyz_3#1(x2,x1)) walk#1(Cons(x2,x7)) = 8 + 4*x7 >= 8 + 4*x7 = comp_f_g(walk#1(x7),walk_xyz_3(x2)) walk_xyz#1(Cons(x1,x2)) = x2 >= x2 = Cons(x1,x2) walk_xyz_3#1(x3,x5) = x5 >= x5 = Cons(x3,x5) * Step 19: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: comp_f_g#1(comp_f_g(x3,x4),walk_xyz_3(x2),x1) -> comp_f_g#1(x3,x4,walk_xyz_3#1(x2,x1)) comp_f_g#1(walk_xyz(),walk_xyz_3(x2),x1) -> walk_xyz#1(walk_xyz_3#1(x2,x1)) walk#1(Cons(x2,x7)) -> comp_f_g(walk#1(x7),walk_xyz_3(x2)) walk_xyz#1(Cons(x1,x2)) -> Cons(x1,x2) walk_xyz_3#1(x3,x5) -> Cons(x3,x5) - Weak TRS: main() -> comp_f_g#1(walk#1(Cons(S(S(0())),Cons(S(S(S(0()))),Nil()))),walk_xyz_3(S(0())),Nil()) walk#1(Nil()) -> walk_xyz() - Signature: {comp_f_g#1/3,main/0,walk#1/1,walk_xyz#1/1,walk_xyz_3#1/2} / {0/0,Cons/2,Nil/0,S/1,comp_f_g/2,walk_xyz/0 ,walk_xyz_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,Cons,Nil,S} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(comp_f_g) = {1}, uargs(comp_f_g#1) = {1,3}, uargs(walk_xyz#1) = {1} Following symbols are considered usable: {comp_f_g#1,main,walk#1,walk_xyz#1,walk_xyz_3#1} TcT has computed the following interpretation: p(0) = [0] p(Cons) = [0] p(Nil) = [0] p(S) = [4] p(comp_f_g) = [8] x1 + [0] p(comp_f_g#1) = [1] x1 + [1] x3 + [4] p(main) = [5] p(walk#1) = [0] p(walk_xyz) = [0] p(walk_xyz#1) = [8] x1 + [4] p(walk_xyz_3) = [4] x1 + [5] p(walk_xyz_3#1) = [0] Following rules are strictly oriented: walk_xyz#1(Cons(x1,x2)) = [4] > [0] = Cons(x1,x2) Following rules are (at-least) weakly oriented: comp_f_g#1(comp_f_g(x3,x4),walk_xyz_3(x2),x1) = [1] x1 + [8] x3 + [4] >= [1] x3 + [4] = comp_f_g#1(x3,x4,walk_xyz_3#1(x2,x1)) comp_f_g#1(walk_xyz(),walk_xyz_3(x2),x1) = [1] x1 + [4] >= [4] = walk_xyz#1(walk_xyz_3#1(x2,x1)) main() = [5] >= [4] = comp_f_g#1(walk#1(Cons(S(S(0())),Cons(S(S(S(0()))),Nil()))),walk_xyz_3(S(0())),Nil()) walk#1(Cons(x2,x7)) = [0] >= [0] = comp_f_g(walk#1(x7),walk_xyz_3(x2)) walk#1(Nil()) = [0] >= [0] = walk_xyz() walk_xyz_3#1(x3,x5) = [0] >= [0] = Cons(x3,x5) * Step 20: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: comp_f_g#1(comp_f_g(x3,x4),walk_xyz_3(x2),x1) -> comp_f_g#1(x3,x4,walk_xyz_3#1(x2,x1)) comp_f_g#1(walk_xyz(),walk_xyz_3(x2),x1) -> walk_xyz#1(walk_xyz_3#1(x2,x1)) walk#1(Cons(x2,x7)) -> comp_f_g(walk#1(x7),walk_xyz_3(x2)) walk_xyz_3#1(x3,x5) -> Cons(x3,x5) - Weak TRS: main() -> comp_f_g#1(walk#1(Cons(S(S(0())),Cons(S(S(S(0()))),Nil()))),walk_xyz_3(S(0())),Nil()) walk#1(Nil()) -> walk_xyz() walk_xyz#1(Cons(x1,x2)) -> Cons(x1,x2) - Signature: {comp_f_g#1/3,main/0,walk#1/1,walk_xyz#1/1,walk_xyz_3#1/2} / {0/0,Cons/2,Nil/0,S/1,comp_f_g/2,walk_xyz/0 ,walk_xyz_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,Cons,Nil,S} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(comp_f_g) = {1}, uargs(comp_f_g#1) = {1,3}, uargs(walk_xyz#1) = {1} Following symbols are considered usable: {comp_f_g#1,main,walk#1,walk_xyz#1,walk_xyz_3#1} TcT has computed the following interpretation: p(0) = [0] p(Cons) = [0] p(Nil) = [0] p(S) = [2] p(comp_f_g) = [1] x1 + [0] p(comp_f_g#1) = [4] x1 + [2] x3 + [6] p(main) = [6] p(walk#1) = [0] p(walk_xyz) = [0] p(walk_xyz#1) = [8] x1 + [0] p(walk_xyz_3) = [14] p(walk_xyz_3#1) = [0] Following rules are strictly oriented: comp_f_g#1(walk_xyz(),walk_xyz_3(x2),x1) = [2] x1 + [6] > [0] = walk_xyz#1(walk_xyz_3#1(x2,x1)) Following rules are (at-least) weakly oriented: comp_f_g#1(comp_f_g(x3,x4),walk_xyz_3(x2),x1) = [2] x1 + [4] x3 + [6] >= [4] x3 + [6] = comp_f_g#1(x3,x4,walk_xyz_3#1(x2,x1)) main() = [6] >= [6] = comp_f_g#1(walk#1(Cons(S(S(0())),Cons(S(S(S(0()))),Nil()))),walk_xyz_3(S(0())),Nil()) walk#1(Cons(x2,x7)) = [0] >= [0] = comp_f_g(walk#1(x7),walk_xyz_3(x2)) walk#1(Nil()) = [0] >= [0] = walk_xyz() walk_xyz#1(Cons(x1,x2)) = [0] >= [0] = Cons(x1,x2) walk_xyz_3#1(x3,x5) = [0] >= [0] = Cons(x3,x5) * Step 21: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: comp_f_g#1(comp_f_g(x3,x4),walk_xyz_3(x2),x1) -> comp_f_g#1(x3,x4,walk_xyz_3#1(x2,x1)) walk#1(Cons(x2,x7)) -> comp_f_g(walk#1(x7),walk_xyz_3(x2)) walk_xyz_3#1(x3,x5) -> Cons(x3,x5) - Weak TRS: comp_f_g#1(walk_xyz(),walk_xyz_3(x2),x1) -> walk_xyz#1(walk_xyz_3#1(x2,x1)) main() -> comp_f_g#1(walk#1(Cons(S(S(0())),Cons(S(S(S(0()))),Nil()))),walk_xyz_3(S(0())),Nil()) walk#1(Nil()) -> walk_xyz() walk_xyz#1(Cons(x1,x2)) -> Cons(x1,x2) - Signature: {comp_f_g#1/3,main/0,walk#1/1,walk_xyz#1/1,walk_xyz_3#1/2} / {0/0,Cons/2,Nil/0,S/1,comp_f_g/2,walk_xyz/0 ,walk_xyz_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,Cons,Nil,S} + 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}, uargs(comp_f_g#1) = {1,3}, uargs(walk_xyz#1) = {1} Following symbols are considered usable: {comp_f_g#1,main,walk#1,walk_xyz#1,walk_xyz_3#1} TcT has computed the following interpretation: p(0) = 2 p(Cons) = 1 + x2 p(Nil) = 0 p(S) = 4 p(comp_f_g) = 3 + x1 p(comp_f_g#1) = 5 + x1 + 2*x3 p(main) = 15 p(walk#1) = 5*x1 p(walk_xyz) = 0 p(walk_xyz#1) = 1 + 2*x1 p(walk_xyz_3) = 0 p(walk_xyz_3#1) = 1 + x2 Following rules are strictly oriented: comp_f_g#1(comp_f_g(x3,x4),walk_xyz_3(x2),x1) = 8 + 2*x1 + x3 > 7 + 2*x1 + x3 = comp_f_g#1(x3,x4,walk_xyz_3#1(x2,x1)) walk#1(Cons(x2,x7)) = 5 + 5*x7 > 3 + 5*x7 = comp_f_g(walk#1(x7),walk_xyz_3(x2)) Following rules are (at-least) weakly oriented: comp_f_g#1(walk_xyz(),walk_xyz_3(x2),x1) = 5 + 2*x1 >= 3 + 2*x1 = walk_xyz#1(walk_xyz_3#1(x2,x1)) main() = 15 >= 15 = comp_f_g#1(walk#1(Cons(S(S(0())),Cons(S(S(S(0()))),Nil()))),walk_xyz_3(S(0())),Nil()) walk#1(Nil()) = 0 >= 0 = walk_xyz() walk_xyz#1(Cons(x1,x2)) = 3 + 2*x2 >= 1 + x2 = Cons(x1,x2) walk_xyz_3#1(x3,x5) = 1 + x5 >= 1 + x5 = Cons(x3,x5) * Step 22: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: walk_xyz_3#1(x3,x5) -> Cons(x3,x5) - Weak TRS: comp_f_g#1(comp_f_g(x3,x4),walk_xyz_3(x2),x1) -> comp_f_g#1(x3,x4,walk_xyz_3#1(x2,x1)) comp_f_g#1(walk_xyz(),walk_xyz_3(x2),x1) -> walk_xyz#1(walk_xyz_3#1(x2,x1)) main() -> comp_f_g#1(walk#1(Cons(S(S(0())),Cons(S(S(S(0()))),Nil()))),walk_xyz_3(S(0())),Nil()) walk#1(Cons(x2,x7)) -> comp_f_g(walk#1(x7),walk_xyz_3(x2)) walk#1(Nil()) -> walk_xyz() walk_xyz#1(Cons(x1,x2)) -> Cons(x1,x2) - Signature: {comp_f_g#1/3,main/0,walk#1/1,walk_xyz#1/1,walk_xyz_3#1/2} / {0/0,Cons/2,Nil/0,S/1,comp_f_g/2,walk_xyz/0 ,walk_xyz_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,Cons,Nil,S} + 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}, uargs(comp_f_g#1) = {1,3}, uargs(walk_xyz#1) = {1} Following symbols are considered usable: {comp_f_g#1,main,walk#1,walk_xyz#1,walk_xyz_3#1} TcT has computed the following interpretation: p(0) = 1 p(Cons) = 1 + x2 p(Nil) = 1 p(S) = 0 p(comp_f_g) = 1 + x1 p(comp_f_g#1) = 4*x1 + x3 p(main) = 14 p(walk#1) = x1 p(walk_xyz) = 1 p(walk_xyz#1) = 2 + x1 p(walk_xyz_3) = 0 p(walk_xyz_3#1) = 2 + x2 Following rules are strictly oriented: walk_xyz_3#1(x3,x5) = 2 + x5 > 1 + x5 = Cons(x3,x5) Following rules are (at-least) weakly oriented: comp_f_g#1(comp_f_g(x3,x4),walk_xyz_3(x2),x1) = 4 + x1 + 4*x3 >= 2 + x1 + 4*x3 = comp_f_g#1(x3,x4,walk_xyz_3#1(x2,x1)) comp_f_g#1(walk_xyz(),walk_xyz_3(x2),x1) = 4 + x1 >= 4 + x1 = walk_xyz#1(walk_xyz_3#1(x2,x1)) main() = 14 >= 13 = comp_f_g#1(walk#1(Cons(S(S(0())),Cons(S(S(S(0()))),Nil()))),walk_xyz_3(S(0())),Nil()) walk#1(Cons(x2,x7)) = 1 + x7 >= 1 + x7 = comp_f_g(walk#1(x7),walk_xyz_3(x2)) walk#1(Nil()) = 1 >= 1 = walk_xyz() walk_xyz#1(Cons(x1,x2)) = 3 + x2 >= 1 + x2 = Cons(x1,x2) * Step 23: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: comp_f_g#1(comp_f_g(x3,x4),walk_xyz_3(x2),x1) -> comp_f_g#1(x3,x4,walk_xyz_3#1(x2,x1)) comp_f_g#1(walk_xyz(),walk_xyz_3(x2),x1) -> walk_xyz#1(walk_xyz_3#1(x2,x1)) main() -> comp_f_g#1(walk#1(Cons(S(S(0())),Cons(S(S(S(0()))),Nil()))),walk_xyz_3(S(0())),Nil()) walk#1(Cons(x2,x7)) -> comp_f_g(walk#1(x7),walk_xyz_3(x2)) walk#1(Nil()) -> walk_xyz() walk_xyz#1(Cons(x1,x2)) -> Cons(x1,x2) walk_xyz_3#1(x3,x5) -> Cons(x3,x5) - Signature: {comp_f_g#1/3,main/0,walk#1/1,walk_xyz#1/1,walk_xyz_3#1/2} / {0/0,Cons/2,Nil/0,S/1,comp_f_g/2,walk_xyz/0 ,walk_xyz_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,Cons,Nil,S} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))