WORST_CASE(?,O(n^1))
* Step 1: Desugar WORST_CASE(?,O(n^1))
    + Considered Problem:
        let comp f g x = f (g x) ;;
        
        type 'a list = Nil | Cons of 'a * 'a list
        ;;
        
        (* rev :: list -> list *)
        let rev l =
          (* walk :: list -> (list -> list) *)
          let rec walk xs = 
            match xs with 
            | Nil -> (fun x -> x)
            | Cons(x,xs') ->
               comp (walk xs')
        	 (fun ys -> Cons(x,ys))
          in walk l Nil
        ;;	  
        	  
    + Applied Processor:
        Desugar {analysedFunction = Nothing}
    + Details:
        none
* Step 2: Defunctionalization WORST_CASE(?,O(n^1))
    + Considered Problem:
        λl : 'l list.
          (λcomp : ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list.
             (λrev : 'l list -> 'l list. rev l)
               (λl : 'l list.
                  (λwalk : 'l list -> 'l list -> 'l list. walk l Nil)
                    (μwalk : 'l list -> 'l list -> 'l list.
                       λxs : 'l list.
                         case xs of
                          | Nil -> λx : 'l list.
                                     x
                          | Cons -> λx : 'l.
                                      λxs' : 'l list. comp (walk xs') (λys : 'l list. Cons(x,ys)))))
            (λf : 'l list -> 'l list. λg : 'l list -> 'l list. λx : 'l list. f (g x)) : 'l list -> 'l list
        where
          Cons :: 'a -> 'a list -> 'a list
          Nil  :: 'a list
    + Applied Processor:
        Defunctionalization
    + Details:
        none
* Step 3: Inline WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: main_2(x0) x2 -> x2 x0
        2: rev_l(x2) x3 -> x3 x2 Nil()
        3: walk_xs() x4 -> x4
        4: walk_xs_3(x4) x6 -> Cons(x4, x6)
        5: cond_walk_xs(Nil(), x1) -> walk_xs()
        6: cond_walk_xs(Cons(x4, x5), x1) -> x1 (walk(x1) x5) walk_xs_3(x4)
        7: walk_1(x1) x3 -> cond_walk_xs(x3, x1)
        8: walk(x1) x2 -> walk_1(x1) x2
        9: rev(x1) x2 -> rev_l(x2) walk(x1)
        10: main_1(x0) x1 -> main_2(x0) rev(x1)
        11: comp_f_g(x1, x2) x3 -> x1 (x2 x3)
        12: comp_f(x1) x2 -> comp_f_g(x1, x2)
        13: comp() x1 -> comp_f(x1)
        14: main(x0) -> main_1(x0) comp()
        where
          Cons         :: 'a -> 'a list -> 'a list
          Nil          :: 'a list
          comp         :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f       :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g     :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          rev_l        :: 'l list -> ('l list -> 'l list -> 'l list) -> 'l list
          rev          :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list
          walk_xs      :: 'l list -> 'l list
          main_1       :: 'l list -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list
          walk_1       :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                           -> 'l list
                           -> 'l list
                           -> 'l list
          main_2       :: 'l list -> ('l list -> 'l list) -> 'l list
          walk_xs_3    :: 'l -> 'l list -> 'l list
          cond_walk_xs :: 'l list
                           -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                           -> 'l list
                           -> 'l list
          walk         :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                           -> 'l list
                           -> 'l list
                           -> 'l list
          main         :: 'l list -> 'l list
    + Applied Processor:
        Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
    + Details:
        none
* Step 4: Inline WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: main_2(x0) x2 -> x2 x0
        2: rev_l(x2) x3 -> x3 x2 Nil()
        3: walk_xs() x4 -> x4
        4: walk_xs_3(x4) x6 -> Cons(x4, x6)
        5: cond_walk_xs(Nil(), x1) -> walk_xs()
        6: cond_walk_xs(Cons(x4, x5), x1) -> x1 (walk(x1) x5) walk_xs_3(x4)
        7: walk_1(x1) x3 -> cond_walk_xs(x3, x1)
        8: walk(x2) x6 -> cond_walk_xs(x6, x2)
        9: rev(x3) x4 -> walk(x3) x4 Nil()
        10: main_1(x0) x3 -> rev(x3) x0
        11: comp_f_g(x1, x2) x3 -> x1 (x2 x3)
        12: comp_f(x1) x2 -> comp_f_g(x1, x2)
        13: comp() x1 -> comp_f(x1)
        14: main(x0) -> main_2(x0) rev(comp())
        where
          Cons         :: 'a -> 'a list -> 'a list
          Nil          :: 'a list
          comp         :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f       :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g     :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          rev_l        :: 'l list -> ('l list -> 'l list -> 'l list) -> 'l list
          rev          :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list
          walk_xs      :: 'l list -> 'l list
          main_1       :: 'l list -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list
          walk_1       :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                           -> 'l list
                           -> 'l list
                           -> 'l list
          main_2       :: 'l list -> ('l list -> 'l list) -> 'l list
          walk_xs_3    :: 'l -> 'l list -> 'l list
          cond_walk_xs :: 'l list
                           -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                           -> 'l list
                           -> 'l list
          walk         :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                           -> 'l list
                           -> 'l list
                           -> 'l list
          main         :: 'l list -> 'l list
    + Applied Processor:
        Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
    + Details:
        none
* Step 5: Inline WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: main_2(x0) x2 -> x2 x0
        2: rev_l(x2) x3 -> x3 x2 Nil()
        3: walk_xs() x4 -> x4
        4: walk_xs_3(x4) x6 -> Cons(x4, x6)
        5: cond_walk_xs(Nil(), x1) -> walk_xs()
        6: cond_walk_xs(Cons(x4, x5), x1) -> x1 (walk(x1) x5) walk_xs_3(x4)
        7: walk_1(x1) x3 -> cond_walk_xs(x3, x1)
        8: walk(x2) x6 -> cond_walk_xs(x6, x2)
        9: rev(x3) x4 -> walk(x3) x4 Nil()
        10: main_1(x8) x6 -> walk(x6) x8 Nil()
        11: comp_f_g(x1, x2) x3 -> x1 (x2 x3)
        12: comp_f(x1) x2 -> comp_f_g(x1, x2)
        13: comp() x1 -> comp_f(x1)
        14: main(x0) -> rev(comp()) x0
        where
          Cons         :: 'a -> 'a list -> 'a list
          Nil          :: 'a list
          comp         :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f       :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g     :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          rev_l        :: 'l list -> ('l list -> 'l list -> 'l list) -> 'l list
          rev          :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list
          walk_xs      :: 'l list -> 'l list
          main_1       :: 'l list -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list
          walk_1       :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                           -> 'l list
                           -> 'l list
                           -> 'l list
          main_2       :: 'l list -> ('l list -> 'l list) -> 'l list
          walk_xs_3    :: 'l -> 'l list -> 'l list
          cond_walk_xs :: 'l list
                           -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                           -> 'l list
                           -> 'l list
          walk         :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                           -> 'l list
                           -> 'l list
                           -> 'l list
          main         :: 'l list -> 'l list
    + Applied Processor:
        Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
    + Details:
        none
* Step 6: Inline WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: main_2(x0) x2 -> x2 x0
        2: rev_l(x2) x3 -> x3 x2 Nil()
        3: walk_xs() x4 -> x4
        4: walk_xs_3(x4) x6 -> Cons(x4, x6)
        5: cond_walk_xs(Nil(), x1) -> walk_xs()
        6: cond_walk_xs(Cons(x4, x5), x1) -> x1 (walk(x1) x5) walk_xs_3(x4)
        7: walk_1(x1) x3 -> cond_walk_xs(x3, x1)
        8: walk(x2) x6 -> cond_walk_xs(x6, x2)
        9: rev(x3) x4 -> walk(x3) x4 Nil()
        10: main_1(x8) x6 -> walk(x6) x8 Nil()
        11: comp_f_g(x1, x2) x3 -> x1 (x2 x3)
        12: comp_f(x1) x2 -> comp_f_g(x1, x2)
        13: comp() x1 -> comp_f(x1)
        14: main(x8) -> walk(comp()) x8 Nil()
        where
          Cons         :: 'a -> 'a list -> 'a list
          Nil          :: 'a list
          comp         :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f       :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g     :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          rev_l        :: 'l list -> ('l list -> 'l list -> 'l list) -> 'l list
          rev          :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list
          walk_xs      :: 'l list -> 'l list
          main_1       :: 'l list -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list
          walk_1       :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                           -> 'l list
                           -> 'l list
                           -> 'l list
          main_2       :: 'l list -> ('l list -> 'l list) -> 'l list
          walk_xs_3    :: 'l -> 'l list -> 'l list
          cond_walk_xs :: 'l list
                           -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                           -> 'l list
                           -> 'l list
          walk         :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                           -> 'l list
                           -> 'l list
                           -> 'l list
          main         :: 'l list -> 'l list
    + Applied Processor:
        Inline {inlineType = InlineFull, inlineSelect = <inline case-expression>}
    + Details:
        none
