WORST_CASE(?,O(n^2))
* Step 1: Desugar WORST_CASE(?,O(n^2))
    + Considered Problem:
        type 'a list = Nil | Cons of 'a * 'a list
        ;;
        
        let rec append xs ys = 
          match xs with 
          | Nil -> ys
          | Cons(x,xs') -> Cons(x, append xs' ys) 
        ;;
          
        let rec rev xs =
          match xs with 
          | Nil -> Nil
          | Cons(x,xs') -> append (rev xs') Cons(x,Nil)
        ;;			  
    + Applied Processor:
        Desugar {analysedFunction = Nothing}
    + Details:
        none
* Step 2: Defunctionalization WORST_CASE(?,O(n^2))
    + Considered Problem:
        λxs : 'a8 list.
          (λappend : 'a8 list -> 'a8 list -> 'a8 list.
             (λrev : 'a8 list -> 'a8 list. rev xs)
               (μrev : 'a8 list -> 'a8 list.
                  λxs : 'a8 list.
                    case xs of  | Nil -> Nil | Cons -> λx : 'a8. λxs' : 'a8 list. append (rev xs') Cons(x,Nil)))
            (μappend : 'a8 list -> 'a8 list -> 'a8 list.
               λxs : 'a8 list.
                 λys : 'a8 list.
                   case xs of  | Nil -> ys | Cons -> λx : 'a8. λxs' : 'a8 list. Cons(x,append xs' ys)) : 'a8 list
                                                                                                          -> 'a8 list
        where
          Cons :: 'a -> 'a list -> 'a list
          Nil  :: 'a list
    + Applied Processor:
        Defunctionalization
    + Details:
        none
* Step 3: Inline WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: main_2(x0) x2 -> x2 x0
        2: cond_rev_xs(Nil(), x1) -> Nil()
        3: cond_rev_xs(Cons(x3, x4), x1) -> x1 (rev(x1) x4) Cons(x3, Nil())
        4: rev_1(x1) x2 -> cond_rev_xs(x2, x1)
        5: rev(x1) x2 -> rev_1(x1) x2
        6: main_1(x0) x1 -> main_2(x0) rev(x1)
        7: cond_append_xs_ys(Nil(), x2) -> x2
        8: cond_append_xs_ys(Cons(x3, x4), x2) -> Cons(x3, append() x4 x2)
        9: append_xs(x1) x2 -> cond_append_xs_ys(x1, x2)
        10: append_1() x1 -> append_xs(x1)
        11: append() x0 -> append_1() x0
        12: main(x0) -> main_1(x0) append()
        where
          Cons              :: 'a -> 'a list -> 'a list
          Nil               :: 'a list
          append_xs         :: 'a8 list -> 'a8 list -> 'a8 list
          append_1          :: 'a8 list -> 'a8 list -> 'a8 list
          main_1            :: 'a8 list -> ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list
          rev_1             :: ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list -> 'a8 list
          main_2            :: 'a8 list -> ('a8 list -> 'a8 list) -> 'a8 list
          cond_rev_xs       :: 'a8 list -> ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list
          cond_append_xs_ys :: 'a8 list -> 'a8 list -> 'a8 list
          append            :: 'a8 list -> 'a8 list -> 'a8 list
          rev               :: ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list -> 'a8 list
          main              :: 'a8 list -> 'a8 list
    + Applied Processor:
        Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
    + Details:
        none
* Step 4: Inline WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: main_2(x0) x2 -> x2 x0
        2: cond_rev_xs(Nil(), x1) -> Nil()
        3: cond_rev_xs(Cons(x3, x4), x1) -> x1 (rev(x1) x4) Cons(x3, Nil())
        4: rev_1(x1) x2 -> cond_rev_xs(x2, x1)
        5: rev(x2) x4 -> cond_rev_xs(x4, x2)
        6: main_1(x0) x3 -> rev(x3) x0
        7: cond_append_xs_ys(Nil(), x2) -> x2
        8: cond_append_xs_ys(Cons(x3, x4), x2) -> Cons(x3, append() x4 x2)
        9: append_xs(x1) x2 -> cond_append_xs_ys(x1, x2)
        10: append_1() x1 -> append_xs(x1)
        11: append() x2 -> append_xs(x2)
        12: main(x0) -> main_2(x0) rev(append())
        where
          Cons              :: 'a -> 'a list -> 'a list
          Nil               :: 'a list
          append_xs         :: 'a8 list -> 'a8 list -> 'a8 list
          append_1          :: 'a8 list -> 'a8 list -> 'a8 list
          main_1            :: 'a8 list -> ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list
          rev_1             :: ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list -> 'a8 list
          main_2            :: 'a8 list -> ('a8 list -> 'a8 list) -> 'a8 list
          cond_rev_xs       :: 'a8 list -> ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list
          cond_append_xs_ys :: 'a8 list -> 'a8 list -> 'a8 list
          append            :: 'a8 list -> 'a8 list -> 'a8 list
          rev               :: ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list -> 'a8 list
          main              :: 'a8 list -> 'a8 list
    + Applied Processor:
        Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
    + Details:
        none
