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 = <inline non-recursive>}
    + 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 = <inline non-recursive>}
    + 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 = <inline non-recursive>}
    + 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 = <inline case-expression>}
    + 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 = <control flow analysis>}
    + 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 = <inline decreasing>}
    + 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 = <inline decreasing>}
    + 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))