* Step 7: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: main_2(x0) x2 -> x2 x0
        2: rev_l(x2) x3 -> x3 x2 Nil()
        3: walk_xs() x4 -> x4
        4: walk_xs_3(x4) x6 -> Cons(x4, x6)
        5: cond_walk_xs(Nil(), x1) -> walk_xs()
        6: cond_walk_xs(Cons(x4, x5), x1) -> x1 (walk(x1) x5) walk_xs_3(x4)
        7: walk_1(x2) Nil() -> walk_xs()
        8: walk_1(x2) Cons(x8, x10) -> x2 (walk(x2) x10) walk_xs_3(x8)
        9: walk(x2) Nil() -> walk_xs()
        10: walk(x2) Cons(x8, x10) -> x2 (walk(x2) x10) walk_xs_3(x8)
        11: rev(x3) x4 -> walk(x3) x4 Nil()
        12: main_1(x8) x6 -> walk(x6) x8 Nil()
        13: comp_f_g(x1, x2) x3 -> x1 (x2 x3)
        14: comp_f(x1) x2 -> comp_f_g(x1, x2)
        15: comp() x1 -> comp_f(x1)
        16: main(x8) -> walk(comp()) x8 Nil()
        where
          Cons         :: 'a -> 'a list -> 'a list
          Nil          :: 'a list
          comp         :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f       :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g     :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          rev_l        :: 'l list -> ('l list -> 'l list -> 'l list) -> 'l list
          rev          :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list
          walk_xs      :: 'l list -> 'l list
          main_1       :: 'l list -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list
          walk_1       :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                           -> 'l list
                           -> 'l list
                           -> 'l list
          main_2       :: 'l list -> ('l list -> 'l list) -> 'l list
          walk_xs_3    :: 'l -> 'l list -> 'l list
          cond_walk_xs :: 'l list
                           -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                           -> 'l list
                           -> 'l list
          walk         :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                           -> 'l list
                           -> 'l list
                           -> 'l list
          main         :: 'l list -> 'l list
    + Applied Processor:
        UsableRules {urType = Syntactic}
    + Details:
        none