* Step 5: Inline WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: main_2(x0) x2 -> x2 x0
        2: cond_rev_xs(Nil(), x1) -> Nil()
        3: cond_rev_xs(Cons(x3, x4), x1) -> x1 (rev(x1) x4) Cons(x3, Nil())
        4: rev_1(x1) x2 -> cond_rev_xs(x2, x1)
        5: rev(x2) x4 -> cond_rev_xs(x4, x2)
        6: main_1(x0) x3 -> rev(x3) x0
        7: cond_append_xs_ys(Nil(), x2) -> x2
        8: cond_append_xs_ys(Cons(x3, x4), x2) -> Cons(x3, append() x4 x2)
        9: append_xs(x1) x2 -> cond_append_xs_ys(x1, x2)
        10: append_1() x1 -> append_xs(x1)
        11: append() x2 -> append_xs(x2)
        12: main(x0) -> rev(append()) x0
        where
          Cons              :: 'a -> 'a list -> 'a list
          Nil               :: 'a list
          append_xs         :: 'a8 list -> 'a8 list -> 'a8 list
          append_1          :: 'a8 list -> 'a8 list -> 'a8 list
          main_1            :: 'a8 list -> ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list
          rev_1             :: ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list -> 'a8 list
          main_2            :: 'a8 list -> ('a8 list -> 'a8 list) -> 'a8 list
          cond_rev_xs       :: 'a8 list -> ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list
          cond_append_xs_ys :: 'a8 list -> 'a8 list -> 'a8 list
          append            :: 'a8 list -> 'a8 list -> 'a8 list
          rev               :: ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list -> 'a8 list
          main              :: 'a8 list -> 'a8 list
    + Applied Processor:
        Inline {inlineType = InlineFull, inlineSelect = <inline case-expression>}
    + Details:
        none
* Step 6: UsableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: main_2(x0) x2 -> x2 x0
        2: cond_rev_xs(Nil(), x1) -> Nil()
        3: cond_rev_xs(Cons(x3, x4), x1) -> x1 (rev(x1) x4) Cons(x3, Nil())
        4: rev_1(x2) Nil() -> Nil()
        5: rev_1(x2) Cons(x6, x8) -> x2 (rev(x2) x8) Cons(x6, Nil())
        6: rev(x2) Nil() -> Nil()
        7: rev(x2) Cons(x6, x8) -> x2 (rev(x2) x8) Cons(x6, Nil())
        8: main_1(x0) x3 -> rev(x3) x0
        9: cond_append_xs_ys(Nil(), x2) -> x2
        10: cond_append_xs_ys(Cons(x3, x4), x2) -> Cons(x3, append() x4 x2)
        11: append_xs(Nil()) x4 -> x4
        12: append_xs(Cons(x6, x8)) x4 -> Cons(x6, append() x8 x4)
        13: append_1() x1 -> append_xs(x1)
        14: append() x2 -> append_xs(x2)
        15: main(x0) -> rev(append()) x0
        where
          Cons              :: 'a -> 'a list -> 'a list
          Nil               :: 'a list
          append_xs         :: 'a8 list -> 'a8 list -> 'a8 list
          append_1          :: 'a8 list -> 'a8 list -> 'a8 list
          main_1            :: 'a8 list -> ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list
          rev_1             :: ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list -> 'a8 list
          main_2            :: 'a8 list -> ('a8 list -> 'a8 list) -> 'a8 list
          cond_rev_xs       :: 'a8 list -> ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list
          cond_append_xs_ys :: 'a8 list -> 'a8 list -> 'a8 list
          append            :: 'a8 list -> 'a8 list -> 'a8 list
          rev               :: ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list -> 'a8 list
          main              :: 'a8 list -> 'a8 list
    + Applied Processor:
        UsableRules {urType = Syntactic}
    + Details:
        none