* Step 8: NeededRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: main_2(x0) x2 -> x2 x0
        2: rev_l(x2) x3 -> x3 x2 Nil()
        3: walk_xs() x4 -> x4
        4: walk_xs_3(x4) x6 -> Cons(x4, x6)
        7: walk_1(x2) Nil() -> walk_xs()
        8: walk_1(x2) Cons(x8, x10) -> x2 (walk(x2) x10) walk_xs_3(x8)
        9: walk(x2) Nil() -> walk_xs()
        10: walk(x2) Cons(x8, x10) -> x2 (walk(x2) x10) walk_xs_3(x8)
        11: rev(x3) x4 -> walk(x3) x4 Nil()
        12: main_1(x8) x6 -> walk(x6) x8 Nil()
        13: comp_f_g(x1, x2) x3 -> x1 (x2 x3)
        14: comp_f(x1) x2 -> comp_f_g(x1, x2)
        15: comp() x1 -> comp_f(x1)
        16: main(x8) -> walk(comp()) x8 Nil()
        where
          Cons      :: 'a -> 'a list -> 'a list
          Nil       :: 'a list
          comp      :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f    :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g  :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          rev_l     :: 'l list -> ('l list -> 'l list -> 'l list) -> 'l list
          rev       :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list
          walk_xs   :: 'l list -> 'l list
          main_1    :: 'l list -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list
          walk_1    :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                        -> 'l list
                        -> 'l list
                        -> 'l list
          main_2    :: 'l list -> ('l list -> 'l list) -> 'l list
          walk_xs_3 :: 'l -> 'l list -> 'l list
          walk      :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                        -> 'l list
                        -> 'l list
                        -> 'l list
          main      :: 'l list -> 'l list
    + Applied Processor:
        NeededRules
    + Details:
        none
* Step 9: CFA WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: main_2(x0) x2 -> x2 x0
        2: rev_l(x2) x3 -> x3 x2 Nil()
        3: walk_xs() x4 -> x4
        4: walk_xs_3(x4) x6 -> Cons(x4, x6)
        5: walk_1(x2) Nil() -> walk_xs()
        6: walk_1(x2) Cons(x8, x10) -> x2 (walk(x2) x10) walk_xs_3(x8)
        7: walk(x2) Nil() -> walk_xs()
        8: walk(x2) Cons(x8, x10) -> x2 (walk(x2) x10) walk_xs_3(x8)
        9: rev(x3) x4 -> walk(x3) x4 Nil()
        10: main_1(x8) x6 -> walk(x6) x8 Nil()
        11: comp_f_g(x1, x2) x3 -> x1 (x2 x3)
        12: comp_f(x1) x2 -> comp_f_g(x1, x2)
        13: comp() x1 -> comp_f(x1)
        14: main(x8) -> walk(comp()) x8 Nil()
        where
          Cons      :: 'a -> 'a list -> 'a list
          Nil       :: 'a list
          comp      :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f    :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g  :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          rev_l     :: 'l list -> ('l list -> 'l list -> 'l list) -> 'l list
          rev       :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list -> 'l list
          walk_xs   :: 'l list -> 'l list
          main_1    :: 'l list -> (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list) -> 'l list
          walk_1    :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                        -> 'l list
                        -> 'l list
                        -> 'l list
          main_2    :: 'l list -> ('l list -> 'l list) -> 'l list
          walk_xs_3 :: 'l -> 'l list -> 'l list
          walk      :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                        -> 'l list
                        -> 'l list
                        -> 'l list
          main      :: 'l list -> 'l list
    + Applied Processor:
        CFA {cfaRefinement = <control flow analysis>}
    + Details:
        {X{*} -> Nil()
              |  Nil()
              |  Nil()
              |  Cons(X{*},X{*})
              |  Nil()
              |  Cons(X{*},X{*})
              |  Nil()
              |  Cons(X{*},X{*})
              |  Nil()
        ,V{x1_11} -> V{x1_12}
        ,V{x1_12} -> V{x1_13}
        ,V{x1_13} -> R{8}
                  |  R{7}
        ,V{x2_7} -> V{x2_8}
                 |  comp()
        ,V{x2_8} -> V{x2_8}
                 |  comp()
        ,V{x2_11} -> V{x2_12}
        ,V{x2_12} -> walk_xs_3(V{x8_8})
        ,V{x3_11} -> R{4}
                  |  Nil()
        ,V{x4_3} -> R{4}
                 |  Nil()
        ,V{x4_4} -> V{x8_8}
        ,V{x6_4} -> V{x3_11}
        ,V{x8_8} -> X{*}
        ,V{x8_14} -> X{*}
        ,V{x10_8} -> X{*}
        ,R{0} -> R{14}
              |  main(X{*})
        ,R{3} -> V{x4_3}
        ,R{4} -> Cons(V{x4_4},V{x6_4})
        ,R{7} -> walk_xs()
        ,R{8} -> R{12}
              |  @(R{13},walk_xs_3(V{x8_8}))
              |  @(@(V{x2_8},R{8}),walk_xs_3(V{x8_8}))
              |  @(@(V{x2_8},R{7}),walk_xs_3(V{x8_8}))
              |  @(@(V{x2_8},@(walk(V{x2_8}),V{x10_8})),walk_xs_3(V{x8_8}))
        ,R{11} -> R{11}
               |  R{3}
               |  @(V{x1_11},R{4})
               |  @(V{x1_11},@(V{x2_11},V{x3_11}))
        ,R{12} -> comp_f_g(V{x1_12},V{x2_12})
        ,R{13} -> comp_f(V{x1_13})
        ,R{14} -> R{11}
               |  R{3}
               |  @(R{8},Nil())
               |  @(R{7},Nil())
               |  @(@(walk(comp()),V{x8_14}),Nil())}
* Step 10: UncurryATRS WORST_CASE(?,O(n^1))
    + Considered Problem:
        3: walk_xs() x4 -> x4
        4: walk_xs_3(x4) x6 -> Cons(x4, x6)
        7: walk(comp()) Nil() -> walk_xs()
        8: walk(comp()) Cons(x2, x1) -> comp() (walk(comp()) x1) walk_xs_3(x2)
        11: comp_f_g(comp_f_g(x3, x4), walk_xs_3(x2)) x1 -> comp_f_g(x3, x4) (walk_xs_3(x2) x1)
        12: comp_f_g(walk_xs(), walk_xs_3(x2)) x1 -> walk_xs() (walk_xs_3(x2) x1)
        13: comp_f(x2) walk_xs_3(x1) -> comp_f_g(x2, walk_xs_3(x1))
        14: comp() x1 -> comp_f(x1)
        15: main(x1) -> walk(comp()) x1 Nil()
        where
          Cons      :: 'a -> 'a list -> 'a list
          Nil       :: 'a list
          comp      :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f    :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g  :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          walk_xs   :: 'l list -> 'l list
          walk_xs_3 :: 'l -> 'l list -> 'l list
          walk      :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                        -> 'l list
                        -> 'l list
                        -> 'l list
          main      :: 'l list -> 'l list
    + Applied Processor:
        UncurryATRS
    + Details:
        none
* Step 11: Inline WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: walk_xs#1(x4) -> x4
        2: walk_xs_3#1(x4, x6) -> Cons(x4, x6)
        3: walk#1(comp(), Nil()) -> walk_xs()
        4: walk#2(comp(), Nil(), x0) -> walk_xs#1(x0)
        5: walk#1(comp(), Cons(x2, x1)) -> comp#2(walk#1(comp(), x1), walk_xs_3(x2))
        6: walk#2(comp(), Cons(x2, x1), x3) -> comp#3(walk#1(comp(), x1), walk_xs_3(x2), x3)
        7: comp_f_g#1(comp_f_g(x3, x4), walk_xs_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xs_3#1(x2, x1))
        8: comp_f_g#1(walk_xs(), walk_xs_3(x2), x1) -> walk_xs#1(walk_xs_3#1(x2, x1))
        9: comp_f#1(x2, walk_xs_3(x1)) -> comp_f_g(x2, walk_xs_3(x1))
        10: comp_f#2(x2, walk_xs_3(x1), x3) -> comp_f_g#1(x2, walk_xs_3(x1), x3)
        11: comp#1(x1) -> comp_f(x1)
        12: comp#2(x1, x2) -> comp_f#1(x1, x2)
        13: comp#3(x1, x2, x3) -> comp_f#2(x1, x2, x3)
        14: main(x1) -> walk#2(comp(), x1, Nil())
        where
          Cons        :: 'a -> 'a list -> 'a list
          Nil         :: 'a list
          comp        :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp#1      :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp#2      :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp#3      :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f      :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f#1    :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f#2    :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g    :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g#1  :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          main        :: 'l list -> 'l list
          walk#1      :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                          -> 'l list
                          -> 'l list
                          -> 'l list
          walk#2      :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                          -> 'l list
                          -> 'l list
                          -> 'l list
          walk_xs     :: 'l list -> 'l list
          walk_xs#1   :: 'l list -> 'l list
          walk_xs_3   :: 'l -> 'l list -> 'l list
          walk_xs_3#1 :: 'l -> 'l list -> 'l list
    + Applied Processor:
        Inline {inlineType = InlineFull, inlineSelect = <inline decreasing>}
    + Details:
        none
* Step 12: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: walk_xs#1(x4) -> x4
        2: walk_xs_3#1(x4, x6) -> Cons(x4, x6)
        3: walk#1(comp(), Nil()) -> walk_xs()
        4: walk#2(comp(), Nil(), x8) -> x8
        5: walk#1(comp(), Cons(x2, x1)) -> comp#2(walk#1(comp(), x1), walk_xs_3(x2))
        6: walk#2(comp(), Cons(x2, x1), x3) -> comp#3(walk#1(comp(), x1), walk_xs_3(x2), x3)
        7: comp_f_g#1(comp_f_g(x3, x4), walk_xs_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xs_3#1(x2, x1))
        8: comp_f_g#1(walk_xs(), walk_xs_3(x5), x3) -> walk_xs_3#1(x5, x3)
        9: comp_f#1(x2, walk_xs_3(x1)) -> comp_f_g(x2, walk_xs_3(x1))
        10: comp_f#2(x2, walk_xs_3(x1), x3) -> comp_f_g#1(x2, walk_xs_3(x1), x3)
        11: comp#1(x1) -> comp_f(x1)
        12: comp#2(x1, x2) -> comp_f#1(x1, x2)
        13: comp#3(x1, x2, x3) -> comp_f#2(x1, x2, x3)
        14: main(x1) -> walk#2(comp(), x1, Nil())
        where
          Cons        :: 'a -> 'a list -> 'a list
          Nil         :: 'a list
          comp        :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp#1      :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp#2      :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp#3      :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f      :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f#1    :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f#2    :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g    :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g#1  :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          main        :: 'l list -> 'l list
          walk#1      :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                          -> 'l list
                          -> 'l list
                          -> 'l list
          walk#2      :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                          -> 'l list
                          -> 'l list
                          -> 'l list
          walk_xs     :: 'l list -> 'l list
          walk_xs#1   :: 'l list -> 'l list
          walk_xs_3   :: 'l -> 'l list -> 'l list
          walk_xs_3#1 :: 'l -> 'l list -> 'l list
    + Applied Processor:
        UsableRules {urType = Syntactic}
    + Details:
        none