* Step 7: NeededRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: main_2(x0) x2 -> x2 x0
        4: rev_1(x2) Nil() -> Nil()
        5: rev_1(x2) Cons(x6, x8) -> x2 (rev(x2) x8) Cons(x6, Nil())
        6: rev(x2) Nil() -> Nil()
        7: rev(x2) Cons(x6, x8) -> x2 (rev(x2) x8) Cons(x6, Nil())
        8: main_1(x0) x3 -> rev(x3) x0
        11: append_xs(Nil()) x4 -> x4
        12: append_xs(Cons(x6, x8)) x4 -> Cons(x6, append() x8 x4)
        13: append_1() x1 -> append_xs(x1)
        14: append() x2 -> append_xs(x2)
        15: main(x0) -> rev(append()) x0
        where
          Cons      :: 'a -> 'a list -> 'a list
          Nil       :: 'a list
          append_xs :: 'a8 list -> 'a8 list -> 'a8 list
          append_1  :: 'a8 list -> 'a8 list -> 'a8 list
          main_1    :: 'a8 list -> ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list
          rev_1     :: ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list -> 'a8 list
          main_2    :: 'a8 list -> ('a8 list -> 'a8 list) -> 'a8 list
          append    :: 'a8 list -> 'a8 list -> 'a8 list
          rev       :: ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list -> 'a8 list
          main      :: 'a8 list -> 'a8 list
    + Applied Processor:
        NeededRules
    + Details:
        none
* Step 8: CFA WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: main_2(x0) x2 -> x2 x0
        2: rev_1(x2) Nil() -> Nil()
        3: rev_1(x2) Cons(x6, x8) -> x2 (rev(x2) x8) Cons(x6, Nil())
        4: rev(x2) Nil() -> Nil()
        5: rev(x2) Cons(x6, x8) -> x2 (rev(x2) x8) Cons(x6, Nil())
        6: main_1(x0) x3 -> rev(x3) x0
        7: append_xs(Nil()) x4 -> x4
        8: append_xs(Cons(x6, x8)) x4 -> Cons(x6, append() x8 x4)
        9: append_1() x1 -> append_xs(x1)
        10: append() x2 -> append_xs(x2)
        11: main(x0) -> rev(append()) x0
        where
          Cons      :: 'a -> 'a list -> 'a list
          Nil       :: 'a list
          append_xs :: 'a8 list -> 'a8 list -> 'a8 list
          append_1  :: 'a8 list -> 'a8 list -> 'a8 list
          main_1    :: 'a8 list -> ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list
          rev_1     :: ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list -> 'a8 list
          main_2    :: 'a8 list -> ('a8 list -> 'a8 list) -> 'a8 list
          append    :: 'a8 list -> 'a8 list -> 'a8 list
          rev       :: ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list -> 'a8 list
          main      :: 'a8 list -> 'a8 list
    + Applied Processor:
        CFA {cfaRefinement = <control flow analysis>}
    + Details:
        {X{*} -> Cons(X{*},X{*})
              |  Cons(X{*},X{*})
              |  Nil()
              |  Nil()
              |  Cons(X{*},X{*})
              |  Cons(X{*},X{*})
              |  Nil()
              |  Nil()
              |  Nil()
              |  Cons(X{*},X{*})
              |  Cons(X{*},X{*})
              |  Nil()
              |  Nil()
        ,V{x0_11} -> X{*}
        ,V{x2_4} -> V{x2_5}
                 |  append()
        ,V{x2_5} -> V{x2_5}
                 |  append()
        ,V{x2_10} -> V{x8_8}
                  |  R{5}
                  |  R{4}
        ,V{x4_7} -> V{x4_8}
                 |  Cons(V{x6_5},Nil())
        ,V{x4_8} -> V{x4_8}
                 |  Cons(V{x6_5},Nil())
        ,V{x6_5} -> X{*}
        ,V{x6_8} -> V{x6_8}
                 |  V{x6_5}
        ,V{x8_5} -> X{*}
        ,V{x8_8} -> R{8}
                 |  R{7}
                 |  @(R{10},V{x4_8})
                 |  @(@(append(),V{x8_8}),V{x4_8})
                 |  Nil()
        ,R{0} -> R{11}
              |  main(X{*})
        ,R{4} -> Nil()
        ,R{5} -> R{8}
              |  R{7}
              |  @(R{10},Cons(V{x6_5},Nil()))
              |  @(@(V{x2_5},R{5}),Cons(V{x6_5},Nil()))
              |  @(@(V{x2_5},R{4}),Cons(V{x6_5},Nil()))
              |  @(@(V{x2_5},@(rev(V{x2_5}),V{x8_5})),Cons(V{x6_5},Nil()))
        ,R{7} -> V{x4_7}
        ,R{8} -> Cons(V{x6_8},R{8})
              |  Cons(V{x6_8},R{7})
              |  Cons(V{x6_8},@(R{10},V{x4_8}))
              |  Cons(V{x6_8},@(@(append(),V{x8_8}),V{x4_8}))
        ,R{10} -> append_xs(V{x2_10})
        ,R{11} -> R{5}
               |  R{4}
               |  @(rev(append()),V{x0_11})}