* Step 13: Inline WORST_CASE(?,O(n^1))
    + Considered Problem:
        2: walk_xs_3#1(x4, x6) -> Cons(x4, x6)
        3: walk#1(comp(), Nil()) -> walk_xs()
        4: walk#2(comp(), Nil(), x8) -> x8
        5: walk#1(comp(), Cons(x2, x1)) -> comp#2(walk#1(comp(), x1), walk_xs_3(x2))
        6: walk#2(comp(), Cons(x2, x1), x3) -> comp#3(walk#1(comp(), x1), walk_xs_3(x2), x3)
        7: comp_f_g#1(comp_f_g(x3, x4), walk_xs_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xs_3#1(x2, x1))
        8: comp_f_g#1(walk_xs(), walk_xs_3(x5), x3) -> walk_xs_3#1(x5, x3)
        9: comp_f#1(x2, walk_xs_3(x1)) -> comp_f_g(x2, walk_xs_3(x1))
        10: comp_f#2(x2, walk_xs_3(x1), x3) -> comp_f_g#1(x2, walk_xs_3(x1), x3)
        12: comp#2(x1, x2) -> comp_f#1(x1, x2)
        13: comp#3(x1, x2, x3) -> comp_f#2(x1, x2, x3)
        14: main(x1) -> walk#2(comp(), x1, Nil())
        where
          Cons        :: 'a -> 'a list -> 'a list
          Nil         :: 'a list
          comp        :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp#2      :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp#3      :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f#1    :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f#2    :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g    :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g#1  :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          main        :: 'l list -> 'l list
          walk#1      :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                          -> 'l list
                          -> 'l list
                          -> 'l list
          walk#2      :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                          -> 'l list
                          -> 'l list
                          -> 'l list
          walk_xs     :: 'l list -> 'l list
          walk_xs_3   :: 'l -> 'l list -> 'l list
          walk_xs_3#1 :: 'l -> 'l list -> 'l list
    + Applied Processor:
        Inline {inlineType = InlineFull, inlineSelect = <inline decreasing>}
    + Details:
        none
* Step 14: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: walk_xs_3#1(x4, x6) -> Cons(x4, x6)
        2: walk#1(comp(), Nil()) -> walk_xs()
        3: walk#2(comp(), Nil(), x8) -> x8
        4: walk#1(comp(), Cons(x5, x3)) -> comp_f#1(walk#1(comp(), x3), walk_xs_3(x5))
        5: walk#2(comp(), Cons(x5, x3), x6) -> comp_f#2(walk#1(comp(), x3), walk_xs_3(x5), x6)
        6: comp_f_g#1(comp_f_g(x3, x4), walk_xs_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xs_3#1(x2, x1))
        7: comp_f_g#1(walk_xs(), walk_xs_3(x5), x3) -> walk_xs_3#1(x5, x3)
        8: comp_f#1(x2, walk_xs_3(x1)) -> comp_f_g(x2, walk_xs_3(x1))
        9: comp_f#2(x2, walk_xs_3(x1), x3) -> comp_f_g#1(x2, walk_xs_3(x1), x3)
        10: comp#2(x4, walk_xs_3(x2)) -> comp_f_g(x4, walk_xs_3(x2))
        11: comp#3(x4, walk_xs_3(x2), x6) -> comp_f_g#1(x4, walk_xs_3(x2), x6)
        12: main(Nil()) -> Nil()
        13: main(Cons(x4, x2)) -> comp#3(walk#1(comp(), x2), walk_xs_3(x4), Nil())
        where
          Cons        :: 'a -> 'a list -> 'a list
          Nil         :: 'a list
          comp        :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp#2      :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp#3      :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f#1    :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f#2    :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g    :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g#1  :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          main        :: 'l list -> 'l list
          walk#1      :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                          -> 'l list
                          -> 'l list
                          -> 'l list
          walk#2      :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                          -> 'l list
                          -> 'l list
                          -> 'l list
          walk_xs     :: 'l list -> 'l list
          walk_xs_3   :: 'l -> 'l list -> 'l list
          walk_xs_3#1 :: 'l -> 'l list -> 'l list
    + Applied Processor:
        UsableRules {urType = Syntactic}
    + Details:
        none
* Step 15: Inline WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: walk_xs_3#1(x4, x6) -> Cons(x4, x6)
        2: walk#1(comp(), Nil()) -> walk_xs()
        4: walk#1(comp(), Cons(x5, x3)) -> comp_f#1(walk#1(comp(), x3), walk_xs_3(x5))
        6: comp_f_g#1(comp_f_g(x3, x4), walk_xs_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xs_3#1(x2, x1))
        7: comp_f_g#1(walk_xs(), walk_xs_3(x5), x3) -> walk_xs_3#1(x5, x3)
        8: comp_f#1(x2, walk_xs_3(x1)) -> comp_f_g(x2, walk_xs_3(x1))
        11: comp#3(x4, walk_xs_3(x2), x6) -> comp_f_g#1(x4, walk_xs_3(x2), x6)
        12: main(Nil()) -> Nil()
        13: main(Cons(x4, x2)) -> comp#3(walk#1(comp(), x2), walk_xs_3(x4), Nil())
        where
          Cons        :: 'a -> 'a list -> 'a list
          Nil         :: 'a list
          comp        :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp#3      :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f#1    :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g    :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g#1  :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          main        :: 'l list -> 'l list
          walk#1      :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                          -> 'l list
                          -> 'l list
                          -> 'l list
          walk_xs     :: 'l list -> 'l list
          walk_xs_3   :: 'l -> 'l list -> 'l list
          walk_xs_3#1 :: 'l -> 'l list -> 'l list
    + Applied Processor:
        Inline {inlineType = InlineFull, inlineSelect = <inline decreasing>}
    + Details:
        none
* Step 16: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: walk_xs_3#1(x4, x6) -> Cons(x4, x6)
        2: walk#1(comp(), Nil()) -> walk_xs()
        3: walk#1(comp(), Cons(x2, x7)) -> comp_f_g(walk#1(comp(), x7), walk_xs_3(x2))
        4: comp_f_g#1(comp_f_g(x3, x4), walk_xs_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xs_3#1(x2, x1))
        5: comp_f_g#1(walk_xs(), walk_xs_3(x5), x3) -> walk_xs_3#1(x5, x3)
        6: comp_f#1(x2, walk_xs_3(x1)) -> comp_f_g(x2, walk_xs_3(x1))
        7: comp#3(x4, walk_xs_3(x2), x6) -> comp_f_g#1(x4, walk_xs_3(x2), x6)
        8: main(Nil()) -> Nil()
        9: main(Cons(x4, x5)) -> comp_f_g#1(walk#1(comp(), x5), walk_xs_3(x4), Nil())
        where
          Cons        :: 'a -> 'a list -> 'a list
          Nil         :: 'a list
          comp        :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp#3      :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f#1    :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g    :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g#1  :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          main        :: 'l list -> 'l list
          walk#1      :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                          -> 'l list
                          -> 'l list
                          -> 'l list
          walk_xs     :: 'l list -> 'l list
          walk_xs_3   :: 'l -> 'l list -> 'l list
          walk_xs_3#1 :: 'l -> 'l list -> 'l list
    + Applied Processor:
        UsableRules {urType = Syntactic}
    + Details:
        none
* Step 17: Compression WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: walk_xs_3#1(x4, x6) -> Cons(x4, x6)
        2: walk#1(comp(), Nil()) -> walk_xs()
        3: walk#1(comp(), Cons(x2, x7)) -> comp_f_g(walk#1(comp(), x7), walk_xs_3(x2))
        4: comp_f_g#1(comp_f_g(x3, x4), walk_xs_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xs_3#1(x2, x1))
        5: comp_f_g#1(walk_xs(), walk_xs_3(x5), x3) -> walk_xs_3#1(x5, x3)
        8: main(Nil()) -> Nil()
        9: main(Cons(x4, x5)) -> comp_f_g#1(walk#1(comp(), x5), walk_xs_3(x4), Nil())
        where
          Cons        :: 'a -> 'a list -> 'a list
          Nil         :: 'a list
          comp        :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g    :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g#1  :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          main        :: 'l list -> 'l list
          walk#1      :: (('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list)
                          -> 'l list
                          -> 'l list
                          -> 'l list
          walk_xs     :: 'l list -> 'l list
          walk_xs_3   :: 'l -> 'l list -> 'l list
          walk_xs_3#1 :: 'l -> 'l list -> 'l list
    + Applied Processor:
        Compression
    + Details:
        none
* Step 18: ToTctProblem WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: walk_xs_3#1(x4, x6) -> Cons(x4, x6)
        2: walk#1(Nil()) -> walk_xs()
        3: walk#1(Cons(x2, x7)) -> comp_f_g(walk#1(x7), walk_xs_3(x2))
        4: comp_f_g#1(comp_f_g(x3, x4), walk_xs_3(x2), x1) -> comp_f_g#1(x3, x4, walk_xs_3#1(x2, x1))
        5: comp_f_g#1(walk_xs(), walk_xs_3(x5), x3) -> walk_xs_3#1(x5, x3)
        6: main(Nil()) -> Nil()
        7: main(Cons(x4, x5)) -> comp_f_g#1(walk#1(x5), walk_xs_3(x4), Nil())
        where
          Cons        :: 'a -> 'a list -> 'a list
          Nil         :: 'a list
          comp_f_g    :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          comp_f_g#1  :: ('l list -> 'l list) -> ('l list -> 'l list) -> 'l list -> 'l list
          main        :: 'l list -> 'l list
          walk#1      :: 'l list -> 'l list -> 'l list
          walk_xs     :: 'l list -> 'l list
          walk_xs_3   :: 'l -> 'l list -> 'l list
          walk_xs_3#1 :: 'l -> 'l list -> 'l list
    + Applied Processor:
        ToTctProblem
    + Details:
        none