* Step 9: UncurryATRS WORST_CASE(?,O(n^2))
    + Considered Problem:
        4: rev(append()) Nil() -> Nil()
        5: rev(append()) Cons(x2, x1) -> append() (rev(append()) x1) Cons(x2, Nil())
        7: append_xs(Nil()) Cons(x1, Nil()) -> Cons(x1, Nil())
        8: append_xs(Cons(x3, x2)) Cons(x1, Nil()) -> Cons(x3, append() x2 Cons(x1, Nil()))
        10: append() x2 -> append_xs(x2)
        11: main(x0) -> rev(append()) x0
        where
          Cons      :: 'a -> 'a list -> 'a list
          Nil       :: 'a list
          append_xs :: 'a8 list -> 'a8 list -> 'a8 list
          append    :: 'a8 list -> 'a8 list -> 'a8 list
          rev       :: ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list -> 'a8 list
          main      :: 'a8 list -> 'a8 list
    + Applied Processor:
        UncurryATRS
    + Details:
        none
* Step 10: UsableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: rev#1(append(), Nil()) -> Nil()
        2: rev#1(append(), Cons(x2, x1)) -> append#2(rev#1(append(), x1), Cons(x2, Nil()))
        3: append_xs#1(Nil(), Cons(x1, Nil())) -> Cons(x1, Nil())
        4: append_xs#1(Cons(x3, x2), Cons(x1, Nil())) -> Cons(x3, append#2(x2, Cons(x1, Nil())))
        5: append#1(x2) -> append_xs(x2)
        6: append#2(x2, x3) -> append_xs#1(x2, x3)
        7: main(x0) -> rev#1(append(), x0)
        where
          Cons        :: 'a -> 'a list -> 'a list
          Nil         :: 'a list
          append      :: 'a8 list -> 'a8 list -> 'a8 list
          append#1    :: 'a8 list -> 'a8 list -> 'a8 list
          append#2    :: 'a8 list -> 'a8 list -> 'a8 list
          append_xs   :: 'a8 list -> 'a8 list -> 'a8 list
          append_xs#1 :: 'a8 list -> 'a8 list -> 'a8 list
          main        :: 'a8 list -> 'a8 list
          rev#1       :: ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list -> 'a8 list
    + Applied Processor:
        UsableRules {urType = DFA}
    + Details:
        none
* Step 11: Inline WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: rev#1(append(), Nil()) -> Nil()
        2: rev#1(append(), Cons(x2, x1)) -> append#2(rev#1(append(), x1), Cons(x2, Nil()))
        3: append_xs#1(Nil(), Cons(x1, Nil())) -> Cons(x1, Nil())
        4: append_xs#1(Cons(x3, x2), Cons(x1, Nil())) -> Cons(x3, append#2(x2, Cons(x1, Nil())))
        6: append#2(x2, x3) -> append_xs#1(x2, x3)
        7: main(x0) -> rev#1(append(), x0)
        where
          Cons        :: 'a -> 'a list -> 'a list
          Nil         :: 'a list
          append      :: 'a8 list -> 'a8 list -> 'a8 list
          append#2    :: 'a8 list -> 'a8 list -> 'a8 list
          append_xs#1 :: 'a8 list -> 'a8 list -> 'a8 list
          main        :: 'a8 list -> 'a8 list
          rev#1       :: ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list -> 'a8 list
    + Applied Processor:
        Inline {inlineType = InlineFull, inlineSelect = <inline decreasing>}
    + Details:
        none