* Step 19: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            comp_f_g#1(comp_f_g(x3,x4),walk_xs_3(x2),x1) -> comp_f_g#1(x3,x4,walk_xs_3#1(x2,x1))
            comp_f_g#1(walk_xs(),walk_xs_3(x5),x3) -> walk_xs_3#1(x5,x3)
            main(Cons(x4,x5)) -> comp_f_g#1(walk#1(x5),walk_xs_3(x4),Nil())
            main(Nil()) -> Nil()
            walk#1(Cons(x2,x7)) -> comp_f_g(walk#1(x7),walk_xs_3(x2))
            walk#1(Nil()) -> walk_xs()
            walk_xs_3#1(x4,x6) -> Cons(x4,x6)
        - Signature:
            {comp_f_g#1/3,main/1,walk#1/1,walk_xs_3#1/2} / {Cons/2,Nil/0,comp_f_g/2,walk_xs/0,walk_xs_3/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil}
    + Applied Processor:
        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}
        
        Following symbols are considered usable:
          {comp_f_g#1,main,walk#1,walk_xs_3#1}
        TcT has computed the following interpretation:
                 p(Cons) = 0              
                  p(Nil) = 1              
             p(comp_f_g) = x1 + x2        
           p(comp_f_g#1) = 2 + 4*x1 + 8*x3
                 p(main) = 14             
               p(walk#1) = 1              
              p(walk_xs) = 0              
            p(walk_xs_3) = 0              
          p(walk_xs_3#1) = 0              
        
        Following rules are strictly oriented:
        comp_f_g#1(walk_xs(),walk_xs_3(x5),x3) = 2 + 8*x3          
                                               > 0                 
                                               = walk_xs_3#1(x5,x3)
        
                                   main(Nil()) = 14                
                                               > 1                 
                                               = Nil()             
        
                                 walk#1(Nil()) = 1                 
                                               > 0                 
                                               = walk_xs()         
        
        
        Following rules are (at-least) weakly oriented:
        comp_f_g#1(comp_f_g(x3,x4),walk_xs_3(x2),x1) =  2 + 8*x1 + 4*x3 + 4*x4                    
                                                     >= 2 + 4*x3                                  
                                                     =  comp_f_g#1(x3,x4,walk_xs_3#1(x2,x1))      
        
                                   main(Cons(x4,x5)) =  14                                        
                                                     >= 14                                        
                                                     =  comp_f_g#1(walk#1(x5),walk_xs_3(x4),Nil())
        
                                 walk#1(Cons(x2,x7)) =  1                                         
                                                     >= 1                                         
                                                     =  comp_f_g(walk#1(x7),walk_xs_3(x2))        
        
                                  walk_xs_3#1(x4,x6) =  0                                         
                                                     >= 0                                         
                                                     =  Cons(x4,x6)                               
        
* Step 20: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            comp_f_g#1(comp_f_g(x3,x4),walk_xs_3(x2),x1) -> comp_f_g#1(x3,x4,walk_xs_3#1(x2,x1))
            main(Cons(x4,x5)) -> comp_f_g#1(walk#1(x5),walk_xs_3(x4),Nil())
            walk#1(Cons(x2,x7)) -> comp_f_g(walk#1(x7),walk_xs_3(x2))
            walk_xs_3#1(x4,x6) -> Cons(x4,x6)
        - Weak TRS:
            comp_f_g#1(walk_xs(),walk_xs_3(x5),x3) -> walk_xs_3#1(x5,x3)
            main(Nil()) -> Nil()
            walk#1(Nil()) -> walk_xs()
        - Signature:
            {comp_f_g#1/3,main/1,walk#1/1,walk_xs_3#1/2} / {Cons/2,Nil/0,comp_f_g/2,walk_xs/0,walk_xs_3/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil}
    + Applied Processor:
        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}
        
        Following symbols are considered usable:
          {comp_f_g#1,main,walk#1,walk_xs_3#1}
        TcT has computed the following interpretation:
                 p(Cons) = 2 + x2         
                  p(Nil) = 1              
             p(comp_f_g) = 2 + x1         
           p(comp_f_g#1) = 1 + 8*x1 + 6*x3
                 p(main) = 4 + 12*x1      
               p(walk#1) = x1             
              p(walk_xs) = 1              
            p(walk_xs_3) = 0              
          p(walk_xs_3#1) = 2 + x2         
        
        Following rules are strictly oriented:
        comp_f_g#1(comp_f_g(x3,x4),walk_xs_3(x2),x1) = 17 + 6*x1 + 8*x3                          
                                                     > 13 + 6*x1 + 8*x3                          
                                                     = comp_f_g#1(x3,x4,walk_xs_3#1(x2,x1))      
        
                                   main(Cons(x4,x5)) = 28 + 12*x5                                
                                                     > 7 + 8*x5                                  
                                                     = comp_f_g#1(walk#1(x5),walk_xs_3(x4),Nil())
        
        
        Following rules are (at-least) weakly oriented:
        comp_f_g#1(walk_xs(),walk_xs_3(x5),x3) =  9 + 6*x3                          
                                               >= 2 + x3                            
                                               =  walk_xs_3#1(x5,x3)                
        
                                   main(Nil()) =  16                                
                                               >= 1                                 
                                               =  Nil()                             
        
                           walk#1(Cons(x2,x7)) =  2 + x7                            
                                               >= 2 + x7                            
                                               =  comp_f_g(walk#1(x7),walk_xs_3(x2))
        
                                 walk#1(Nil()) =  1                                 
                                               >= 1                                 
                                               =  walk_xs()                         
        
                            walk_xs_3#1(x4,x6) =  2 + x6                            
                                               >= 2 + x6                            
                                               =  Cons(x4,x6)                       
        
* Step 21: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            walk#1(Cons(x2,x7)) -> comp_f_g(walk#1(x7),walk_xs_3(x2))
            walk_xs_3#1(x4,x6) -> Cons(x4,x6)
        - Weak TRS:
            comp_f_g#1(comp_f_g(x3,x4),walk_xs_3(x2),x1) -> comp_f_g#1(x3,x4,walk_xs_3#1(x2,x1))
            comp_f_g#1(walk_xs(),walk_xs_3(x5),x3) -> walk_xs_3#1(x5,x3)
            main(Cons(x4,x5)) -> comp_f_g#1(walk#1(x5),walk_xs_3(x4),Nil())
            main(Nil()) -> Nil()
            walk#1(Nil()) -> walk_xs()
        - Signature:
            {comp_f_g#1/3,main/1,walk#1/1,walk_xs_3#1/2} / {Cons/2,Nil/0,comp_f_g/2,walk_xs/0,walk_xs_3/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil}
    + Applied Processor:
        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}
        
        Following symbols are considered usable:
          {comp_f_g#1,main,walk#1,walk_xs_3#1}
        TcT has computed the following interpretation:
                 p(Cons) = [1] x2 + [5]                  
                  p(Nil) = [0]                           
             p(comp_f_g) = [1] x1 + [12] x2 + [2]        
           p(comp_f_g#1) = [1] x1 + [8] x2 + [2] x3 + [8]
                 p(main) = [3] x1 + [9]                  
               p(walk#1) = [3] x1 + [8]                  
              p(walk_xs) = [6]                           
            p(walk_xs_3) = [1]                           
          p(walk_xs_3#1) = [1] x2 + [5]                  
        
        Following rules are strictly oriented:
        walk#1(Cons(x2,x7)) = [3] x7 + [23]                     
                            > [3] x7 + [22]                     
                            = comp_f_g(walk#1(x7),walk_xs_3(x2))
        
        
        Following rules are (at-least) weakly oriented:
        comp_f_g#1(comp_f_g(x3,x4),walk_xs_3(x2),x1) =  [2] x1 + [1] x3 + [12] x4 + [18]          
                                                     >= [2] x1 + [1] x3 + [8] x4 + [18]           
                                                     =  comp_f_g#1(x3,x4,walk_xs_3#1(x2,x1))      
        
              comp_f_g#1(walk_xs(),walk_xs_3(x5),x3) =  [2] x3 + [22]                             
                                                     >= [1] x3 + [5]                              
                                                     =  walk_xs_3#1(x5,x3)                        
        
                                   main(Cons(x4,x5)) =  [3] x5 + [24]                             
                                                     >= [3] x5 + [24]                             
                                                     =  comp_f_g#1(walk#1(x5),walk_xs_3(x4),Nil())
        
                                         main(Nil()) =  [9]                                       
                                                     >= [0]                                       
                                                     =  Nil()                                     
        
                                       walk#1(Nil()) =  [8]                                       
                                                     >= [6]                                       
                                                     =  walk_xs()                                 
        
                                  walk_xs_3#1(x4,x6) =  [1] x6 + [5]                              
                                                     >= [1] x6 + [5]                              
                                                     =  Cons(x4,x6)                               
        
* Step 22: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            walk_xs_3#1(x4,x6) -> Cons(x4,x6)
        - Weak TRS:
            comp_f_g#1(comp_f_g(x3,x4),walk_xs_3(x2),x1) -> comp_f_g#1(x3,x4,walk_xs_3#1(x2,x1))
            comp_f_g#1(walk_xs(),walk_xs_3(x5),x3) -> walk_xs_3#1(x5,x3)
            main(Cons(x4,x5)) -> comp_f_g#1(walk#1(x5),walk_xs_3(x4),Nil())
            main(Nil()) -> Nil()
            walk#1(Cons(x2,x7)) -> comp_f_g(walk#1(x7),walk_xs_3(x2))
            walk#1(Nil()) -> walk_xs()
        - Signature:
            {comp_f_g#1/3,main/1,walk#1/1,walk_xs_3#1/2} / {Cons/2,Nil/0,comp_f_g/2,walk_xs/0,walk_xs_3/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil}
    + Applied Processor:
        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}
        
        Following symbols are considered usable:
          {comp_f_g#1,main,walk#1,walk_xs_3#1}
        TcT has computed the following interpretation:
                 p(Cons) = [1] x2 + [3]         
                  p(Nil) = [2]                  
             p(comp_f_g) = [1] x1 + [2]         
           p(comp_f_g#1) = [8] x1 + [1] x3 + [7]
                 p(main) = [8] x1 + [0]         
               p(walk#1) = [1] x1 + [1]         
              p(walk_xs) = [2]                  
            p(walk_xs_3) = [2]                  
          p(walk_xs_3#1) = [1] x2 + [8]         
        
        Following rules are strictly oriented:
        walk_xs_3#1(x4,x6) = [1] x6 + [8]
                           > [1] x6 + [3]
                           = Cons(x4,x6) 
        
        
        Following rules are (at-least) weakly oriented:
        comp_f_g#1(comp_f_g(x3,x4),walk_xs_3(x2),x1) =  [1] x1 + [8] x3 + [23]                    
                                                     >= [1] x1 + [8] x3 + [15]                    
                                                     =  comp_f_g#1(x3,x4,walk_xs_3#1(x2,x1))      
        
              comp_f_g#1(walk_xs(),walk_xs_3(x5),x3) =  [1] x3 + [23]                             
                                                     >= [1] x3 + [8]                              
                                                     =  walk_xs_3#1(x5,x3)                        
        
                                   main(Cons(x4,x5)) =  [8] x5 + [24]                             
                                                     >= [8] x5 + [17]                             
                                                     =  comp_f_g#1(walk#1(x5),walk_xs_3(x4),Nil())
        
                                         main(Nil()) =  [16]                                      
                                                     >= [2]                                       
                                                     =  Nil()                                     
        
                                 walk#1(Cons(x2,x7)) =  [1] x7 + [4]                              
                                                     >= [1] x7 + [3]                              
                                                     =  comp_f_g(walk#1(x7),walk_xs_3(x2))        
        
                                       walk#1(Nil()) =  [3]                                       
                                                     >= [2]                                       
                                                     =  walk_xs()                                 
        
* Step 23: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            comp_f_g#1(comp_f_g(x3,x4),walk_xs_3(x2),x1) -> comp_f_g#1(x3,x4,walk_xs_3#1(x2,x1))
            comp_f_g#1(walk_xs(),walk_xs_3(x5),x3) -> walk_xs_3#1(x5,x3)
            main(Cons(x4,x5)) -> comp_f_g#1(walk#1(x5),walk_xs_3(x4),Nil())
            main(Nil()) -> Nil()
            walk#1(Cons(x2,x7)) -> comp_f_g(walk#1(x7),walk_xs_3(x2))
            walk#1(Nil()) -> walk_xs()
            walk_xs_3#1(x4,x6) -> Cons(x4,x6)
        - Signature:
            {comp_f_g#1/3,main/1,walk#1/1,walk_xs_3#1/2} / {Cons/2,Nil/0,comp_f_g/2,walk_xs/0,walk_xs_3/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^1))