* Step 12: UsableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: rev#1(append(), Nil()) -> Nil()
        2: rev#1(append(), Cons(x2, x1)) -> append#2(rev#1(append(), x1), Cons(x2, Nil()))
        3: append_xs#1(Nil(), Cons(x1, Nil())) -> Cons(x1, Nil())
        4: append_xs#1(Cons(x3, x2), Cons(x1, Nil())) -> Cons(x3, append#2(x2, Cons(x1, Nil())))
        5: append#2(Nil(), Cons(x2, Nil())) -> Cons(x2, Nil())
        6: append#2(Cons(x6, x4), Cons(x2, Nil())) -> Cons(x6, append#2(x4, Cons(x2, Nil())))
        7: main(x0) -> rev#1(append(), x0)
        where
          Cons        :: 'a -> 'a list -> 'a list
          Nil         :: 'a list
          append      :: 'a8 list -> 'a8 list -> 'a8 list
          append#2    :: 'a8 list -> 'a8 list -> 'a8 list
          append_xs#1 :: 'a8 list -> 'a8 list -> 'a8 list
          main        :: 'a8 list -> 'a8 list
          rev#1       :: ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list -> 'a8 list
    + Applied Processor:
        UsableRules {urType = Syntactic}
    + Details:
        none
* Step 13: Compression WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: rev#1(append(), Nil()) -> Nil()
        2: rev#1(append(), Cons(x2, x1)) -> append#2(rev#1(append(), x1), Cons(x2, Nil()))
        5: append#2(Nil(), Cons(x2, Nil())) -> Cons(x2, Nil())
        6: append#2(Cons(x6, x4), Cons(x2, Nil())) -> Cons(x6, append#2(x4, Cons(x2, Nil())))
        7: main(x0) -> rev#1(append(), x0)
        where
          Cons     :: 'a -> 'a list -> 'a list
          Nil      :: 'a list
          append   :: 'a8 list -> 'a8 list -> 'a8 list
          append#2 :: 'a8 list -> 'a8 list -> 'a8 list
          main     :: 'a8 list -> 'a8 list
          rev#1    :: ('a8 list -> 'a8 list -> 'a8 list) -> 'a8 list -> 'a8 list
    + Applied Processor:
        Compression
    + Details:
        none
* Step 14: ToTctProblem WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: rev#1(Nil()) -> Nil()
        2: rev#1(Cons(x2, x1)) -> append#2(rev#1(x1), Cons(x2, Nil()))
        3: append#2(Nil(), Cons(x2, Nil())) -> Cons(x2, Nil())
        4: append#2(Cons(x6, x4), Cons(x2, Nil())) -> Cons(x6, append#2(x4, Cons(x2, Nil())))
        5: main(x0) -> rev#1(x0)
        where
          Cons     :: 'a -> 'a list -> 'a list
          Nil      :: 'a list
          append#2 :: 'a8 list -> 'a8 list -> 'a8 list
          main     :: 'a8 list -> 'a8 list
          rev#1    :: 'a8 list -> 'a8 list
    + Applied Processor:
        ToTctProblem
    + Details:
        none
* Step 15: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            append#2(Cons(x6,x4),Cons(x2,Nil())) -> Cons(x6,append#2(x4,Cons(x2,Nil())))
            append#2(Nil(),Cons(x2,Nil())) -> Cons(x2,Nil())
            main(x0) -> rev#1(x0)
            rev#1(Cons(x2,x1)) -> append#2(rev#1(x1),Cons(x2,Nil()))
            rev#1(Nil()) -> Nil()
        - Signature:
            {append#2/2,main/1,rev#1/1} / {Cons/2,Nil/0}
        - 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(Cons) = {2},
          uargs(append#2) = {1}
        
        Following symbols are considered usable:
          {append#2,main,rev#1}
        TcT has computed the following interpretation:
              p(Cons) = [1] x2 + [0]         
               p(Nil) = [0]                  
          p(append#2) = [8] x1 + [1] x2 + [0]
              p(main) = [2]                  
             p(rev#1) = [0]                  
        
        Following rules are strictly oriented:
        main(x0) = [2]      
                 > [0]      
                 = rev#1(x0)
        
        
        Following rules are (at-least) weakly oriented:
        append#2(Cons(x6,x4),Cons(x2,Nil())) =  [8] x4 + [0]                        
                                             >= [8] x4 + [0]                        
                                             =  Cons(x6,append#2(x4,Cons(x2,Nil())))
        
              append#2(Nil(),Cons(x2,Nil())) =  [0]                                 
                                             >= [0]                                 
                                             =  Cons(x2,Nil())                      
        
                          rev#1(Cons(x2,x1)) =  [0]                                 
                                             >= [0]                                 
                                             =  append#2(rev#1(x1),Cons(x2,Nil()))  
        
                                rev#1(Nil()) =  [0]                                 
                                             >= [0]                                 
                                             =  Nil()                               
        
* Step 16: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            append#2(Cons(x6,x4),Cons(x2,Nil())) -> Cons(x6,append#2(x4,Cons(x2,Nil())))
            append#2(Nil(),Cons(x2,Nil())) -> Cons(x2,Nil())
            rev#1(Cons(x2,x1)) -> append#2(rev#1(x1),Cons(x2,Nil()))
            rev#1(Nil()) -> Nil()
        - Weak TRS:
            main(x0) -> rev#1(x0)
        - Signature:
            {append#2/2,main/1,rev#1/1} / {Cons/2,Nil/0}
        - 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(Cons) = {2},
          uargs(append#2) = {1}
        
        Following symbols are considered usable:
          {append#2,main,rev#1}
        TcT has computed the following interpretation:
              p(Cons) = x2
               p(Nil) = 1 
          p(append#2) = x1
              p(main) = 9 
             p(rev#1) = 2 
        
        Following rules are strictly oriented:
        rev#1(Nil()) = 2    
                     > 1    
                     = Nil()
        
        
        Following rules are (at-least) weakly oriented:
        append#2(Cons(x6,x4),Cons(x2,Nil())) =  x4                                  
                                             >= x4                                  
                                             =  Cons(x6,append#2(x4,Cons(x2,Nil())))
        
              append#2(Nil(),Cons(x2,Nil())) =  1                                   
                                             >= 1                                   
                                             =  Cons(x2,Nil())                      
        
                                    main(x0) =  9                                   
                                             >= 2                                   
                                             =  rev#1(x0)                           
        
                          rev#1(Cons(x2,x1)) =  2                                   
                                             >= 2                                   
                                             =  append#2(rev#1(x1),Cons(x2,Nil()))  
        
* Step 17: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            append#2(Cons(x6,x4),Cons(x2,Nil())) -> Cons(x6,append#2(x4,Cons(x2,Nil())))
            append#2(Nil(),Cons(x2,Nil())) -> Cons(x2,Nil())
            rev#1(Cons(x2,x1)) -> append#2(rev#1(x1),Cons(x2,Nil()))
        - Weak TRS:
            main(x0) -> rev#1(x0)
            rev#1(Nil()) -> Nil()
        - Signature:
            {append#2/2,main/1,rev#1/1} / {Cons/2,Nil/0}
        - 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(Cons) = {2},
          uargs(append#2) = {1}
        
        Following symbols are considered usable:
          {append#2,main,rev#1}
        TcT has computed the following interpretation:
              p(Cons) = 12 + x2  
               p(Nil) = 5        
          p(append#2) = x1 + x2  
              p(main) = 9 + 12*x1
             p(rev#1) = 6 + 2*x1 
        
        Following rules are strictly oriented:
        append#2(Nil(),Cons(x2,Nil())) = 22                                
                                       > 17                                
                                       = Cons(x2,Nil())                    
        
                    rev#1(Cons(x2,x1)) = 30 + 2*x1                         
                                       > 23 + 2*x1                         
                                       = append#2(rev#1(x1),Cons(x2,Nil()))
        
        
        Following rules are (at-least) weakly oriented:
        append#2(Cons(x6,x4),Cons(x2,Nil())) =  29 + x4                             
                                             >= 29 + x4                             
                                             =  Cons(x6,append#2(x4,Cons(x2,Nil())))
        
                                    main(x0) =  9 + 12*x0                           
                                             >= 6 + 2*x0                            
                                             =  rev#1(x0)                           
        
                                rev#1(Nil()) =  16                                  
                                             >= 5                                   
                                             =  Nil()                               
        
* Step 18: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            append#2(Cons(x6,x4),Cons(x2,Nil())) -> Cons(x6,append#2(x4,Cons(x2,Nil())))
        - Weak TRS:
            append#2(Nil(),Cons(x2,Nil())) -> Cons(x2,Nil())
            main(x0) -> rev#1(x0)
            rev#1(Cons(x2,x1)) -> append#2(rev#1(x1),Cons(x2,Nil()))
            rev#1(Nil()) -> Nil()
        - Signature:
            {append#2/2,main/1,rev#1/1} / {Cons/2,Nil/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil}
    + Applied Processor:
        NaturalMI {miDimension = 3, miDegree = 3, 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(Cons) = {2},
          uargs(append#2) = {1}
        
        Following symbols are considered usable:
          {append#2,main,rev#1}
        TcT has computed the following interpretation:
              p(Cons) = [1 1 0]      [0]             
                        [0 1 0] x2 + [1]             
                        [0 0 0]      [2]             
               p(Nil) = [0]                          
                        [1]                          
                        [0]                          
          p(append#2) = [1 2 0]      [0 0 0]      [0]
                        [0 1 0] x1 + [0 0 0] x2 + [1]
                        [0 0 0]      [0 2 0]      [2]
              p(main) = [3 2 0]      [0]             
                        [0 1 2] x1 + [1]             
                        [2 3 2]      [1]             
             p(rev#1) = [2 0 0]      [0]             
                        [0 1 0] x1 + [0]             
                        [2 2 2]      [0]             
        
        Following rules are strictly oriented:
        append#2(Cons(x6,x4),Cons(x2,Nil())) = [1 3 0]      [2]                    
                                               [0 1 0] x4 + [2]                    
                                               [0 0 0]      [6]                    
                                             > [1 3 0]      [1]                    
                                               [0 1 0] x4 + [2]                    
                                               [0 0 0]      [2]                    
                                             = Cons(x6,append#2(x4,Cons(x2,Nil())))
        
        
        Following rules are (at-least) weakly oriented:
        append#2(Nil(),Cons(x2,Nil())) =  [2]                               
                                          [2]                               
                                          [6]                               
                                       >= [1]                               
                                          [2]                               
                                          [2]                               
                                       =  Cons(x2,Nil())                    
        
                              main(x0) =  [3 2 0]      [0]                  
                                          [0 1 2] x0 + [1]                  
                                          [2 3 2]      [1]                  
                                       >= [2 0 0]      [0]                  
                                          [0 1 0] x0 + [0]                  
                                          [2 2 2]      [0]                  
                                       =  rev#1(x0)                         
        
                    rev#1(Cons(x2,x1)) =  [2 2 0]      [0]                  
                                          [0 1 0] x1 + [1]                  
                                          [2 4 0]      [6]                  
                                       >= [2 2 0]      [0]                  
                                          [0 1 0] x1 + [1]                  
                                          [0 0 0]      [6]                  
                                       =  append#2(rev#1(x1),Cons(x2,Nil()))
        
                          rev#1(Nil()) =  [0]                               
                                          [1]                               
                                          [2]                               
                                       >= [0]                               
                                          [1]                               
                                          [0]                               
                                       =  Nil()                             
        
* Step 19: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            append#2(Cons(x6,x4),Cons(x2,Nil())) -> Cons(x6,append#2(x4,Cons(x2,Nil())))
            append#2(Nil(),Cons(x2,Nil())) -> Cons(x2,Nil())
            main(x0) -> rev#1(x0)
            rev#1(Cons(x2,x1)) -> append#2(rev#1(x1),Cons(x2,Nil()))
            rev#1(Nil()) -> Nil()
        - Signature:
            {append#2/2,main/1,rev#1/1} / {Cons/2,Nil/0}
        - 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^2))