WORST_CASE(?,O(n^3))
* Step 1: Desugar WORST_CASE(?,O(n^3))
    + 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
        
        (* * * * * * * * * * *
         * Resource Aware ML *
         * * * * * * * * * * *
         *
         * * *  Use Cases  * *
         *
         * File:
         *   examples/running.raml
         *
         * Author:
         *   Jan Hoffmann (S(S(0))015)
         *
         * Description:
         *   Running example in the S(S(0))015 TR.
         *
         *)
        ;;
        type Exception = Not_found | Inv_arg
        
        ;;
        let rec append l1 l2 =
          match l1 with
            | Nil()-> l2
            | Cons(x,xs) -> Cons(x,(append xs l2))
        
        ;;
        let rec partition f l =
          match l with
            | Nil()-> Pair(Nil,Nil)
            | Cons(x,xs) ->
               (match partition f xs with
               | Pair(cs,bs) -> ite (f x) Pair(cs,Cons(x,bs)) Pair(Cons(x,cs),bs))
        
        ;;
        let rec quicksort gt xyz = match xyz with
          | Nil()-> Nil
          | Cons(x,xs) ->
             (match partition (gt x) xs with
              | Pair(ys, zs) -> append (quicksort gt ys) (Cons(x,(quicksort gt zs))))
        
        ;;
        type ('a,'b) ablist =
            Acons of 'a * ('a,'b) ablist
          | Bcons of 'b * ('a,'b) ablist
          | Nil
        ;;
        let rec abmap f g abs =
          match abs with
          | Acons(a,abs') -> Acons(f a, abmap f g abs')
          | Bcons(b,abs') -> Bcons(g b, abmap f g abs')
          | Nil()-> Nil
        ;;
        let asort gt abs =
          abmap (quicksort gt) (fun x -> x) abs
        ;;
        let asort' gt abs =
          abmap (quicksort gt) (fun unused -> error Inv_arg) abs
        ;;
        let btick = abmap (fun a -> a) (fun b ->  b)
        ;;
        let rec abfoldr f g acc abs =
          match abs with
          | Acons(a,abs') ->
             let acc' = abfoldr f g acc abs' in
             f a acc'
          | Bcons(b,abs') ->
             let acc' = abfoldr f g acc abs' in
             g b acc'
          | Nil()->
             acc
        ;;
        let cons_all abs =
          let f x y =
            let fa = fun x acc -> error Not_found in
            let fb = fun b acc -> Bcons(plus b x,acc) in
            abfoldr fa fb Nil y
          in
          let g x y = Bcons (x,y) in
          abfoldr f g Nil abs
        ;;
        (* let abs = Acons ((Cons(S(0),Cons(S(S(0)),Nil))),Bcons (S(S(S(0))), Bcons (S(S(S(S(0)))), Nil)))
         * ;; *)
        (* let e1 () = asort  (>) (Acons ((Cons(S(0),Cons(S(S(0)),Nil))),Bcons (0, Acons ((Cons(S(S(S(0))),Cons(S(S(S(S(0)))),Nil))), Nil))))
         * let e2 () = asort' (>) (Acons ((Cons(S(0),Cons(S(S(0)),Nil))),Bcons (0, Acons ((Cons(S(S(S(0))),Cons(S(S(S(S(0)))),Nil))), Nil))))
         * let e3 () = btick (Acons ((Cons(S(0),Cons(S(S(0)),Nil))),Bcons (0, Acons ((Cons(S(S(S(0))),Cons(S(S(S(S(0)))),Nil))), Nil))))
         *
         *
         * ;;
         * let abs = Acons (S(0)00, Bcons (S(S(0)), Bcons (S(S(S(0))), Acons(S(S(S(S(0)))),Nil)))) *)
        
        
        let main abs = cons_all abs
        
        
        ;;
    + Applied Processor:
        Desugar {analysedFunction = Nothing}
    + Details:
        none
* Step 2: Defunctionalization WORST_CASE(?,O(n^3))
    + Considered Problem:
        λabs : (nat,nat) ablist.
          (λplus : nat -> nat -> nat.
             (λabfoldr : (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                          -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                          -> (nat,nat) ablist
                          -> (nat,nat) ablist
                          -> (nat,nat) ablist.
                (λcons_all : (nat,nat) ablist -> (nat,nat) ablist.
                   (λmain : (nat,nat) ablist -> (nat,nat) ablist. main abs) (λabs : (nat,nat) ablist. cons_all abs))
                  (λabs : (nat,nat) ablist.
                     (λf : nat -> (nat,nat) ablist -> (nat,nat) ablist.
                        (λg : nat -> (nat,nat) ablist -> (nat,nat) ablist. abfoldr f g Nil abs)
                          (λx : nat. λy : (nat,nat) ablist. Bcons(x,y)))
                       (λx : nat.
                          λy : (nat,nat) ablist.
                            (λfa : nat -> (nat,nat) ablist -> (nat,nat) ablist.
                               (λfb : nat -> (nat,nat) ablist -> (nat,nat) ablist. abfoldr fa fb Nil y)
                                 (λb : nat. λacc : (nat,nat) ablist. Bcons(plus b x,acc)))
                              (λx : nat. λacc : (nat,nat) ablist. ⟘  Not_found))))
               (μabfoldr : (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                            -> (nat,nat) ablist
                            -> (nat,nat) ablist
                            -> (nat,nat) ablist.
                  λf : nat -> (nat,nat) ablist -> (nat,nat) ablist.
                    λg : nat -> (nat,nat) ablist -> (nat,nat) ablist.
                      λacc : (nat,nat) ablist.
                        λabs : (nat,nat) ablist.
                          case abs of
                           | Acons -> λa : nat.
                                        λabs' : (nat,nat) ablist.
                                          (λacc' : (nat,nat) ablist. f a acc') (abfoldr f g acc abs')
                           | Bcons -> λb : nat.
                                        λabs' : (nat,nat) ablist.
                                          (λacc' : (nat,nat) ablist. g b acc') (abfoldr f g acc abs')
                           | Nil -> acc))
            (μplus : nat -> nat -> nat. λn : nat. λm : nat. case m of  | 0 -> n | S -> λx : nat. S(plus n x)) : (nat
                                                                                                                 ,nat) ablist
                                                                                                                 -> (nat
                                                                                                                     ,nat) ablist
        where
          0         :: nat
          Acons     :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons     :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Cons      :: 'a -> 'a list -> 'a list
          False     :: bool
          Inv_arg   :: Exception
          Nil       :: ('a,'b) ablist
          None      :: 'a option
          Not_found :: Exception
          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^3))
    + Considered Problem:
        1: main_4(x0) x4 -> x4 x0
        2: main_5(x3) x4 -> x3 x4
        3: main_3(x0) x3 -> main_4(x0) main_5(x3)
        4: cons_all_abs_1(x2, x3, x4) x5 -> x2 x4 x5 Nil() x3
        5: g_x(x5) x6 -> Bcons(x5, x6)
        6: g() x5 -> g_x(x5)
        7: cons_all_abs(x2, x3) x4 -> cons_all_abs_1(x2, x3, x4) g()
        8: f_x_y_1(x2, x5, x6) x7 -> x2 x6 x7 Nil() x5
        9: fb_1(x1, x4, x7) x8 -> Bcons(x1 x7 x4, x8)
        10: fb(x1, x4) x7 -> fb_1(x1, x4, x7)
        11: f_x_y(x1, x2, x4, x5) x6 -> f_x_y_1(x2, x5, x6) fb(x1, x4)
        12: fa_1() x7 -> bot[0]() Not_found()
        13: fa() x6 -> fa_1()
        14: f_x(x1, x2, x4) x5 -> f_x_y(x1, x2, x4, x5) fa()
        15: f(x1, x2) x4 -> f_x(x1, x2, x4)
        16: cons_all(x1, x2) x3 -> cons_all_abs(x2, x3) f(x1, x2)
        17: main_2(x0, x1) x2 -> main_3(x0) cons_all(x1, x2)
        18: abfoldr_f_g_acc_abs_2(x2, x6) x8 -> x2 x6 x8
        19: abfoldr_f_g_acc_abs_5(x3, x6) x8 -> x3 x6 x8
        20: cond_abfoldr_f_g_acc_abs(Acons(x6, x7), x2, x3, x4) -> abfoldr_f_g_acc_abs_2(x2, x6) (abfoldr() x2 x3 x4
              x7)
        21: cond_abfoldr_f_g_acc_abs(Bcons(x6, x7), x2, x3, x4) -> abfoldr_f_g_acc_abs_5(x3, x6) (abfoldr() x2 x3 x4
              x7)
        22: cond_abfoldr_f_g_acc_abs(Nil(), x2, x3, x4) -> x4
        23: abfoldr_f_g_acc(x2, x3, x4) x5 -> cond_abfoldr_f_g_acc_abs(x5, x2, x3, x4)
        24: abfoldr_f_g(x2, x3) x4 -> abfoldr_f_g_acc(x2, x3, x4)
        25: abfoldr_f(x2) x3 -> abfoldr_f_g(x2, x3)
        26: abfoldr_1() x2 -> abfoldr_f(x2)
        27: abfoldr() x0 -> abfoldr_1() x0
        28: main_1(x0) x1 -> main_2(x0, x1) abfoldr()
        29: cond_plus_n_m(0(), x1) -> x1
        30: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3)
        31: plus_n(x1) x2 -> cond_plus_n_m(x2, x1)
        32: plus_1() x1 -> plus_n(x1)
        33: plus() x0 -> plus_1() x0
        34: main(x0) -> main_1(x0) plus()
        where
          0                        :: nat
          Acons                    :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons                    :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Nil                      :: ('a,'b) ablist
          Not_found                :: Exception
          S                        :: nat -> nat
          cons_all_abs             :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          abfoldr_f_g_acc          :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          cons_all                 :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          f                        :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          abfoldr_f                :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          fa                       :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb                       :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          g                        :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          abfoldr_f_g              :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          plus_n                   :: nat -> nat -> nat
          f_x                      :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          g_x                      :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          f_x_y                    :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          abfoldr_1                :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          cons_all_abs_1           :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          fa_1                     :: (nat,nat) ablist -> (nat,nat) ablist
          fb_1                     :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          main_1                   :: (nat,nat) ablist -> (nat -> nat -> nat) -> (nat,nat) ablist
          plus_1                   :: nat -> nat -> nat
          f_x_y_1                  :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          abfoldr_f_g_acc_abs_2    :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          main_2                   :: (nat,nat) ablist
                                       -> (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          main_3                   :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist
          main_4                   :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist
          abfoldr_f_g_acc_abs_5    :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          main_5                   :: ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist
          bot[0]                   :: Exception -> (nat,nat) ablist
          cond_abfoldr_f_g_acc_abs :: (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          cond_plus_n_m            :: nat -> nat -> nat
          abfoldr                  :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          plus                     :: nat -> nat -> nat
          main                     :: (nat,nat) ablist -> (nat,nat) ablist
    + Applied Processor:
        Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
    + Details:
        none
* Step 4: Inline WORST_CASE(?,O(n^3))
    + Considered Problem:
        1: main_4(x0) x4 -> x4 x0
        2: main_5(x3) x4 -> x3 x4
        3: main_3(x0) x7 -> main_5(x7) x0
        4: cons_all_abs_1(x2, x3, x4) x5 -> x2 x4 x5 Nil() x3
        5: g_x(x5) x6 -> Bcons(x5, x6)
        6: g() x5 -> g_x(x5)
        7: cons_all_abs(x4, x6) x8 -> x4 x8 g() Nil() x6
        8: f_x_y_1(x2, x5, x6) x7 -> x2 x6 x7 Nil() x5
        9: fb_1(x1, x4, x7) x8 -> Bcons(x1 x7 x4, x8)
        10: fb(x1, x4) x7 -> fb_1(x1, x4, x7)
        11: f_x_y(x3, x4, x9, x10) x12 -> x4 x12 fb(x3, x9) Nil() x10
        12: fa_1() x7 -> bot[0]() Not_found()
        13: fa() x6 -> fa_1()
        14: f_x(x2, x4, x8) x10 -> f_x_y_1(x4, x10, fa()) fb(x2, x8)
        15: f(x1, x2) x4 -> f_x(x1, x2, x4)
        16: cons_all(x3, x4) x6 -> cons_all_abs_1(x4, x6, f(x3, x4)) g()
        17: main_2(x0, x3) x5 -> main_4(x0) main_5(cons_all(x3, x5))
        18: abfoldr_f_g_acc_abs_2(x2, x6) x8 -> x2 x6 x8
        19: abfoldr_f_g_acc_abs_5(x3, x6) x8 -> x3 x6 x8
        20: cond_abfoldr_f_g_acc_abs(Acons(x12, x15), x4, x7, x9) -> x4 x12 (abfoldr() x4 x7 x9 x15)
        21: cond_abfoldr_f_g_acc_abs(Bcons(x12, x15), x5, x6, x9) -> x6 x12 (abfoldr() x5 x6 x9 x15)
        22: cond_abfoldr_f_g_acc_abs(Nil(), x2, x3, x4) -> x4
        23: abfoldr_f_g_acc(x2, x3, x4) x5 -> cond_abfoldr_f_g_acc_abs(x5, x2, x3, x4)
        24: abfoldr_f_g(x2, x3) x4 -> abfoldr_f_g_acc(x2, x3, x4)
        25: abfoldr_f(x2) x3 -> abfoldr_f_g(x2, x3)
        26: abfoldr_1() x2 -> abfoldr_f(x2)
        27: abfoldr() x4 -> abfoldr_f(x4)
        28: main_1(x0) x2 -> main_3(x0) cons_all(x2, abfoldr())
        29: cond_plus_n_m(0(), x1) -> x1
        30: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3)
        31: plus_n(x1) x2 -> cond_plus_n_m(x2, x1)
        32: plus_1() x1 -> plus_n(x1)
        33: plus() x2 -> plus_n(x2)
        34: main(x0) -> main_2(x0, plus()) abfoldr()
        where
          0                        :: nat
          Acons                    :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons                    :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Nil                      :: ('a,'b) ablist
          Not_found                :: Exception
          S                        :: nat -> nat
          cons_all_abs             :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          abfoldr_f_g_acc          :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          cons_all                 :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          f                        :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          abfoldr_f                :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          fa                       :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb                       :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          g                        :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          abfoldr_f_g              :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          plus_n                   :: nat -> nat -> nat
          f_x                      :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          g_x                      :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          f_x_y                    :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          abfoldr_1                :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          cons_all_abs_1           :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          fa_1                     :: (nat,nat) ablist -> (nat,nat) ablist
          fb_1                     :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          main_1                   :: (nat,nat) ablist -> (nat -> nat -> nat) -> (nat,nat) ablist
          plus_1                   :: nat -> nat -> nat
          f_x_y_1                  :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          abfoldr_f_g_acc_abs_2    :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          main_2                   :: (nat,nat) ablist
                                       -> (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          main_3                   :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist
          main_4                   :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist
          abfoldr_f_g_acc_abs_5    :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          main_5                   :: ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist
          bot[0]                   :: Exception -> (nat,nat) ablist
          cond_abfoldr_f_g_acc_abs :: (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          cond_plus_n_m            :: nat -> nat -> nat
          abfoldr                  :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          plus                     :: nat -> nat -> nat
          main                     :: (nat,nat) ablist -> (nat,nat) ablist
    + Applied Processor:
        Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
    + Details:
        none
* Step 5: Inline WORST_CASE(?,O(n^3))
    + Considered Problem:
        1: main_4(x0) x4 -> x4 x0
        2: main_5(x3) x4 -> x3 x4
        3: main_3(x8) x6 -> x6 x8
        4: cons_all_abs_1(x2, x3, x4) x5 -> x2 x4 x5 Nil() x3
        5: g_x(x5) x6 -> Bcons(x5, x6)
        6: g() x5 -> g_x(x5)
        7: cons_all_abs(x4, x6) x8 -> x4 x8 g() Nil() x6
        8: f_x_y_1(x2, x5, x6) x7 -> x2 x6 x7 Nil() x5
        9: fb_1(x1, x4, x7) x8 -> Bcons(x1 x7 x4, x8)
        10: fb(x1, x4) x7 -> fb_1(x1, x4, x7)
        11: f_x_y(x3, x4, x9, x10) x12 -> x4 x12 fb(x3, x9) Nil() x10
        12: fa_1() x7 -> bot[0]() Not_found()
        13: fa() x6 -> fa_1()
        14: f_x(x5, x4, x17) x10 -> x4 fa() fb(x5, x17) Nil() x10
        15: f(x1, x2) x4 -> f_x(x1, x2, x4)
        16: cons_all(x7, x4) x6 -> x4 f(x7, x4) g() Nil() x6
        17: main_2(x0, x7) x11 -> main_5(cons_all(x7, x11)) x0
        18: abfoldr_f_g_acc_abs_2(x2, x6) x8 -> x2 x6 x8
        19: abfoldr_f_g_acc_abs_5(x3, x6) x8 -> x3 x6 x8
        20: cond_abfoldr_f_g_acc_abs(Acons(x12, x15), x4, x7, x9) -> x4 x12 (abfoldr() x4 x7 x9 x15)
        21: cond_abfoldr_f_g_acc_abs(Bcons(x12, x15), x5, x6, x9) -> x6 x12 (abfoldr() x5 x6 x9 x15)
        22: cond_abfoldr_f_g_acc_abs(Nil(), x2, x3, x4) -> x4
        23: abfoldr_f_g_acc(x2, x3, x4) x5 -> cond_abfoldr_f_g_acc_abs(x5, x2, x3, x4)
        24: abfoldr_f_g(x2, x3) x4 -> abfoldr_f_g_acc(x2, x3, x4)
        25: abfoldr_f(x2) x3 -> abfoldr_f_g(x2, x3)
        26: abfoldr_1() x2 -> abfoldr_f(x2)
        27: abfoldr() x4 -> abfoldr_f(x4)
        28: main_1(x0) x5 -> main_5(cons_all(x5, abfoldr())) x0
        29: cond_plus_n_m(0(), x1) -> x1
        30: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3)
        31: plus_n(x1) x2 -> cond_plus_n_m(x2, x1)
        32: plus_1() x1 -> plus_n(x1)
        33: plus() x2 -> plus_n(x2)
        34: main(x0) -> main_4(x0) main_5(cons_all(plus(), abfoldr()))
        where
          0                        :: nat
          Acons                    :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons                    :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Nil                      :: ('a,'b) ablist
          Not_found                :: Exception
          S                        :: nat -> nat
          cons_all_abs             :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          abfoldr_f_g_acc          :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          cons_all                 :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          f                        :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          abfoldr_f                :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          fa                       :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb                       :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          g                        :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          abfoldr_f_g              :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          plus_n                   :: nat -> nat -> nat
          f_x                      :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          g_x                      :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          f_x_y                    :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          abfoldr_1                :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          cons_all_abs_1           :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          fa_1                     :: (nat,nat) ablist -> (nat,nat) ablist
          fb_1                     :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          main_1                   :: (nat,nat) ablist -> (nat -> nat -> nat) -> (nat,nat) ablist
          plus_1                   :: nat -> nat -> nat
          f_x_y_1                  :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          abfoldr_f_g_acc_abs_2    :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          main_2                   :: (nat,nat) ablist
                                       -> (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          main_3                   :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist
          main_4                   :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist
          abfoldr_f_g_acc_abs_5    :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          main_5                   :: ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist
          bot[0]                   :: Exception -> (nat,nat) ablist
          cond_abfoldr_f_g_acc_abs :: (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          cond_plus_n_m            :: nat -> nat -> nat
          abfoldr                  :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          plus                     :: nat -> nat -> nat
          main                     :: (nat,nat) ablist -> (nat,nat) ablist
    + Applied Processor:
        Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
    + Details:
        none
* Step 6: Inline WORST_CASE(?,O(n^3))
    + Considered Problem:
        1: main_4(x0) x4 -> x4 x0
        2: main_5(x3) x4 -> x3 x4
        3: main_3(x8) x6 -> x6 x8
        4: cons_all_abs_1(x2, x3, x4) x5 -> x2 x4 x5 Nil() x3
        5: g_x(x5) x6 -> Bcons(x5, x6)
        6: g() x5 -> g_x(x5)
        7: cons_all_abs(x4, x6) x8 -> x4 x8 g() Nil() x6
        8: f_x_y_1(x2, x5, x6) x7 -> x2 x6 x7 Nil() x5
        9: fb_1(x1, x4, x7) x8 -> Bcons(x1 x7 x4, x8)
        10: fb(x1, x4) x7 -> fb_1(x1, x4, x7)
        11: f_x_y(x3, x4, x9, x10) x12 -> x4 x12 fb(x3, x9) Nil() x10
        12: fa_1() x7 -> bot[0]() Not_found()
        13: fa() x6 -> fa_1()
        14: f_x(x5, x4, x17) x10 -> x4 fa() fb(x5, x17) Nil() x10
        15: f(x1, x2) x4 -> f_x(x1, x2, x4)
        16: cons_all(x7, x4) x6 -> x4 f(x7, x4) g() Nil() x6
        17: main_2(x8, x15) x23 -> cons_all(x15, x23) x8
        18: abfoldr_f_g_acc_abs_2(x2, x6) x8 -> x2 x6 x8
        19: abfoldr_f_g_acc_abs_5(x3, x6) x8 -> x3 x6 x8
        20: cond_abfoldr_f_g_acc_abs(Acons(x12, x15), x4, x7, x9) -> x4 x12 (abfoldr() x4 x7 x9 x15)
        21: cond_abfoldr_f_g_acc_abs(Bcons(x12, x15), x5, x6, x9) -> x6 x12 (abfoldr() x5 x6 x9 x15)
        22: cond_abfoldr_f_g_acc_abs(Nil(), x2, x3, x4) -> x4
        23: abfoldr_f_g_acc(x2, x3, x4) x5 -> cond_abfoldr_f_g_acc_abs(x5, x2, x3, x4)
        24: abfoldr_f_g(x2, x3) x4 -> abfoldr_f_g_acc(x2, x3, x4)
        25: abfoldr_f(x2) x3 -> abfoldr_f_g(x2, x3)
        26: abfoldr_1() x2 -> abfoldr_f(x2)
        27: abfoldr() x4 -> abfoldr_f(x4)
        28: main_1(x8) x11 -> cons_all(x11, abfoldr()) x8
        29: cond_plus_n_m(0(), x1) -> x1
        30: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3)
        31: plus_n(x1) x2 -> cond_plus_n_m(x2, x1)
        32: plus_1() x1 -> plus_n(x1)
        33: plus() x2 -> plus_n(x2)
        34: main(x0) -> main_5(cons_all(plus(), abfoldr())) x0
        where
          0                        :: nat
          Acons                    :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons                    :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Nil                      :: ('a,'b) ablist
          Not_found                :: Exception
          S                        :: nat -> nat
          cons_all_abs             :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          abfoldr_f_g_acc          :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          cons_all                 :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          f                        :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          abfoldr_f                :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          fa                       :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb                       :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          g                        :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          abfoldr_f_g              :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          plus_n                   :: nat -> nat -> nat
          f_x                      :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          g_x                      :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          f_x_y                    :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          abfoldr_1                :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          cons_all_abs_1           :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          fa_1                     :: (nat,nat) ablist -> (nat,nat) ablist
          fb_1                     :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          main_1                   :: (nat,nat) ablist -> (nat -> nat -> nat) -> (nat,nat) ablist
          plus_1                   :: nat -> nat -> nat
          f_x_y_1                  :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          abfoldr_f_g_acc_abs_2    :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          main_2                   :: (nat,nat) ablist
                                       -> (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          main_3                   :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist
          main_4                   :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist
          abfoldr_f_g_acc_abs_5    :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          main_5                   :: ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist
          bot[0]                   :: Exception -> (nat,nat) ablist
          cond_abfoldr_f_g_acc_abs :: (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          cond_plus_n_m            :: nat -> nat -> nat
          abfoldr                  :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          plus                     :: nat -> nat -> nat
          main                     :: (nat,nat) ablist -> (nat,nat) ablist
    + Applied Processor:
        Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
    + Details:
        none
* Step 7: Inline WORST_CASE(?,O(n^3))
    + Considered Problem:
        1: main_4(x0) x4 -> x4 x0
        2: main_5(x3) x4 -> x3 x4
        3: main_3(x8) x6 -> x6 x8
        4: cons_all_abs_1(x2, x3, x4) x5 -> x2 x4 x5 Nil() x3
        5: g_x(x5) x6 -> Bcons(x5, x6)
        6: g() x5 -> g_x(x5)
        7: cons_all_abs(x4, x6) x8 -> x4 x8 g() Nil() x6
        8: f_x_y_1(x2, x5, x6) x7 -> x2 x6 x7 Nil() x5
        9: fb_1(x1, x4, x7) x8 -> Bcons(x1 x7 x4, x8)
        10: fb(x1, x4) x7 -> fb_1(x1, x4, x7)
        11: f_x_y(x3, x4, x9, x10) x12 -> x4 x12 fb(x3, x9) Nil() x10
        12: fa_1() x7 -> bot[0]() Not_found()
        13: fa() x6 -> fa_1()
        14: f_x(x5, x4, x17) x10 -> x4 fa() fb(x5, x17) Nil() x10
        15: f(x1, x2) x4 -> f_x(x1, x2, x4)
        16: cons_all(x7, x4) x6 -> x4 f(x7, x4) g() Nil() x6
        17: main_2(x12, x14) x8 -> x8 f(x14, x8) g() Nil() x12
        18: abfoldr_f_g_acc_abs_2(x2, x6) x8 -> x2 x6 x8
        19: abfoldr_f_g_acc_abs_5(x3, x6) x8 -> x3 x6 x8
        20: cond_abfoldr_f_g_acc_abs(Acons(x12, x15), x4, x7, x9) -> x4 x12 (abfoldr() x4 x7 x9 x15)
        21: cond_abfoldr_f_g_acc_abs(Bcons(x12, x15), x5, x6, x9) -> x6 x12 (abfoldr() x5 x6 x9 x15)
        22: cond_abfoldr_f_g_acc_abs(Nil(), x2, x3, x4) -> x4
        23: abfoldr_f_g_acc(x2, x3, x4) x5 -> cond_abfoldr_f_g_acc_abs(x5, x2, x3, x4)
        24: abfoldr_f_g(x2, x3) x4 -> abfoldr_f_g_acc(x2, x3, x4)
        25: abfoldr_f(x2) x3 -> abfoldr_f_g(x2, x3)
        26: abfoldr_1() x2 -> abfoldr_f(x2)
        27: abfoldr() x4 -> abfoldr_f(x4)
        28: main_1(x12) x14 -> abfoldr() f(x14, abfoldr()) g() Nil() x12
        29: cond_plus_n_m(0(), x1) -> x1
        30: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3)
        31: plus_n(x1) x2 -> cond_plus_n_m(x2, x1)
        32: plus_1() x1 -> plus_n(x1)
        33: plus() x2 -> plus_n(x2)
        34: main(x8) -> cons_all(plus(), abfoldr()) x8
        where
          0                        :: nat
          Acons                    :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons                    :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Nil                      :: ('a,'b) ablist
          Not_found                :: Exception
          S                        :: nat -> nat
          cons_all_abs             :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          abfoldr_f_g_acc          :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          cons_all                 :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          f                        :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          abfoldr_f                :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          fa                       :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb                       :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          g                        :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          abfoldr_f_g              :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          plus_n                   :: nat -> nat -> nat
          f_x                      :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          g_x                      :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          f_x_y                    :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          abfoldr_1                :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          cons_all_abs_1           :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          fa_1                     :: (nat,nat) ablist -> (nat,nat) ablist
          fb_1                     :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          main_1                   :: (nat,nat) ablist -> (nat -> nat -> nat) -> (nat,nat) ablist
          plus_1                   :: nat -> nat -> nat
          f_x_y_1                  :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          abfoldr_f_g_acc_abs_2    :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          main_2                   :: (nat,nat) ablist
                                       -> (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          main_3                   :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist
          main_4                   :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist
          abfoldr_f_g_acc_abs_5    :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          main_5                   :: ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist
          bot[0]                   :: Exception -> (nat,nat) ablist
          cond_abfoldr_f_g_acc_abs :: (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          cond_plus_n_m            :: nat -> nat -> nat
          abfoldr                  :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          plus                     :: nat -> nat -> nat
          main                     :: (nat,nat) ablist -> (nat,nat) ablist
    + Applied Processor:
        Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
    + Details:
        none
* Step 8: Inline WORST_CASE(?,O(n^3))
    + Considered Problem:
        1: main_4(x0) x4 -> x4 x0
        2: main_5(x3) x4 -> x3 x4
        3: main_3(x8) x6 -> x6 x8
        4: cons_all_abs_1(x2, x3, x4) x5 -> x2 x4 x5 Nil() x3
        5: g_x(x5) x6 -> Bcons(x5, x6)
        6: g() x5 -> g_x(x5)
        7: cons_all_abs(x4, x6) x8 -> x4 x8 g() Nil() x6
        8: f_x_y_1(x2, x5, x6) x7 -> x2 x6 x7 Nil() x5
        9: fb_1(x1, x4, x7) x8 -> Bcons(x1 x7 x4, x8)
        10: fb(x1, x4) x7 -> fb_1(x1, x4, x7)
        11: f_x_y(x3, x4, x9, x10) x12 -> x4 x12 fb(x3, x9) Nil() x10
        12: fa_1() x7 -> bot[0]() Not_found()
        13: fa() x6 -> fa_1()
        14: f_x(x5, x4, x17) x10 -> x4 fa() fb(x5, x17) Nil() x10
        15: f(x1, x2) x4 -> f_x(x1, x2, x4)
        16: cons_all(x7, x4) x6 -> x4 f(x7, x4) g() Nil() x6
        17: main_2(x12, x14) x8 -> x8 f(x14, x8) g() Nil() x12
        18: abfoldr_f_g_acc_abs_2(x2, x6) x8 -> x2 x6 x8
        19: abfoldr_f_g_acc_abs_5(x3, x6) x8 -> x3 x6 x8
        20: cond_abfoldr_f_g_acc_abs(Acons(x12, x15), x4, x7, x9) -> x4 x12 (abfoldr() x4 x7 x9 x15)
        21: cond_abfoldr_f_g_acc_abs(Bcons(x12, x15), x5, x6, x9) -> x6 x12 (abfoldr() x5 x6 x9 x15)
        22: cond_abfoldr_f_g_acc_abs(Nil(), x2, x3, x4) -> x4
        23: abfoldr_f_g_acc(x2, x3, x4) x5 -> cond_abfoldr_f_g_acc_abs(x5, x2, x3, x4)
        24: abfoldr_f_g(x2, x3) x4 -> abfoldr_f_g_acc(x2, x3, x4)
        25: abfoldr_f(x2) x3 -> abfoldr_f_g(x2, x3)
        26: abfoldr_1() x2 -> abfoldr_f(x2)
        27: abfoldr() x4 -> abfoldr_f(x4)
        28: main_1(x12) x14 -> abfoldr() f(x14, abfoldr()) g() Nil() x12
        29: cond_plus_n_m(0(), x1) -> x1
        30: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3)
        31: plus_n(x1) x2 -> cond_plus_n_m(x2, x1)
        32: plus_1() x1 -> plus_n(x1)
        33: plus() x2 -> plus_n(x2)
        34: main(x12) -> abfoldr() f(plus(), abfoldr()) g() Nil() x12
        where
          0                        :: nat
          Acons                    :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons                    :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Nil                      :: ('a,'b) ablist
          Not_found                :: Exception
          S                        :: nat -> nat
          cons_all_abs             :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          abfoldr_f_g_acc          :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          cons_all                 :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          f                        :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          abfoldr_f                :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          fa                       :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb                       :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          g                        :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          abfoldr_f_g              :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          plus_n                   :: nat -> nat -> nat
          f_x                      :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          g_x                      :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          f_x_y                    :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          abfoldr_1                :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          cons_all_abs_1           :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          fa_1                     :: (nat,nat) ablist -> (nat,nat) ablist
          fb_1                     :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          main_1                   :: (nat,nat) ablist -> (nat -> nat -> nat) -> (nat,nat) ablist
          plus_1                   :: nat -> nat -> nat
          f_x_y_1                  :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          abfoldr_f_g_acc_abs_2    :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          main_2                   :: (nat,nat) ablist
                                       -> (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          main_3                   :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist
          main_4                   :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist
          abfoldr_f_g_acc_abs_5    :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          main_5                   :: ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist
          bot[0]                   :: Exception -> (nat,nat) ablist
          cond_abfoldr_f_g_acc_abs :: (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          cond_plus_n_m            :: nat -> nat -> nat
          abfoldr                  :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          plus                     :: nat -> nat -> nat
          main                     :: (nat,nat) ablist -> (nat,nat) ablist
    + Applied Processor:
        Inline {inlineType = InlineFull, inlineSelect = <inline case-expression>}
    + Details:
        none
* Step 9: UsableRules WORST_CASE(?,O(n^3))
    + Considered Problem:
        1: main_4(x0) x4 -> x4 x0
        2: main_5(x3) x4 -> x3 x4
        3: main_3(x8) x6 -> x6 x8
        4: cons_all_abs_1(x2, x3, x4) x5 -> x2 x4 x5 Nil() x3
        5: g_x(x5) x6 -> Bcons(x5, x6)
        6: g() x5 -> g_x(x5)
        7: cons_all_abs(x4, x6) x8 -> x4 x8 g() Nil() x6
        8: f_x_y_1(x2, x5, x6) x7 -> x2 x6 x7 Nil() x5
        9: fb_1(x1, x4, x7) x8 -> Bcons(x1 x7 x4, x8)
        10: fb(x1, x4) x7 -> fb_1(x1, x4, x7)
        11: f_x_y(x3, x4, x9, x10) x12 -> x4 x12 fb(x3, x9) Nil() x10
        12: fa_1() x7 -> bot[0]() Not_found()
        13: fa() x6 -> fa_1()
        14: f_x(x5, x4, x17) x10 -> x4 fa() fb(x5, x17) Nil() x10
        15: f(x1, x2) x4 -> f_x(x1, x2, x4)
        16: cons_all(x7, x4) x6 -> x4 f(x7, x4) g() Nil() x6
        17: main_2(x12, x14) x8 -> x8 f(x14, x8) g() Nil() x12
        18: abfoldr_f_g_acc_abs_2(x2, x6) x8 -> x2 x6 x8
        19: abfoldr_f_g_acc_abs_5(x3, x6) x8 -> x3 x6 x8
        20: cond_abfoldr_f_g_acc_abs(Acons(x12, x15), x4, x7, x9) -> x4 x12 (abfoldr() x4 x7 x9 x15)
        21: cond_abfoldr_f_g_acc_abs(Bcons(x12, x15), x5, x6, x9) -> x6 x12 (abfoldr() x5 x6 x9 x15)
        22: cond_abfoldr_f_g_acc_abs(Nil(), x2, x3, x4) -> x4
        23: abfoldr_f_g_acc(x8, x14, x18) Acons(x24, x30) -> x8 x24 (abfoldr() x8 x14 x18 x30)
        24: abfoldr_f_g_acc(x10, x12, x18) Bcons(x24, x30) -> x12 x24 (abfoldr() x10 x12 x18 x30)
        25: abfoldr_f_g_acc(x4, x6, x8) Nil() -> x8
        26: abfoldr_f_g(x2, x3) x4 -> abfoldr_f_g_acc(x2, x3, x4)
        27: abfoldr_f(x2) x3 -> abfoldr_f_g(x2, x3)
        28: abfoldr_1() x2 -> abfoldr_f(x2)
        29: abfoldr() x4 -> abfoldr_f(x4)
        30: main_1(x12) x14 -> abfoldr() f(x14, abfoldr()) g() Nil() x12
        31: cond_plus_n_m(0(), x1) -> x1
        32: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3)
        33: plus_n(x2) 0() -> x2
        34: plus_n(x2) S(x6) -> S(plus() x2 x6)
        35: plus_1() x1 -> plus_n(x1)
        36: plus() x2 -> plus_n(x2)
        37: main(x12) -> abfoldr() f(plus(), abfoldr()) g() Nil() x12
        where
          0                        :: nat
          Acons                    :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons                    :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Nil                      :: ('a,'b) ablist
          Not_found                :: Exception
          S                        :: nat -> nat
          cons_all_abs             :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          abfoldr_f_g_acc          :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          cons_all                 :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          f                        :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          abfoldr_f                :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          fa                       :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb                       :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          g                        :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          abfoldr_f_g              :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          plus_n                   :: nat -> nat -> nat
          f_x                      :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          g_x                      :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          f_x_y                    :: (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          abfoldr_1                :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          cons_all_abs_1           :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          fa_1                     :: (nat,nat) ablist -> (nat,nat) ablist
          fb_1                     :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          main_1                   :: (nat,nat) ablist -> (nat -> nat -> nat) -> (nat,nat) ablist
          plus_1                   :: nat -> nat -> nat
          f_x_y_1                  :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist
                                        -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          abfoldr_f_g_acc_abs_2    :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          main_2                   :: (nat,nat) ablist
                                       -> (nat -> nat -> nat)
                                       -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist
                                            -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
          main_3                   :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist
          main_4                   :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist
          abfoldr_f_g_acc_abs_5    :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> nat
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          main_5                   :: ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist
          bot[0]                   :: Exception -> (nat,nat) ablist
          cond_abfoldr_f_g_acc_abs :: (nat,nat) ablist
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          cond_plus_n_m            :: nat -> nat -> nat
          abfoldr                  :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
                                       -> (nat,nat) ablist
          plus                     :: nat -> nat -> nat
          main                     :: (nat,nat) ablist -> (nat,nat) ablist
    + Applied Processor:
        UsableRules {urType = Syntactic}
    + Details:
        none
* Step 10: NeededRules WORST_CASE(?,O(n^3))
    + Considered Problem:
        1: main_4(x0) x4 -> x4 x0
        2: main_5(x3) x4 -> x3 x4
        3: main_3(x8) x6 -> x6 x8
        4: cons_all_abs_1(x2, x3, x4) x5 -> x2 x4 x5 Nil() x3
        5: g_x(x5) x6 -> Bcons(x5, x6)
        6: g() x5 -> g_x(x5)
        7: cons_all_abs(x4, x6) x8 -> x4 x8 g() Nil() x6
        8: f_x_y_1(x2, x5, x6) x7 -> x2 x6 x7 Nil() x5
        9: fb_1(x1, x4, x7) x8 -> Bcons(x1 x7 x4, x8)
        10: fb(x1, x4) x7 -> fb_1(x1, x4, x7)
        11: f_x_y(x3, x4, x9, x10) x12 -> x4 x12 fb(x3, x9) Nil() x10
        12: fa_1() x7 -> bot[0]() Not_found()
        13: fa() x6 -> fa_1()
        14: f_x(x5, x4, x17) x10 -> x4 fa() fb(x5, x17) Nil() x10
        15: f(x1, x2) x4 -> f_x(x1, x2, x4)
        16: cons_all(x7, x4) x6 -> x4 f(x7, x4) g() Nil() x6
        17: main_2(x12, x14) x8 -> x8 f(x14, x8) g() Nil() x12
        18: abfoldr_f_g_acc_abs_2(x2, x6) x8 -> x2 x6 x8
        19: abfoldr_f_g_acc_abs_5(x3, x6) x8 -> x3 x6 x8
        23: abfoldr_f_g_acc(x8, x14, x18) Acons(x24, x30) -> x8 x24 (abfoldr() x8 x14 x18 x30)
        24: abfoldr_f_g_acc(x10, x12, x18) Bcons(x24, x30) -> x12 x24 (abfoldr() x10 x12 x18 x30)
        25: abfoldr_f_g_acc(x4, x6, x8) Nil() -> x8
        26: abfoldr_f_g(x2, x3) x4 -> abfoldr_f_g_acc(x2, x3, x4)
        27: abfoldr_f(x2) x3 -> abfoldr_f_g(x2, x3)
        28: abfoldr_1() x2 -> abfoldr_f(x2)
        29: abfoldr() x4 -> abfoldr_f(x4)
        30: main_1(x12) x14 -> abfoldr() f(x14, abfoldr()) g() Nil() x12
        33: plus_n(x2) 0() -> x2
        34: plus_n(x2) S(x6) -> S(plus() x2 x6)
        35: plus_1() x1 -> plus_n(x1)
        36: plus() x2 -> plus_n(x2)
        37: main(x12) -> abfoldr() f(plus(), abfoldr()) g() Nil() x12
        where
          0                     :: nat
          Acons                 :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons                 :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Nil                   :: ('a,'b) ablist
          Not_found             :: Exception
          S                     :: nat -> nat
          cons_all_abs          :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
          abfoldr_f_g_acc       :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
          cons_all              :: (nat -> nat -> nat)
                                    -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                         -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                         -> (nat,nat) ablist
                                         -> (nat,nat) ablist
                                         -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
          f                     :: (nat -> nat -> nat)
                                    -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                         -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                         -> (nat,nat) ablist
                                         -> (nat,nat) ablist
                                         -> (nat,nat) ablist)
                                    -> nat
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
          abfoldr_f             :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
          fa                    :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb                    :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          g                     :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          abfoldr_f_g           :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
          plus_n                :: nat -> nat -> nat
          f_x                   :: (nat -> nat -> nat)
                                    -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                         -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                         -> (nat,nat) ablist
                                         -> (nat,nat) ablist
                                         -> (nat,nat) ablist)
                                    -> nat
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
          g_x                   :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          f_x_y                 :: (nat -> nat -> nat)
                                    -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                         -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                         -> (nat,nat) ablist
                                         -> (nat,nat) ablist
                                         -> (nat,nat) ablist)
                                    -> nat
                                    -> (nat,nat) ablist
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
          abfoldr_1             :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
          cons_all_abs_1        :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
          fa_1                  :: (nat,nat) ablist -> (nat,nat) ablist
          fb_1                  :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          main_1                :: (nat,nat) ablist -> (nat -> nat -> nat) -> (nat,nat) ablist
          plus_1                :: nat -> nat -> nat
          f_x_y_1               :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
          abfoldr_f_g_acc_abs_2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> nat
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
          main_2                :: (nat,nat) ablist
                                    -> (nat -> nat -> nat)
                                    -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                         -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                         -> (nat,nat) ablist
                                         -> (nat,nat) ablist
                                         -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
          main_3                :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist
          main_4                :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist
          abfoldr_f_g_acc_abs_5 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> nat
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
          main_5                :: ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist
          bot[0]                :: Exception -> (nat,nat) ablist
          abfoldr               :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
          plus                  :: nat -> nat -> nat
          main                  :: (nat,nat) ablist -> (nat,nat) ablist
    + Applied Processor:
        NeededRules
    + Details:
        none
* Step 11: CFA WORST_CASE(?,O(n^3))
    + Considered Problem:
        1: main_4(x0) x4 -> x4 x0
        2: main_5(x3) x4 -> x3 x4
        3: main_3(x8) x6 -> x6 x8
        4: cons_all_abs_1(x2, x3, x4) x5 -> x2 x4 x5 Nil() x3
        5: g_x(x5) x6 -> Bcons(x5, x6)
        6: g() x5 -> g_x(x5)
        7: cons_all_abs(x4, x6) x8 -> x4 x8 g() Nil() x6
        8: f_x_y_1(x2, x5, x6) x7 -> x2 x6 x7 Nil() x5
        9: fb_1(x1, x4, x7) x8 -> Bcons(x1 x7 x4, x8)
        10: fb(x1, x4) x7 -> fb_1(x1, x4, x7)
        11: f_x_y(x3, x4, x9, x10) x12 -> x4 x12 fb(x3, x9) Nil() x10
        12: fa_1() x7 -> bot[0]() Not_found()
        13: fa() x6 -> fa_1()
        14: f_x(x5, x4, x17) x10 -> x4 fa() fb(x5, x17) Nil() x10
        15: f(x1, x2) x4 -> f_x(x1, x2, x4)
        16: cons_all(x7, x4) x6 -> x4 f(x7, x4) g() Nil() x6
        17: main_2(x12, x14) x8 -> x8 f(x14, x8) g() Nil() x12
        18: abfoldr_f_g_acc_abs_2(x2, x6) x8 -> x2 x6 x8
        19: abfoldr_f_g_acc_abs_5(x3, x6) x8 -> x3 x6 x8
        20: abfoldr_f_g_acc(x8, x14, x18) Acons(x24, x30) -> x8 x24 (abfoldr() x8 x14 x18 x30)
        21: abfoldr_f_g_acc(x10, x12, x18) Bcons(x24, x30) -> x12 x24 (abfoldr() x10 x12 x18 x30)
        22: abfoldr_f_g_acc(x4, x6, x8) Nil() -> x8
        23: abfoldr_f_g(x2, x3) x4 -> abfoldr_f_g_acc(x2, x3, x4)
        24: abfoldr_f(x2) x3 -> abfoldr_f_g(x2, x3)
        25: abfoldr_1() x2 -> abfoldr_f(x2)
        26: abfoldr() x4 -> abfoldr_f(x4)
        27: main_1(x12) x14 -> abfoldr() f(x14, abfoldr()) g() Nil() x12
        28: plus_n(x2) 0() -> x2
        29: plus_n(x2) S(x6) -> S(plus() x2 x6)
        30: plus_1() x1 -> plus_n(x1)
        31: plus() x2 -> plus_n(x2)
        32: main(x12) -> abfoldr() f(plus(), abfoldr()) g() Nil() x12
        where
          0                     :: nat
          Acons                 :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons                 :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Nil                   :: ('a,'b) ablist
          Not_found             :: Exception
          S                     :: nat -> nat
          cons_all_abs          :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
          abfoldr_f_g_acc       :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
          cons_all              :: (nat -> nat -> nat)
                                    -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                         -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                         -> (nat,nat) ablist
                                         -> (nat,nat) ablist
                                         -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
          f                     :: (nat -> nat -> nat)
                                    -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                         -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                         -> (nat,nat) ablist
                                         -> (nat,nat) ablist
                                         -> (nat,nat) ablist)
                                    -> nat
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
          abfoldr_f             :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
          fa                    :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb                    :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          g                     :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          abfoldr_f_g           :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
          plus_n                :: nat -> nat -> nat
          f_x                   :: (nat -> nat -> nat)
                                    -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                         -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                         -> (nat,nat) ablist
                                         -> (nat,nat) ablist
                                         -> (nat,nat) ablist)
                                    -> nat
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
          g_x                   :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          f_x_y                 :: (nat -> nat -> nat)
                                    -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                         -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                         -> (nat,nat) ablist
                                         -> (nat,nat) ablist
                                         -> (nat,nat) ablist)
                                    -> nat
                                    -> (nat,nat) ablist
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
          abfoldr_1             :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
          cons_all_abs_1        :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
          fa_1                  :: (nat,nat) ablist -> (nat,nat) ablist
          fb_1                  :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          main_1                :: (nat,nat) ablist -> (nat -> nat -> nat) -> (nat,nat) ablist
          plus_1                :: nat -> nat -> nat
          f_x_y_1               :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
          abfoldr_f_g_acc_abs_2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> nat
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
          main_2                :: (nat,nat) ablist
                                    -> (nat -> nat -> nat)
                                    -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                         -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                         -> (nat,nat) ablist
                                         -> (nat,nat) ablist
                                         -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
          main_3                :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist
          main_4                :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist
          abfoldr_f_g_acc_abs_5 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> nat
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
          main_5                :: ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist
          bot[0]                :: Exception -> (nat,nat) ablist
          abfoldr               :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
                                    -> (nat,nat) ablist
          plus                  :: nat -> nat -> nat
          main                  :: (nat,nat) ablist -> (nat,nat) ablist
    + Applied Processor:
        CFA {cfaRefinement = <control flow analysis>}
    + Details:
        {X{*} -> Nil()
              |  S(X{*})
              |  S(X{*})
              |  0()
              |  Nil()
              |  Nil()
              |  Bcons(X{*},X{*})
              |  Acons(X{*},X{*})
              |  Nil()
              |  Nil()
              |  Nil()
              |  Not_found()
              |  Nil()
              |  Bcons(X{*},X{*})
              |  Nil()
              |  Nil()
              |  Bcons(X{*},X{*})
              |  Nil()
        ,V{x1_9} -> V{x1_10}
        ,V{x1_10} -> V{x5_14}
        ,V{x1_15} -> plus()
        ,V{x2_15} -> abfoldr()
        ,V{x2_23} -> V{x2_24}
        ,V{x2_24} -> V{x4_26}
        ,V{x2_28} -> V{x2_31}
        ,V{x2_29} -> V{x2_31}
        ,V{x2_31} -> V{x2_29}
                  |  V{x7_9}
        ,V{x3_23} -> V{x3_24}
        ,V{x3_24} -> fb(V{x5_14},V{x17_14})
                  |  V{x12_21}
                  |  V{x14_20}
                  |  g()
        ,V{x4_9} -> V{x4_10}
        ,V{x4_10} -> V{x17_14}
        ,V{x4_14} -> V{x2_15}
        ,V{x4_15} -> V{x24_20}
        ,V{x4_22} -> V{x2_23}
        ,V{x4_23} -> V{x18_21}
                  |  V{x18_20}
                  |  Nil()
        ,V{x4_26} -> fa()
                  |  V{x10_21}
                  |  V{x8_20}
                  |  f(plus(),abfoldr())
        ,V{x5_5} -> V{x5_6}
        ,V{x5_6} -> V{x24_21}
        ,V{x5_14} -> V{x1_15}
        ,V{x6_5} -> R{22}
                 |  R{21}
                 |  R{20}
        ,V{x6_13} -> V{x24_20}
        ,V{x6_22} -> V{x3_23}
        ,V{x6_29} -> X{*}
        ,V{x7_9} -> V{x7_10}
        ,V{x7_10} -> V{x24_21}
        ,V{x7_12} -> R{22}
                  |  R{21}
                  |  R{20}
        ,V{x8_9} -> R{22}
                 |  R{21}
                 |  R{20}
        ,V{x8_20} -> V{x2_23}
        ,V{x8_22} -> V{x4_23}
        ,V{x10_14} -> R{21}
                   |  R{20}
                   |  R{22}
        ,V{x10_21} -> V{x2_23}
        ,V{x12_21} -> V{x3_23}
        ,V{x12_32} -> X{*}
        ,V{x14_20} -> V{x3_23}
        ,V{x17_14} -> V{x4_15}
        ,V{x18_20} -> V{x4_23}
        ,V{x18_21} -> V{x4_23}
        ,V{x24_20} -> X{*}
        ,V{x24_21} -> R{29}
                   |  R{28}
                   |  V{x5_5}
                   |  @(@(V{x1_9},V{x7_9}),V{x4_9})
                   |  @(R{31},V{x4_9})
                   |  X{*}
        ,V{x30_20} -> X{*}
        ,V{x30_21} -> V{x6_5}
                   |  V{x8_9}
                   |  X{*}
        ,R{0} -> R{32}
              |  main(X{*})
        ,R{5} -> Bcons(V{x5_5},V{x6_5})
        ,R{6} -> g_x(V{x5_6})
        ,R{9} -> Bcons(R{29},V{x8_9})
              |  Bcons(R{28},V{x8_9})
              |  Bcons(@(R{31},V{x4_9}),V{x8_9})
              |  Bcons(@(@(V{x1_9},V{x7_9}),V{x4_9}),V{x8_9})
        ,R{10} -> fb_1(V{x1_10},V{x4_10},V{x7_10})
        ,R{12} -> @(bot[0](),Not_found())
        ,R{13} -> fa_1()
        ,R{14} -> R{22}
               |  R{21}
               |  @(R{23},V{x10_14})
               |  @(@(R{24},Nil()),V{x10_14})
               |  @(@(@(R{26},fb(V{x5_14},V{x17_14})),Nil()),V{x10_14})
               |  @(@(@(@(V{x4_14},fa()),fb(V{x5_14},V{x17_14})),Nil()),V{x10_14})
        ,R{15} -> f_x(V{x1_15},V{x2_15},V{x4_15})
        ,R{20} -> R{12}
               |  @(R{13},@(@(@(@(abfoldr(),V{x8_20}),V{x14_20}),V{x18_20}),V{x30_20}))
               |  @(R{13},@(@(@(R{26},V{x14_20}),V{x18_20}),V{x30_20}))
               |  @(R{13},@(@(R{24},V{x18_20}),V{x30_20}))
               |  @(R{13},@(R{23},V{x30_20}))
               |  @(R{13},R{20})
               |  @(R{13},R{21})
               |  @(R{13},R{22})
               |  R{14}
               |  @(R{15},R{20})
               |  @(R{15},R{21})
               |  @(R{15},R{22})
               |  @(@(V{x8_20},V{x24_20}),R{22})
               |  @(@(V{x8_20},V{x24_20}),R{21})
               |  @(@(V{x8_20},V{x24_20}),R{20})
               |  @(R{15},@(R{23},V{x30_20}))
               |  @(@(V{x8_20},V{x24_20}),@(R{23},V{x30_20}))
               |  @(R{15},@(@(R{24},V{x18_20}),V{x30_20}))
               |  @(@(V{x8_20},V{x24_20}),@(@(R{24},V{x18_20}),V{x30_20}))
               |  @(R{15},@(@(@(R{26},V{x14_20}),V{x18_20}),V{x30_20}))
               |  @(@(V{x8_20},V{x24_20}),@(@(@(R{26},V{x14_20}),V{x18_20}),V{x30_20}))
               |  @(R{15},@(@(@(@(abfoldr(),V{x8_20}),V{x14_20}),V{x18_20}),V{x30_20}))
               |  @(@(V{x8_20},V{x24_20}),@(@(@(@(abfoldr(),V{x8_20}),V{x14_20}),V{x18_20}),V{x30_20}))
        ,R{21} -> R{9}
               |  @(R{10},@(@(@(@(abfoldr(),V{x10_21}),V{x12_21}),V{x18_21}),V{x30_21}))
               |  @(R{10},@(@(@(R{26},V{x12_21}),V{x18_21}),V{x30_21}))
               |  @(R{10},@(@(R{24},V{x18_21}),V{x30_21}))
               |  @(R{10},@(R{23},V{x30_21}))
               |  @(R{10},R{20})
               |  @(R{10},R{21})
               |  @(R{10},R{22})
               |  R{5}
               |  @(R{6},R{20})
               |  @(R{6},R{21})
               |  @(R{6},R{22})
               |  @(@(V{x12_21},V{x24_21}),R{22})
               |  @(@(V{x12_21},V{x24_21}),R{21})
               |  @(@(V{x12_21},V{x24_21}),R{20})
               |  @(R{6},@(R{23},V{x30_21}))
               |  @(@(V{x12_21},V{x24_21}),@(R{23},V{x30_21}))
               |  @(R{6},@(@(R{24},V{x18_21}),V{x30_21}))
               |  @(@(V{x12_21},V{x24_21}),@(@(R{24},V{x18_21}),V{x30_21}))
               |  @(R{6},@(@(@(R{26},V{x12_21}),V{x18_21}),V{x30_21}))
               |  @(@(V{x12_21},V{x24_21}),@(@(@(R{26},V{x12_21}),V{x18_21}),V{x30_21}))
               |  @(R{6},@(@(@(@(abfoldr(),V{x10_21}),V{x12_21}),V{x18_21}),V{x30_21}))
               |  @(@(V{x12_21},V{x24_21}),@(@(@(@(abfoldr(),V{x10_21}),V{x12_21}),V{x18_21}),V{x30_21}))
        ,R{22} -> V{x8_22}
        ,R{23} -> abfoldr_f_g_acc(V{x2_23},V{x3_23},V{x4_23})
        ,R{24} -> abfoldr_f_g(V{x2_24},V{x3_24})
        ,R{26} -> abfoldr_f(V{x4_26})
        ,R{28} -> V{x2_28}
        ,R{29} -> S(R{29})
               |  S(R{28})
               |  S(@(R{31},V{x6_29}))
               |  S(@(@(plus(),V{x2_29}),V{x6_29}))
        ,R{31} -> plus_n(V{x2_31})
        ,R{32} -> R{22}
               |  R{21}
               |  R{20}
               |  @(R{23},V{x12_32})
               |  @(@(R{24},Nil()),V{x12_32})
               |  @(@(@(R{26},g()),Nil()),V{x12_32})
               |  @(@(@(@(abfoldr(),f(plus(),abfoldr())),g()),Nil()),V{x12_32})}
* Step 12: UncurryATRS WORST_CASE(?,O(n^3))
    + Considered Problem:
        5: g_x(x5) x6 -> Bcons(x5, x6)
        6: g() x5 -> g_x(x5)
        9: fb_1(plus(), x3, x2) x1 -> Bcons(plus() x2 x3, x1)
        10: fb(plus(), x2) x1 -> fb_1(plus(), x2, x1)
        12: fa_1() x7 -> bot[0]() Not_found()
        13: fa() x6 -> fa_1()
        14: f_x(plus(), abfoldr(), x2) x1 -> abfoldr() fa() fb(plus(), x2) Nil() x1
        15: f(plus(), abfoldr()) x1 -> f_x(plus(), abfoldr(), x1)
        20: abfoldr_f_g_acc(fa(), x3, Nil()) Acons(x2, x1) -> fa() x2 (abfoldr() fa() x3 Nil() x1)
        21: abfoldr_f_g_acc(f(plus(), abfoldr()), x3, Nil()) Acons(x2, x1) -> f(plus(), abfoldr()) x2 (abfoldr()
              f(plus(), abfoldr()) x3 Nil() x1)
        22: abfoldr_f_g_acc(x5, fb(x3, x4), Nil()) Bcons(x2, x1) -> fb(x3, x4) x2 (abfoldr() x5 fb(x3, x4) Nil() x1)
        23: abfoldr_f_g_acc(x3, g(), Nil()) Bcons(x2, x1) -> g() x2 (abfoldr() x3 g() Nil() x1)
        24: abfoldr_f_g_acc(x2, x1, Nil()) Nil() -> Nil()
        25: abfoldr_f_g(x2, x1) Nil() -> abfoldr_f_g_acc(x2, x1, Nil())
        26: abfoldr_f(x2) x3 -> abfoldr_f_g(x2, x3)
        28: abfoldr() x4 -> abfoldr_f(x4)
        30: plus_n(x2) 0() -> x2
        31: plus_n(x2) S(x1) -> S(plus() x2 x1)
        33: plus() x2 -> plus_n(x2)
        34: main(x1) -> abfoldr() f(plus(), abfoldr()) g() Nil() x1
        where
          0               :: nat
          Acons           :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons           :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Nil             :: ('a,'b) ablist
          Not_found       :: Exception
          S               :: nat -> nat
          abfoldr_f_g_acc :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                              -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                              -> (nat,nat) ablist
                              -> (nat,nat) ablist
                              -> (nat,nat) ablist
          f               :: (nat -> nat -> nat)
                              -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                   -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                   -> (nat,nat) ablist
                                   -> (nat,nat) ablist
                                   -> (nat,nat) ablist)
                              -> nat
                              -> (nat,nat) ablist
                              -> (nat,nat) ablist
          abfoldr_f       :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                              -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                              -> (nat,nat) ablist
                              -> (nat,nat) ablist
                              -> (nat,nat) ablist
          fa              :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb              :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          g               :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          abfoldr_f_g     :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                              -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                              -> (nat,nat) ablist
                              -> (nat,nat) ablist
                              -> (nat,nat) ablist
          plus_n          :: nat -> nat -> nat
          f_x             :: (nat -> nat -> nat)
                              -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                   -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                   -> (nat,nat) ablist
                                   -> (nat,nat) ablist
                                   -> (nat,nat) ablist)
                              -> nat
                              -> (nat,nat) ablist
                              -> (nat,nat) ablist
          g_x             :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fa_1            :: (nat,nat) ablist -> (nat,nat) ablist
          fb_1            :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          bot[0]          :: Exception -> (nat,nat) ablist
          abfoldr         :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                              -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                              -> (nat,nat) ablist
                              -> (nat,nat) ablist
                              -> (nat,nat) ablist
          plus            :: nat -> nat -> nat
          main            :: (nat,nat) ablist -> (nat,nat) ablist
    + Applied Processor:
        UncurryATRS
    + Details:
        none
* Step 13: Inline WORST_CASE(?,O(n^3))
    + Considered Problem:
        1: g_x#1(x5, x6) -> Bcons(x5, x6)
        2: g#1(x5) -> g_x(x5)
        3: g#2(x5, x6) -> g_x#1(x5, x6)
        4: fb_1#1(plus(), x3, x2, x1) -> Bcons(plus#2(x2, x3), x1)
        5: fb#1(plus(), x2, x1) -> fb_1(plus(), x2, x1)
        6: fb#2(plus(), x2, x1, x3) -> fb_1#1(plus(), x2, x1, x3)
        7: fa_1#1(x7) -> bot[0]#1(Not_found())
        8: fa#1(x6) -> fa_1()
        9: fa#2(x6, x0) -> fa_1#1(x0)
        10: f_x#1(plus(), abfoldr(), x2, x1) -> abfoldr#4(fa(), fb(plus(), x2), Nil(), x1)
        11: f#1(plus(), abfoldr(), x1) -> f_x(plus(), abfoldr(), x1)
        12: f#2(plus(), abfoldr(), x1, x2) -> f_x#1(plus(), abfoldr(), x1, x2)
        13: abfoldr_f_g_acc#1(fa(), x3, Nil(), Acons(x2, x1)) -> fa#2(x2, abfoldr#4(fa(), x3, Nil(), x1))
        14: abfoldr_f_g_acc#1(f(plus(), abfoldr()), x3, Nil(), Acons(x2, x1)) -> f#2(plus(), abfoldr()
                                                                                     , x2
                                                                                     , abfoldr#4(f(plus(), abfoldr())
                                                                                                 , x3, Nil(), x1))
        15: abfoldr_f_g_acc#1(x5, fb(x3, x4), Nil(), Bcons(x2, x1)) -> fb#2(x3, x4
                                                                            , x2
                                                                            , abfoldr#4(x5, fb(x3, x4), Nil(), x1))
        16: abfoldr_f_g_acc#1(x3, g(), Nil(), Bcons(x2, x1)) -> g#2(x2, abfoldr#4(x3, g(), Nil(), x1))
        17: abfoldr_f_g_acc#1(x2, x1, Nil(), Nil()) -> Nil()
        18: abfoldr_f_g#1(x2, x1, Nil()) -> abfoldr_f_g_acc(x2, x1, Nil())
        19: abfoldr_f_g#2(x2, x1, Nil(), x3) -> abfoldr_f_g_acc#1(x2, x1, Nil(), x3)
        20: abfoldr_f#1(x2, x3) -> abfoldr_f_g(x2, x3)
        21: abfoldr_f#2(x2, x3, x4) -> abfoldr_f_g#1(x2, x3, x4)
        22: abfoldr_f#3(x2, x3, x4, x5) -> abfoldr_f_g#2(x2, x3, x4, x5)
        23: abfoldr#1(x4) -> abfoldr_f(x4)
        24: abfoldr#2(x4, x5) -> abfoldr_f#1(x4, x5)
        25: abfoldr#3(x4, x5, x6) -> abfoldr_f#2(x4, x5, x6)
        26: abfoldr#4(x4, x5, x6, x7) -> abfoldr_f#3(x4, x5, x6, x7)
        27: plus_n#1(x2, 0()) -> x2
        28: plus_n#1(x2, S(x1)) -> S(plus#2(x2, x1))
        29: plus#1(x2) -> plus_n(x2)
        30: plus#2(x2, x3) -> plus_n#1(x2, x3)
        31: main(x1) -> abfoldr#4(f(plus(), abfoldr()), g(), Nil(), x1)
        where
          0                 :: nat
          Acons             :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons             :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Nil               :: ('a,'b) ablist
          Not_found         :: Exception
          S                 :: nat -> nat
          abfoldr           :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr#1         :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr#2         :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr#3         :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr#4         :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f         :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f#1       :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f#2       :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f#3       :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f_g       :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f_g#1     :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f_g#2     :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f_g_acc   :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f_g_acc#1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          bot[0]#1          :: Exception -> (nat,nat) ablist
          f                 :: (nat -> nat -> nat)
                                -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                -> nat
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          f#1               :: (nat -> nat -> nat)
                                -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                -> nat
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          f#2               :: (nat -> nat -> nat)
                                -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                -> nat
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          f_x               :: (nat -> nat -> nat)
                                -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                -> nat
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          f_x#1             :: (nat -> nat -> nat)
                                -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                -> nat
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          fa                :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fa#1              :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fa#2              :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fa_1              :: (nat,nat) ablist -> (nat,nat) ablist
          fa_1#1            :: (nat,nat) ablist -> (nat,nat) ablist
          fb                :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb#1              :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb#2              :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb_1              :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb_1#1            :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          g                 :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          g#1               :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          g#2               :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          g_x               :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          g_x#1             :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          main              :: (nat,nat) ablist -> (nat,nat) ablist
          plus              :: nat -> nat -> nat
          plus#1            :: nat -> nat -> nat
          plus#2            :: nat -> nat -> nat
          plus_n            :: nat -> nat -> nat
          plus_n#1          :: nat -> nat -> nat
    + Applied Processor:
        Inline {inlineType = InlineFull, inlineSelect = <inline decreasing>}
    + Details:
        none
* Step 14: UsableRules WORST_CASE(?,O(n^3))
    + Considered Problem:
        1: g_x#1(x5, x6) -> Bcons(x5, x6)
        2: g#1(x5) -> g_x(x5)
        3: g#2(x5, x6) -> g_x#1(x5, x6)
        4: fb_1#1(plus(), x3, x2, x1) -> Bcons(plus#2(x2, x3), x1)
        5: fb#1(plus(), x2, x1) -> fb_1(plus(), x2, x1)
        6: fb#2(plus(), x2, x1, x3) -> fb_1#1(plus(), x2, x1, x3)
        7: fa_1#1(x7) -> bot[0]#1(Not_found())
        8: fa#1(x6) -> fa_1()
        9: fa#2(x6, x0) -> fa_1#1(x0)
        10: f_x#1(plus(), abfoldr(), x2, x1) -> abfoldr#4(fa(), fb(plus(), x2), Nil(), x1)
        11: f#1(plus(), abfoldr(), x1) -> f_x(plus(), abfoldr(), x1)
        12: f#2(plus(), abfoldr(), x1, x2) -> f_x#1(plus(), abfoldr(), x1, x2)
        13: abfoldr_f_g_acc#1(fa(), x7, Nil(), Acons(x12, x3)) -> fa_1#1(abfoldr#4(fa(), x7, Nil(), x3))
        14: abfoldr_f_g_acc#1(f(plus(), abfoldr()), x3, Nil(), Acons(x2, x1)) -> f#2(plus(), abfoldr()
                                                                                     , x2
                                                                                     , abfoldr#4(f(plus(), abfoldr())
                                                                                                 , x3, Nil(), x1))
        15: abfoldr_f_g_acc#1(x5, fb(x3, x4), Nil(), Bcons(x2, x1)) -> fb#2(x3, x4
                                                                            , x2
                                                                            , abfoldr#4(x5, fb(x3, x4), Nil(), x1))
        16: abfoldr_f_g_acc#1(x3, g(), Nil(), Bcons(x2, x1)) -> g#2(x2, abfoldr#4(x3, g(), Nil(), x1))
        17: abfoldr_f_g_acc#1(x2, x1, Nil(), Nil()) -> Nil()
        18: abfoldr_f_g#1(x2, x1, Nil()) -> abfoldr_f_g_acc(x2, x1, Nil())
        19: abfoldr_f_g#2(x2, x1, Nil(), x3) -> abfoldr_f_g_acc#1(x2, x1, Nil(), x3)
        20: abfoldr_f#1(x2, x3) -> abfoldr_f_g(x2, x3)
        21: abfoldr_f#2(x2, x3, x4) -> abfoldr_f_g#1(x2, x3, x4)
        22: abfoldr_f#3(x2, x3, x4, x5) -> abfoldr_f_g#2(x2, x3, x4, x5)
        23: abfoldr#1(x4) -> abfoldr_f(x4)
        24: abfoldr#2(x4, x5) -> abfoldr_f#1(x4, x5)
        25: abfoldr#3(x4, x5, x6) -> abfoldr_f#2(x4, x5, x6)
        26: abfoldr#4(x4, x5, x6, x7) -> abfoldr_f#3(x4, x5, x6, x7)
        27: plus_n#1(x2, 0()) -> x2
        28: plus_n#1(x2, S(x1)) -> S(plus#2(x2, x1))
        29: plus#1(x2) -> plus_n(x2)
        30: plus#2(x2, x3) -> plus_n#1(x2, x3)
        31: main(x1) -> abfoldr#4(f(plus(), abfoldr()), g(), Nil(), x1)
        where
          0                 :: nat
          Acons             :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons             :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Nil               :: ('a,'b) ablist
          Not_found         :: Exception
          S                 :: nat -> nat
          abfoldr           :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr#1         :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr#2         :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr#3         :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr#4         :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f         :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f#1       :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f#2       :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f#3       :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f_g       :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f_g#1     :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f_g#2     :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f_g_acc   :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f_g_acc#1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          bot[0]#1          :: Exception -> (nat,nat) ablist
          f                 :: (nat -> nat -> nat)
                                -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                -> nat
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          f#1               :: (nat -> nat -> nat)
                                -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                -> nat
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          f#2               :: (nat -> nat -> nat)
                                -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                -> nat
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          f_x               :: (nat -> nat -> nat)
                                -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                -> nat
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          f_x#1             :: (nat -> nat -> nat)
                                -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                -> nat
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          fa                :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fa#1              :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fa#2              :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fa_1              :: (nat,nat) ablist -> (nat,nat) ablist
          fa_1#1            :: (nat,nat) ablist -> (nat,nat) ablist
          fb                :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb#1              :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb#2              :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb_1              :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb_1#1            :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          g                 :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          g#1               :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          g#2               :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          g_x               :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          g_x#1             :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          main              :: (nat,nat) ablist -> (nat,nat) ablist
          plus              :: nat -> nat -> nat
          plus#1            :: nat -> nat -> nat
          plus#2            :: nat -> nat -> nat
          plus_n            :: nat -> nat -> nat
          plus_n#1          :: nat -> nat -> nat
    + Applied Processor:
        UsableRules {urType = Syntactic}
    + Details:
        none
* Step 15: Inline WORST_CASE(?,O(n^3))
    + Considered Problem:
        1: g_x#1(x5, x6) -> Bcons(x5, x6)
        3: g#2(x5, x6) -> g_x#1(x5, x6)
        4: fb_1#1(plus(), x3, x2, x1) -> Bcons(plus#2(x2, x3), x1)
        6: fb#2(plus(), x2, x1, x3) -> fb_1#1(plus(), x2, x1, x3)
        7: fa_1#1(x7) -> bot[0]#1(Not_found())
        10: f_x#1(plus(), abfoldr(), x2, x1) -> abfoldr#4(fa(), fb(plus(), x2), Nil(), x1)
        12: f#2(plus(), abfoldr(), x1, x2) -> f_x#1(plus(), abfoldr(), x1, x2)
        13: abfoldr_f_g_acc#1(fa(), x7, Nil(), Acons(x12, x3)) -> fa_1#1(abfoldr#4(fa(), x7, Nil(), x3))
        14: abfoldr_f_g_acc#1(f(plus(), abfoldr()), x3, Nil(), Acons(x2, x1)) -> f#2(plus(), abfoldr()
                                                                                     , x2
                                                                                     , abfoldr#4(f(plus(), abfoldr())
                                                                                                 , x3, Nil(), x1))
        15: abfoldr_f_g_acc#1(x5, fb(x3, x4), Nil(), Bcons(x2, x1)) -> fb#2(x3, x4
                                                                            , x2
                                                                            , abfoldr#4(x5, fb(x3, x4), Nil(), x1))
        16: abfoldr_f_g_acc#1(x3, g(), Nil(), Bcons(x2, x1)) -> g#2(x2, abfoldr#4(x3, g(), Nil(), x1))
        17: abfoldr_f_g_acc#1(x2, x1, Nil(), Nil()) -> Nil()
        19: abfoldr_f_g#2(x2, x1, Nil(), x3) -> abfoldr_f_g_acc#1(x2, x1, Nil(), x3)
        22: abfoldr_f#3(x2, x3, x4, x5) -> abfoldr_f_g#2(x2, x3, x4, x5)
        26: abfoldr#4(x4, x5, x6, x7) -> abfoldr_f#3(x4, x5, x6, x7)
        27: plus_n#1(x2, 0()) -> x2
        28: plus_n#1(x2, S(x1)) -> S(plus#2(x2, x1))
        30: plus#2(x2, x3) -> plus_n#1(x2, x3)
        31: main(x1) -> abfoldr#4(f(plus(), abfoldr()), g(), Nil(), x1)
        where
          0                 :: nat
          Acons             :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons             :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Nil               :: ('a,'b) ablist
          Not_found         :: Exception
          S                 :: nat -> nat
          abfoldr           :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr#4         :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f#3       :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f_g#2     :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f_g_acc#1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          bot[0]#1          :: Exception -> (nat,nat) ablist
          f                 :: (nat -> nat -> nat)
                                -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                -> nat
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          f#2               :: (nat -> nat -> nat)
                                -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                -> nat
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          f_x#1             :: (nat -> nat -> nat)
                                -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                -> nat
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          fa                :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fa_1#1            :: (nat,nat) ablist -> (nat,nat) ablist
          fb                :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb#2              :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb_1#1            :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          g                 :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          g#2               :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          g_x#1             :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          main              :: (nat,nat) ablist -> (nat,nat) ablist
          plus              :: nat -> nat -> nat
          plus#2            :: nat -> nat -> nat
          plus_n#1          :: nat -> nat -> nat
    + Applied Processor:
        Inline {inlineType = InlineFull, inlineSelect = <inline decreasing>}
    + Details:
        none
* Step 16: UsableRules WORST_CASE(?,O(n^3))
    + Considered Problem:
        1: g_x#1(x5, x6) -> Bcons(x5, x6)
        2: g#2(x10, x12) -> Bcons(x10, x12)
        3: fb_1#1(plus(), x3, x2, x1) -> Bcons(plus#2(x2, x3), x1)
        4: fb#2(plus(), x6, x4, x2) -> Bcons(plus#2(x4, x6), x2)
        5: fa_1#1(x7) -> bot[0]#1(Not_found())
        6: f_x#1(plus(), abfoldr(), x2, x1) -> abfoldr#4(fa(), fb(plus(), x2), Nil(), x1)
        7: f#2(plus(), abfoldr(), x4, x2) -> abfoldr#4(fa(), fb(plus(), x4), Nil(), x2)
        8: abfoldr_f_g_acc#1(fa(), x7, Nil(), Acons(x12, x3)) -> fa_1#1(abfoldr#4(fa(), x7, Nil(), x3))
        9: abfoldr_f_g_acc#1(f(plus(), abfoldr()), x7, Nil(), Acons(x2, x3)) -> f_x#1(plus(), abfoldr()
                                                                                      , x2
                                                                                      , abfoldr#4(f(plus(), abfoldr())
                                                                                                  , x7, Nil(), x3))
        10: abfoldr_f_g_acc#1(x11, fb(plus(), x4), Nil(), Bcons(x2, x3)) -> fb_1#1(plus(), x4
                                                                                   , x2
                                                                                   , abfoldr#4(x11, fb(plus(), x4)
                                                                                               , Nil()
                                                                                               , x3))
        11: abfoldr_f_g_acc#1(x7, g(), Nil(), Bcons(x10, x3)) -> g_x#1(x10, abfoldr#4(x7, g(), Nil(), x3))
        12: abfoldr_f_g_acc#1(x2, x1, Nil(), Nil()) -> Nil()
        13: abfoldr_f_g#2(fa(), x14, Nil(), Acons(x24, x6)) -> fa_1#1(abfoldr#4(fa(), x14, Nil(), x6))
        14: abfoldr_f_g#2(f(plus(), abfoldr()), x6, Nil(), Acons(x4, x2)) -> f#2(plus(), abfoldr()
                                                                                 , x4
                                                                                 , abfoldr#4(f(plus(), abfoldr()), x6
                                                                                             , Nil()
                                                                                             , x2))
        15: abfoldr_f_g#2(x10, fb(x6, x8), Nil(), Bcons(x4, x2)) -> fb#2(x6, x8
                                                                         , x4
                                                                         , abfoldr#4(x10, fb(x6, x8), Nil(), x2))
        16: abfoldr_f_g#2(x6, g(), Nil(), Bcons(x4, x2)) -> g#2(x4, abfoldr#4(x6, g(), Nil(), x2))
        17: abfoldr_f_g#2(x4, x2, Nil(), Nil()) -> Nil()
        18: abfoldr_f#3(x4, x2, Nil(), x6) -> abfoldr_f_g_acc#1(x4, x2, Nil(), x6)
        19: abfoldr#4(x4, x6, x8, x10) -> abfoldr_f_g#2(x4, x6, x8, x10)
        20: plus_n#1(x2, 0()) -> x2
        21: plus_n#1(x2, S(x1)) -> S(plus#2(x2, x1))
        22: plus#2(x4, 0()) -> x4
        23: plus#2(x4, S(x2)) -> S(plus#2(x4, x2))
        24: main(x1) -> abfoldr#4(f(plus(), abfoldr()), g(), Nil(), x1)
        where
          0                 :: nat
          Acons             :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons             :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Nil               :: ('a,'b) ablist
          Not_found         :: Exception
          S                 :: nat -> nat
          abfoldr           :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr#4         :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f#3       :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f_g#2     :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          abfoldr_f_g_acc#1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          bot[0]#1          :: Exception -> (nat,nat) ablist
          f                 :: (nat -> nat -> nat)
                                -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                -> nat
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          f#2               :: (nat -> nat -> nat)
                                -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                -> nat
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          f_x#1             :: (nat -> nat -> nat)
                                -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist
                                     -> (nat,nat) ablist)
                                -> nat
                                -> (nat,nat) ablist
                                -> (nat,nat) ablist
          fa                :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fa_1#1            :: (nat,nat) ablist -> (nat,nat) ablist
          fb                :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb#2              :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb_1#1            :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          g                 :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          g#2               :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          g_x#1             :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          main              :: (nat,nat) ablist -> (nat,nat) ablist
          plus              :: nat -> nat -> nat
          plus#2            :: nat -> nat -> nat
          plus_n#1          :: nat -> nat -> nat
    + Applied Processor:
        UsableRules {urType = Syntactic}
    + Details:
        none
* Step 17: Inline WORST_CASE(?,O(n^3))
    + Considered Problem:
        2: g#2(x10, x12) -> Bcons(x10, x12)
        4: fb#2(plus(), x6, x4, x2) -> Bcons(plus#2(x4, x6), x2)
        5: fa_1#1(x7) -> bot[0]#1(Not_found())
        7: f#2(plus(), abfoldr(), x4, x2) -> abfoldr#4(fa(), fb(plus(), x4), Nil(), x2)
        13: abfoldr_f_g#2(fa(), x14, Nil(), Acons(x24, x6)) -> fa_1#1(abfoldr#4(fa(), x14, Nil(), x6))
        14: abfoldr_f_g#2(f(plus(), abfoldr()), x6, Nil(), Acons(x4, x2)) -> f#2(plus(), abfoldr()
                                                                                 , x4
                                                                                 , abfoldr#4(f(plus(), abfoldr()), x6
                                                                                             , Nil()
                                                                                             , x2))
        15: abfoldr_f_g#2(x10, fb(x6, x8), Nil(), Bcons(x4, x2)) -> fb#2(x6, x8
                                                                         , x4
                                                                         , abfoldr#4(x10, fb(x6, x8), Nil(), x2))
        16: abfoldr_f_g#2(x6, g(), Nil(), Bcons(x4, x2)) -> g#2(x4, abfoldr#4(x6, g(), Nil(), x2))
        17: abfoldr_f_g#2(x4, x2, Nil(), Nil()) -> Nil()
        19: abfoldr#4(x4, x6, x8, x10) -> abfoldr_f_g#2(x4, x6, x8, x10)
        22: plus#2(x4, 0()) -> x4
        23: plus#2(x4, S(x2)) -> S(plus#2(x4, x2))
        24: main(x1) -> abfoldr#4(f(plus(), abfoldr()), g(), Nil(), x1)
        where
          0             :: nat
          Acons         :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons         :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Nil           :: ('a,'b) ablist
          Not_found     :: Exception
          S             :: nat -> nat
          abfoldr       :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                            -> (nat,nat) ablist
                            -> (nat,nat) ablist
                            -> (nat,nat) ablist
          abfoldr#4     :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                            -> (nat,nat) ablist
                            -> (nat,nat) ablist
                            -> (nat,nat) ablist
          abfoldr_f_g#2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                            -> (nat,nat) ablist
                            -> (nat,nat) ablist
                            -> (nat,nat) ablist
          bot[0]#1      :: Exception -> (nat,nat) ablist
          f             :: (nat -> nat -> nat)
                            -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                 -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                 -> (nat,nat) ablist
                                 -> (nat,nat) ablist
                                 -> (nat,nat) ablist)
                            -> nat
                            -> (nat,nat) ablist
                            -> (nat,nat) ablist
          f#2           :: (nat -> nat -> nat)
                            -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                 -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                 -> (nat,nat) ablist
                                 -> (nat,nat) ablist
                                 -> (nat,nat) ablist)
                            -> nat
                            -> (nat,nat) ablist
                            -> (nat,nat) ablist
          fa            :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fa_1#1        :: (nat,nat) ablist -> (nat,nat) ablist
          fb            :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb#2          :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          g             :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          g#2           :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          main          :: (nat,nat) ablist -> (nat,nat) ablist
          plus          :: nat -> nat -> nat
          plus#2        :: nat -> nat -> nat
    + Applied Processor:
        Inline {inlineType = InlineFull, inlineSelect = <inline decreasing>}
    + Details:
        none
* Step 18: UsableRules WORST_CASE(?,O(n^3))
    + Considered Problem:
        1: g#2(x10, x12) -> Bcons(x10, x12)
        2: fb#2(plus(), x6, x4, x2) -> Bcons(plus#2(x4, x6), x2)
        3: fa_1#1(x7) -> bot[0]#1(Not_found())
        4: f#2(plus(), abfoldr(), x4, x2) -> abfoldr#4(fa(), fb(plus(), x4), Nil(), x2)
        5: abfoldr_f_g#2(fa(), x14, Nil(), Acons(x24, x6)) -> fa_1#1(abfoldr#4(fa(), x14, Nil(), x6))
        6: abfoldr_f_g#2(f(plus(), abfoldr()), x13, Nil(), Acons(x8, x5)) -> abfoldr#4(fa(), fb(plus(), x8)
                                                                                       , Nil()
                                                                                       , abfoldr#4(f(plus(), abfoldr())
                                                                                                   , x13, Nil(), x5))
        7: abfoldr_f_g#2(x21, fb(plus(), x12), Nil(), Bcons(x8, x5)) -> Bcons(plus#2(x8, x12), abfoldr#4(x21
                                                                                                         , fb(plus()
                                                                                                              , x12)
                                                                                                         , Nil()
                                                                                                         , x5))
        8: abfoldr_f_g#2(x13, g(), Nil(), Bcons(x20, x5)) -> Bcons(x20, abfoldr#4(x13, g(), Nil(), x5))
        9: abfoldr_f_g#2(x4, x2, Nil(), Nil()) -> Nil()
        10: abfoldr#4(fa(), x28, Nil(), Acons(x48, x12)) -> fa_1#1(abfoldr#4(fa(), x28, Nil(), x12))
        11: abfoldr#4(f(plus(), abfoldr()), x12, Nil(), Acons(x8, x4)) -> f#2(plus(), abfoldr()
                                                                              , x8
                                                                              , abfoldr#4(f(plus(), abfoldr()), x12
                                                                                          , Nil()
                                                                                          , x4))
        12: abfoldr#4(x20, fb(x12, x16), Nil(), Bcons(x8, x4)) -> fb#2(x12, x16
                                                                       , x8
                                                                       , abfoldr#4(x20, fb(x12, x16), Nil(), x4))
        13: abfoldr#4(x12, g(), Nil(), Bcons(x8, x4)) -> g#2(x8, abfoldr#4(x12, g(), Nil(), x4))
        14: abfoldr#4(x8, x4, Nil(), Nil()) -> Nil()
        15: plus#2(x4, 0()) -> x4
        16: plus#2(x4, S(x2)) -> S(plus#2(x4, x2))
        17: main(x1) -> abfoldr#4(f(plus(), abfoldr()), g(), Nil(), x1)
        where
          0             :: nat
          Acons         :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons         :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Nil           :: ('a,'b) ablist
          Not_found     :: Exception
          S             :: nat -> nat
          abfoldr       :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                            -> (nat,nat) ablist
                            -> (nat,nat) ablist
                            -> (nat,nat) ablist
          abfoldr#4     :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                            -> (nat,nat) ablist
                            -> (nat,nat) ablist
                            -> (nat,nat) ablist
          abfoldr_f_g#2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                            -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                            -> (nat,nat) ablist
                            -> (nat,nat) ablist
                            -> (nat,nat) ablist
          bot[0]#1      :: Exception -> (nat,nat) ablist
          f             :: (nat -> nat -> nat)
                            -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                 -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                 -> (nat,nat) ablist
                                 -> (nat,nat) ablist
                                 -> (nat,nat) ablist)
                            -> nat
                            -> (nat,nat) ablist
                            -> (nat,nat) ablist
          f#2           :: (nat -> nat -> nat)
                            -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                 -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                                 -> (nat,nat) ablist
                                 -> (nat,nat) ablist
                                 -> (nat,nat) ablist)
                            -> nat
                            -> (nat,nat) ablist
                            -> (nat,nat) ablist
          fa            :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fa_1#1        :: (nat,nat) ablist -> (nat,nat) ablist
          fb            :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb#2          :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          g             :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          g#2           :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          main          :: (nat,nat) ablist -> (nat,nat) ablist
          plus          :: nat -> nat -> nat
          plus#2        :: nat -> nat -> nat
    + Applied Processor:
        UsableRules {urType = Syntactic}
    + Details:
        none
* Step 19: Inline WORST_CASE(?,O(n^3))
    + Considered Problem:
        1: g#2(x10, x12) -> Bcons(x10, x12)
        2: fb#2(plus(), x6, x4, x2) -> Bcons(plus#2(x4, x6), x2)
        3: fa_1#1(x7) -> bot[0]#1(Not_found())
        4: f#2(plus(), abfoldr(), x4, x2) -> abfoldr#4(fa(), fb(plus(), x4), Nil(), x2)
        10: abfoldr#4(fa(), x28, Nil(), Acons(x48, x12)) -> fa_1#1(abfoldr#4(fa(), x28, Nil(), x12))
        11: abfoldr#4(f(plus(), abfoldr()), x12, Nil(), Acons(x8, x4)) -> f#2(plus(), abfoldr()
                                                                              , x8
                                                                              , abfoldr#4(f(plus(), abfoldr()), x12
                                                                                          , Nil()
                                                                                          , x4))
        12: abfoldr#4(x20, fb(x12, x16), Nil(), Bcons(x8, x4)) -> fb#2(x12, x16
                                                                       , x8
                                                                       , abfoldr#4(x20, fb(x12, x16), Nil(), x4))
        13: abfoldr#4(x12, g(), Nil(), Bcons(x8, x4)) -> g#2(x8, abfoldr#4(x12, g(), Nil(), x4))
        14: abfoldr#4(x8, x4, Nil(), Nil()) -> Nil()
        15: plus#2(x4, 0()) -> x4
        16: plus#2(x4, S(x2)) -> S(plus#2(x4, x2))
        17: main(x1) -> abfoldr#4(f(plus(), abfoldr()), g(), Nil(), x1)
        where
          0         :: nat
          Acons     :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons     :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Nil       :: ('a,'b) ablist
          Not_found :: Exception
          S         :: nat -> nat
          abfoldr   :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
          abfoldr#4 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
          bot[0]#1  :: Exception -> (nat,nat) ablist
          f         :: (nat -> nat -> nat)
                        -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                             -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                             -> (nat,nat) ablist
                             -> (nat,nat) ablist
                             -> (nat,nat) ablist)
                        -> nat
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
          f#2       :: (nat -> nat -> nat)
                        -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                             -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                             -> (nat,nat) ablist
                             -> (nat,nat) ablist
                             -> (nat,nat) ablist)
                        -> nat
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
          fa        :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fa_1#1    :: (nat,nat) ablist -> (nat,nat) ablist
          fb        :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb#2      :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          g         :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          g#2       :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          main      :: (nat,nat) ablist -> (nat,nat) ablist
          plus      :: nat -> nat -> nat
          plus#2    :: nat -> nat -> nat
    + Applied Processor:
        Inline {inlineType = InlineFull, inlineSelect = <inline decreasing>}
    + Details:
        none
* Step 20: UsableRules WORST_CASE(?,O(n^3))
    + Considered Problem:
        1: g#2(x10, x12) -> Bcons(x10, x12)
        2: fb#2(plus(), x6, x4, x2) -> Bcons(plus#2(x4, x6), x2)
        3: fa_1#1(x7) -> bot[0]#1(Not_found())
        4: f#2(plus(), abfoldr(), x4, x2) -> abfoldr#4(fa(), fb(plus(), x4), Nil(), x2)
        5: abfoldr#4(fa(), x28, Nil(), Acons(x48, x12)) -> fa_1#1(abfoldr#4(fa(), x28, Nil(), x12))
        6: abfoldr#4(f(plus(), abfoldr()), x25, Nil(), Acons(x8, x9)) -> abfoldr#4(fa(), fb(plus(), x8)
                                                                                   , Nil()
                                                                                   , abfoldr#4(f(plus(), abfoldr()), x25
                                                                                               , Nil()
                                                                                               , x9))
        7: abfoldr#4(x41, fb(plus(), x12), Nil(), Bcons(x8, x9)) -> Bcons(plus#2(x8, x12), abfoldr#4(x41, fb(plus()
                                                                                                             , x12)
                                                                                                     , Nil()
                                                                                                     , x9))
        8: abfoldr#4(x25, g(), Nil(), Bcons(x20, x9)) -> Bcons(x20, abfoldr#4(x25, g(), Nil(), x9))
        9: abfoldr#4(x8, x4, Nil(), Nil()) -> Nil()
        10: plus#2(x4, 0()) -> x4
        11: plus#2(x4, S(x2)) -> S(plus#2(x4, x2))
        12: main(x1) -> abfoldr#4(f(plus(), abfoldr()), g(), Nil(), x1)
        where
          0         :: nat
          Acons     :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons     :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Nil       :: ('a,'b) ablist
          Not_found :: Exception
          S         :: nat -> nat
          abfoldr   :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
          abfoldr#4 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
          bot[0]#1  :: Exception -> (nat,nat) ablist
          f         :: (nat -> nat -> nat)
                        -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                             -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                             -> (nat,nat) ablist
                             -> (nat,nat) ablist
                             -> (nat,nat) ablist)
                        -> nat
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
          f#2       :: (nat -> nat -> nat)
                        -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                             -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                             -> (nat,nat) ablist
                             -> (nat,nat) ablist
                             -> (nat,nat) ablist)
                        -> nat
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
          fa        :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fa_1#1    :: (nat,nat) ablist -> (nat,nat) ablist
          fb        :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb#2      :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          g         :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          g#2       :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          main      :: (nat,nat) ablist -> (nat,nat) ablist
          plus      :: nat -> nat -> nat
          plus#2    :: nat -> nat -> nat
    + Applied Processor:
        UsableRules {urType = Syntactic}
    + Details:
        none
* Step 21: UsableRules WORST_CASE(?,O(n^3))
    + Considered Problem:
        3: fa_1#1(x7) -> bot[0]#1(Not_found())
        5: abfoldr#4(fa(), x28, Nil(), Acons(x48, x12)) -> fa_1#1(abfoldr#4(fa(), x28, Nil(), x12))
        6: abfoldr#4(f(plus(), abfoldr()), x25, Nil(), Acons(x8, x9)) -> abfoldr#4(fa(), fb(plus(), x8)
                                                                                   , Nil()
                                                                                   , abfoldr#4(f(plus(), abfoldr()), x25
                                                                                               , Nil()
                                                                                               , x9))
        7: abfoldr#4(x41, fb(plus(), x12), Nil(), Bcons(x8, x9)) -> Bcons(plus#2(x8, x12), abfoldr#4(x41, fb(plus()
                                                                                                             , x12)
                                                                                                     , Nil()
                                                                                                     , x9))
        8: abfoldr#4(x25, g(), Nil(), Bcons(x20, x9)) -> Bcons(x20, abfoldr#4(x25, g(), Nil(), x9))
        9: abfoldr#4(x8, x4, Nil(), Nil()) -> Nil()
        10: plus#2(x4, 0()) -> x4
        11: plus#2(x4, S(x2)) -> S(plus#2(x4, x2))
        12: main(x1) -> abfoldr#4(f(plus(), abfoldr()), g(), Nil(), x1)
        where
          0         :: nat
          Acons     :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons     :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Nil       :: ('a,'b) ablist
          Not_found :: Exception
          S         :: nat -> nat
          abfoldr   :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
          abfoldr#4 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
          bot[0]#1  :: Exception -> (nat,nat) ablist
          f         :: (nat -> nat -> nat)
                        -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                             -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                             -> (nat,nat) ablist
                             -> (nat,nat) ablist
                             -> (nat,nat) ablist)
                        -> nat
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
          fa        :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fa_1#1    :: (nat,nat) ablist -> (nat,nat) ablist
          fb        :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          g         :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          main      :: (nat,nat) ablist -> (nat,nat) ablist
          plus      :: nat -> nat -> nat
          plus#2    :: nat -> nat -> nat
    + Applied Processor:
        UsableRules {urType = DFA}
    + Details:
        none
* Step 22: Compression WORST_CASE(?,O(n^3))
    + Considered Problem:
        3: abfoldr#4(f(plus(), abfoldr()), x25, Nil(), Acons(x8, x9)) -> abfoldr#4(fa(), fb(plus(), x8)
                                                                                   , Nil()
                                                                                   , abfoldr#4(f(plus(), abfoldr()), x25
                                                                                               , Nil()
                                                                                               , x9))
        4: abfoldr#4(x41, fb(plus(), x12), Nil(), Bcons(x8, x9)) -> Bcons(plus#2(x8, x12), abfoldr#4(x41, fb(plus()
                                                                                                             , x12)
                                                                                                     , Nil()
                                                                                                     , x9))
        5: abfoldr#4(x25, g(), Nil(), Bcons(x20, x9)) -> Bcons(x20, abfoldr#4(x25, g(), Nil(), x9))
        6: abfoldr#4(x8, x4, Nil(), Nil()) -> Nil()
        7: plus#2(x4, 0()) -> x4
        8: plus#2(x4, S(x2)) -> S(plus#2(x4, x2))
        9: main(x1) -> abfoldr#4(f(plus(), abfoldr()), g(), Nil(), x1)
        where
          0         :: nat
          Acons     :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons     :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Nil       :: ('a,'b) ablist
          S         :: nat -> nat
          abfoldr   :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
          abfoldr#4 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
          f         :: (nat -> nat -> nat)
                        -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist)
                             -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                             -> (nat,nat) ablist
                             -> (nat,nat) ablist
                             -> (nat,nat) ablist)
                        -> nat
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
          fa        :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb        :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          g         :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          main      :: (nat,nat) ablist -> (nat,nat) ablist
          plus      :: nat -> nat -> nat
          plus#2    :: nat -> nat -> nat
    + Applied Processor:
        Compression
    + Details:
        none
* Step 23: ToTctProblem WORST_CASE(?,O(n^3))
    + Considered Problem:
        1: abfoldr#4(f(), x25, Acons(x8, x9)) -> abfoldr#4(fa(), fb(x8), abfoldr#4(f(), x25, x9))
        2: abfoldr#4(x41, fb(x12), Bcons(x8, x9)) -> Bcons(plus#2(x8, x12), abfoldr#4(x41, fb(x12), x9))
        3: abfoldr#4(x25, g(), Bcons(x20, x9)) -> Bcons(x20, abfoldr#4(x25, g(), x9))
        4: abfoldr#4(x8, x4, Nil()) -> Nil()
        5: plus#2(x4, 0()) -> x4
        6: plus#2(x4, S(x2)) -> S(plus#2(x4, x2))
        7: main(x1) -> abfoldr#4(f(), g(), x1)
        where
          0         :: nat
          Acons     :: 'a -> ('a,'b) ablist -> ('a,'b) ablist
          Bcons     :: 'b -> ('a,'b) ablist -> ('a,'b) ablist
          Nil       :: ('a,'b) ablist
          S         :: nat -> nat
          abfoldr#4 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                        -> (nat -> (nat,nat) ablist -> (nat,nat) ablist)
                        -> (nat,nat) ablist
                        -> (nat,nat) ablist
          f         :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fa        :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          fb        :: nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist
          g         :: nat -> (nat,nat) ablist -> (nat,nat) ablist
          main      :: (nat,nat) ablist -> (nat,nat) ablist
          plus#2    :: nat -> nat -> nat
    + Applied Processor:
        ToTctProblem
    + Details:
        none
* Step 24: DependencyPairs WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9))
            abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9))
            abfoldr#4(x8,x4,Nil()) -> Nil()
            abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9))
            main(x1) -> abfoldr#4(f(),g(),x1)
            plus#2(x4,0()) -> x4
            plus#2(x4,S(x2)) -> S(plus#2(x4,x2))
        - Signature:
            {abfoldr#4/3,main/1,plus#2/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1,g/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main} and constructors {0,Acons,Bcons,Nil,S}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9))
          abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9))
          abfoldr#4#(x8,x4,Nil()) -> c_3()
          abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                 ,abfoldr#4#(f(),x25,x9))
          main#(x1) -> c_5(abfoldr#4#(f(),g(),x1))
          plus#2#(x4,0()) -> c_6()
          plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2))
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 25: PredecessorEstimation WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9))
            abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9))
            abfoldr#4#(x8,x4,Nil()) -> c_3()
            abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                   ,abfoldr#4#(f(),x25,x9))
            main#(x1) -> c_5(abfoldr#4#(f(),g(),x1))
            plus#2#(x4,0()) -> c_6()
            plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2))
        - Weak TRS:
            abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9))
            abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9))
            abfoldr#4(x8,x4,Nil()) -> Nil()
            abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9))
            main(x1) -> abfoldr#4(f(),g(),x1)
            plus#2(x4,0()) -> x4
            plus#2(x4,S(x2)) -> S(plus#2(x4,x2))
        - Signature:
            {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1
            ,g/0,c_1/1,c_2/2,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,Nil,S}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {3,6}
        by application of
          Pre({3,6}) = {1,2,4,5,7}.
        Here rules are labelled as follows:
          1: abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9))
          2: abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9))
          3: abfoldr#4#(x8,x4,Nil()) -> c_3()
          4: abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                    ,abfoldr#4#(f(),x25,x9))
          5: main#(x1) -> c_5(abfoldr#4#(f(),g(),x1))
          6: plus#2#(x4,0()) -> c_6()
          7: plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2))
* Step 26: RemoveWeakSuffixes WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9))
            abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9))
            abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                   ,abfoldr#4#(f(),x25,x9))
            main#(x1) -> c_5(abfoldr#4#(f(),g(),x1))
            plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2))
        - Weak DPs:
            abfoldr#4#(x8,x4,Nil()) -> c_3()
            plus#2#(x4,0()) -> c_6()
        - Weak TRS:
            abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9))
            abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9))
            abfoldr#4(x8,x4,Nil()) -> Nil()
            abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9))
            main(x1) -> abfoldr#4(f(),g(),x1)
            plus#2(x4,0()) -> x4
            plus#2(x4,S(x2)) -> S(plus#2(x4,x2))
        - Signature:
            {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1
            ,g/0,c_1/1,c_2/2,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,Nil,S}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9))
             -->_1 abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                          ,abfoldr#4#(f(),x25,x9)):3
             -->_1 abfoldr#4#(x8,x4,Nil()) -> c_3():6
             -->_1 abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)):1
          
          2:S:abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9))
             -->_1 plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)):5
             -->_2 abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                          ,abfoldr#4#(f(),x25,x9)):3
             -->_1 plus#2#(x4,0()) -> c_6():7
             -->_2 abfoldr#4#(x8,x4,Nil()) -> c_3():6
             -->_2 abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)):2
          
          3:S:abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                     ,abfoldr#4#(f(),x25,x9))
             -->_2 abfoldr#4#(x8,x4,Nil()) -> c_3():6
             -->_1 abfoldr#4#(x8,x4,Nil()) -> c_3():6
             -->_2 abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                          ,abfoldr#4#(f(),x25,x9)):3
             -->_2 abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)):2
             -->_1 abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)):2
             -->_2 abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)):1
          
          4:S:main#(x1) -> c_5(abfoldr#4#(f(),g(),x1))
             -->_1 abfoldr#4#(x8,x4,Nil()) -> c_3():6
             -->_1 abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                          ,abfoldr#4#(f(),x25,x9)):3
             -->_1 abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)):1
          
          5:S:plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2))
             -->_1 plus#2#(x4,0()) -> c_6():7
             -->_1 plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)):5
          
          6:W:abfoldr#4#(x8,x4,Nil()) -> c_3()
             
          
          7:W:plus#2#(x4,0()) -> c_6()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          7: plus#2#(x4,0()) -> c_6()
          6: abfoldr#4#(x8,x4,Nil()) -> c_3()
* Step 27: UsableRules WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9))
            abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9))
            abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                   ,abfoldr#4#(f(),x25,x9))
            main#(x1) -> c_5(abfoldr#4#(f(),g(),x1))
            plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2))
        - Weak TRS:
            abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9))
            abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9))
            abfoldr#4(x8,x4,Nil()) -> Nil()
            abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9))
            main(x1) -> abfoldr#4(f(),g(),x1)
            plus#2(x4,0()) -> x4
            plus#2(x4,S(x2)) -> S(plus#2(x4,x2))
        - Signature:
            {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1
            ,g/0,c_1/1,c_2/2,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,Nil,S}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9))
          abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9))
          abfoldr#4(x8,x4,Nil()) -> Nil()
          abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9))
          plus#2(x4,0()) -> x4
          plus#2(x4,S(x2)) -> S(plus#2(x4,x2))
          abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9))
          abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9))
          abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                 ,abfoldr#4#(f(),x25,x9))
          main#(x1) -> c_5(abfoldr#4#(f(),g(),x1))
          plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2))
* Step 28: DecomposeDG WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9))
            abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9))
            abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                   ,abfoldr#4#(f(),x25,x9))
            main#(x1) -> c_5(abfoldr#4#(f(),g(),x1))
            plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2))
        - Weak TRS:
            abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9))
            abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9))
            abfoldr#4(x8,x4,Nil()) -> Nil()
            abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9))
            plus#2(x4,0()) -> x4
            plus#2(x4,S(x2)) -> S(plus#2(x4,x2))
        - Signature:
            {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1
            ,g/0,c_1/1,c_2/2,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,Nil,S}
    + Applied Processor:
        DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
    + Details:
        We decompose the input problem according to the dependency graph into the upper component
          abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9))
          abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9))
          abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                 ,abfoldr#4#(f(),x25,x9))
          main#(x1) -> c_5(abfoldr#4#(f(),g(),x1))
        and a lower component
          plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2))
        Further, following extension rules are added to the lower component.
          abfoldr#4#(x25,g(),Bcons(x20,x9)) -> abfoldr#4#(x25,g(),x9)
          abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> abfoldr#4#(x41,fb(x12),x9)
          abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> plus#2#(x8,x12)
          abfoldr#4#(f(),x25,Acons(x8,x9)) -> abfoldr#4#(f(),x25,x9)
          abfoldr#4#(f(),x25,Acons(x8,x9)) -> abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
          main#(x1) -> abfoldr#4#(f(),g(),x1)
** Step 28.a:1: SimplifyRHS WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9))
            abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9))
            abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                   ,abfoldr#4#(f(),x25,x9))
            main#(x1) -> c_5(abfoldr#4#(f(),g(),x1))
        - Weak TRS:
            abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9))
            abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9))
            abfoldr#4(x8,x4,Nil()) -> Nil()
            abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9))
            plus#2(x4,0()) -> x4
            plus#2(x4,S(x2)) -> S(plus#2(x4,x2))
        - Signature:
            {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1
            ,g/0,c_1/1,c_2/2,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,Nil,S}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9))
             -->_1 abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                          ,abfoldr#4#(f(),x25,x9)):3
             -->_1 abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)):1
          
          2:S:abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9))
             -->_2 abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                          ,abfoldr#4#(f(),x25,x9)):3
             -->_2 abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)):2
          
          3:S:abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                     ,abfoldr#4#(f(),x25,x9))
             -->_2 abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                          ,abfoldr#4#(f(),x25,x9)):3
             -->_2 abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)):2
             -->_1 abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)):2
             -->_2 abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)):1
          
          4:S:main#(x1) -> c_5(abfoldr#4#(f(),g(),x1))
             -->_1 abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                          ,abfoldr#4#(f(),x25,x9)):3
             -->_1 abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)):1
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(abfoldr#4#(x41,fb(x12),x9))
** Step 28.a:2: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9))
            abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(abfoldr#4#(x41,fb(x12),x9))
            abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                   ,abfoldr#4#(f(),x25,x9))
            main#(x1) -> c_5(abfoldr#4#(f(),g(),x1))
        - Weak TRS:
            abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9))
            abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9))
            abfoldr#4(x8,x4,Nil()) -> Nil()
            abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9))
            plus#2(x4,0()) -> x4
            plus#2(x4,S(x2)) -> S(plus#2(x4,x2))
        - Signature:
            {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1
            ,g/0,c_1/1,c_2/1,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,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(c_1) = {1},
          uargs(c_2) = {1},
          uargs(c_4) = {1,2},
          uargs(c_5) = {1}
        
        Following symbols are considered usable:
          {abfoldr#4#,main#}
        TcT has computed the following interpretation:
                   p(0) = [0]                  
               p(Acons) = [1] x1 + [1] x2 + [0]
               p(Bcons) = [1] x1 + [1] x2 + [0]
                 p(Nil) = [0]                  
                   p(S) = [1] x1 + [0]         
           p(abfoldr#4) = [0]                  
                   p(f) = [0]                  
                  p(fa) = [0]                  
                  p(fb) = [0]                  
                   p(g) = [0]                  
                p(main) = [0]                  
              p(plus#2) = [0]                  
          p(abfoldr#4#) = [0]                  
               p(main#) = [1]                  
             p(plus#2#) = [0]                  
                 p(c_1) = [4] x1 + [0]         
                 p(c_2) = [4] x1 + [0]         
                 p(c_3) = [0]                  
                 p(c_4) = [1] x1 + [4] x2 + [0]
                 p(c_5) = [2] x1 + [0]         
                 p(c_6) = [0]                  
                 p(c_7) = [0]                  
        
        Following rules are strictly oriented:
        main#(x1) = [1]                        
                  > [0]                        
                  = c_5(abfoldr#4#(f(),g(),x1))
        
        
        Following rules are (at-least) weakly oriented:
           abfoldr#4#(x25,g(),Bcons(x20,x9)) =  [0]                                                                      
                                             >= [0]                                                                      
                                             =  c_1(abfoldr#4#(x25,g(),x9))                                              
        
        abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) =  [0]                                                                      
                                             >= [0]                                                                      
                                             =  c_2(abfoldr#4#(x41,fb(x12),x9))                                          
        
            abfoldr#4#(f(),x25,Acons(x8,x9)) =  [0]                                                                      
                                             >= [0]                                                                      
                                             =  c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)),abfoldr#4#(f(),x25,x9))
        
** Step 28.a:3: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9))
            abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(abfoldr#4#(x41,fb(x12),x9))
            abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                   ,abfoldr#4#(f(),x25,x9))
        - Weak DPs:
            main#(x1) -> c_5(abfoldr#4#(f(),g(),x1))
        - Weak TRS:
            abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9))
            abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9))
            abfoldr#4(x8,x4,Nil()) -> Nil()
            abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9))
            plus#2(x4,0()) -> x4
            plus#2(x4,S(x2)) -> S(plus#2(x4,x2))
        - Signature:
            {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1
            ,g/0,c_1/1,c_2/1,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,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(c_1) = {1},
          uargs(c_2) = {1},
          uargs(c_4) = {1,2},
          uargs(c_5) = {1}
        
        Following symbols are considered usable:
          {abfoldr#4,abfoldr#4#,main#}
        TcT has computed the following interpretation:
                   p(0) = [2]                  
               p(Acons) = [1] x1 + [1] x2 + [1]
               p(Bcons) = [1] x2 + [0]         
                 p(Nil) = [0]                  
                   p(S) = [4]                  
           p(abfoldr#4) = [0]                  
                   p(f) = [0]                  
                  p(fa) = [4]                  
                  p(fb) = [1] x1 + [2]         
                   p(g) = [8]                  
                p(main) = [1] x1 + [2]         
              p(plus#2) = [3] x2 + [8]         
          p(abfoldr#4#) = [2] x3 + [0]         
               p(main#) = [3] x1 + [5]         
             p(plus#2#) = [1] x1 + [1] x2 + [2]
                 p(c_1) = [1] x1 + [0]         
                 p(c_2) = [1] x1 + [0]         
                 p(c_3) = [1]                  
                 p(c_4) = [1] x1 + [1] x2 + [0]
                 p(c_5) = [1] x1 + [5]         
                 p(c_6) = [0]                  
                 p(c_7) = [1] x1 + [0]         
        
        Following rules are strictly oriented:
        abfoldr#4#(f(),x25,Acons(x8,x9)) = [2] x8 + [2] x9 + [2]                                                    
                                         > [2] x9 + [0]                                                             
                                         = c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)),abfoldr#4#(f(),x25,x9))
        
        
        Following rules are (at-least) weakly oriented:
           abfoldr#4#(x25,g(),Bcons(x20,x9)) =  [2] x9 + [0]                                   
                                             >= [2] x9 + [0]                                   
                                             =  c_1(abfoldr#4#(x25,g(),x9))                    
        
        abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) =  [2] x9 + [0]                                   
                                             >= [2] x9 + [0]                                   
                                             =  c_2(abfoldr#4#(x41,fb(x12),x9))                
        
                                   main#(x1) =  [3] x1 + [5]                                   
                                             >= [2] x1 + [5]                                   
                                             =  c_5(abfoldr#4#(f(),g(),x1))                    
        
            abfoldr#4(x25,g(),Bcons(x20,x9)) =  [0]                                            
                                             >= [0]                                            
                                             =  Bcons(x20,abfoldr#4(x25,g(),x9))               
        
         abfoldr#4(x41,fb(x12),Bcons(x8,x9)) =  [0]                                            
                                             >= [0]                                            
                                             =  Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9))
        
                      abfoldr#4(x8,x4,Nil()) =  [0]                                            
                                             >= [0]                                            
                                             =  Nil()                                          
        
             abfoldr#4(f(),x25,Acons(x8,x9)) =  [0]                                            
                                             >= [0]                                            
                                             =  abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9))   
        
** Step 28.a:4: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9))
            abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(abfoldr#4#(x41,fb(x12),x9))
        - Weak DPs:
            abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                   ,abfoldr#4#(f(),x25,x9))
            main#(x1) -> c_5(abfoldr#4#(f(),g(),x1))
        - Weak TRS:
            abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9))
            abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9))
            abfoldr#4(x8,x4,Nil()) -> Nil()
            abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9))
            plus#2(x4,0()) -> x4
            plus#2(x4,S(x2)) -> S(plus#2(x4,x2))
        - Signature:
            {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1
            ,g/0,c_1/1,c_2/1,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,Nil,S}
    + Applied Processor:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(c_1) = {1},
          uargs(c_2) = {1},
          uargs(c_4) = {1,2},
          uargs(c_5) = {1}
        
        Following symbols are considered usable:
          {abfoldr#4,abfoldr#4#,main#}
        TcT has computed the following interpretation:
                   p(0) = 2                        
               p(Acons) = x2                       
               p(Bcons) = 2 + x2                   
                 p(Nil) = 2                        
                   p(S) = 0                        
           p(abfoldr#4) = x1*x3 + x3               
                   p(f) = 1                        
                  p(fa) = 0                        
                  p(fb) = 0                        
                   p(g) = 1                        
                p(main) = x1 + x1^2                
              p(plus#2) = 1 + 2*x1 + 2*x1*x2 + 2*x2
          p(abfoldr#4#) = x1 + x2*x3 + x2^2        
               p(main#) = 3 + 2*x1                 
             p(plus#2#) = 1                        
                 p(c_1) = x1                       
                 p(c_2) = x1                       
                 p(c_3) = 0                        
                 p(c_4) = x1 + x2                  
                 p(c_5) = 1 + x1                   
                 p(c_6) = 0                        
                 p(c_7) = 2                        
        
        Following rules are strictly oriented:
        abfoldr#4#(x25,g(),Bcons(x20,x9)) = 3 + x25 + x9               
                                          > 1 + x25 + x9               
                                          = c_1(abfoldr#4#(x25,g(),x9))
        
        
        Following rules are (at-least) weakly oriented:
        abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) =  x41                                                                      
                                             >= x41                                                                      
                                             =  c_2(abfoldr#4#(x41,fb(x12),x9))                                          
        
            abfoldr#4#(f(),x25,Acons(x8,x9)) =  1 + x25*x9 + x25^2                                                       
                                             >= 1 + x25*x9 + x25^2                                                       
                                             =  c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)),abfoldr#4#(f(),x25,x9))
        
                                   main#(x1) =  3 + 2*x1                                                                 
                                             >= 3 + x1                                                                   
                                             =  c_5(abfoldr#4#(f(),g(),x1))                                              
        
            abfoldr#4(x25,g(),Bcons(x20,x9)) =  2 + 2*x25 + x25*x9 + x9                                                  
                                             >= 2 + x25*x9 + x9                                                          
                                             =  Bcons(x20,abfoldr#4(x25,g(),x9))                                         
        
         abfoldr#4(x41,fb(x12),Bcons(x8,x9)) =  2 + 2*x41 + x41*x9 + x9                                                  
                                             >= 2 + x41*x9 + x9                                                          
                                             =  Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9))                          
        
                      abfoldr#4(x8,x4,Nil()) =  2 + 2*x8                                                                 
                                             >= 2                                                                        
                                             =  Nil()                                                                    
        
             abfoldr#4(f(),x25,Acons(x8,x9)) =  2*x9                                                                     
                                             >= 2*x9                                                                     
                                             =  abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9))                             
        
** Step 28.a:5: MI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(abfoldr#4#(x41,fb(x12),x9))
        - Weak DPs:
            abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9))
            abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                   ,abfoldr#4#(f(),x25,x9))
            main#(x1) -> c_5(abfoldr#4#(f(),g(),x1))
        - Weak TRS:
            abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9))
            abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9))
            abfoldr#4(x8,x4,Nil()) -> Nil()
            abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9))
            plus#2(x4,0()) -> x4
            plus#2(x4,S(x2)) -> S(plus#2(x4,x2))
        - Signature:
            {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1
            ,g/0,c_1/1,c_2/1,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,Nil,S}
    + Applied Processor:
        MI {miKind = Automaton (Just 2), miDimension = 4, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind Automaton (Just 2):
        
        The following argument positions are considered usable:
          uargs(c_1) = {1},
          uargs(c_2) = {1},
          uargs(c_4) = {1,2},
          uargs(c_5) = {1}
        
        Following symbols are considered usable:
          {abfoldr#4,abfoldr#4#,main#}
        TcT has computed the following interpretation:
                   p(0) = [0]                                                
                          [0]                                                
                          [0]                                                
                          [0]                                                
               p(Acons) = [1 0 0 0]       [1]                                
                          [0 1 1 0] x_2 + [1]                                
                          [0 0 1 0]       [0]                                
                          [0 0 0 0]       [0]                                
               p(Bcons) = [0 0 0 0]       [0]                                
                          [0 1 0 0] x_2 + [1]                                
                          [0 0 1 0]       [1]                                
                          [0 0 0 0]       [0]                                
                 p(Nil) = [1]                                                
                          [0]                                                
                          [0]                                                
                          [0]                                                
                   p(S) = [1 0 0 0]       [1]                                
                          [0 0 1 0] x_1 + [0]                                
                          [0 0 0 0]       [0]                                
                          [0 0 0 1]       [0]                                
           p(abfoldr#4) = [0 0 0 0]       [1 0 0 0]       [1 0 0 0]       [0]
                          [1 0 0 0] x_1 + [0 0 0 0] x_2 + [0 0 1 0] x_3 + [0]
                          [0 1 0 0]       [0 0 0 0]       [0 0 1 0]       [0]
                          [0 0 0 0]       [1 0 0 0]       [1 0 0 0]       [1]
                   p(f) = [1]                                                
                          [0]                                                
                          [0]                                                
                          [1]                                                
                  p(fa) = [0]                                                
                          [0]                                                
                          [1]                                                
                          [0]                                                
                  p(fb) = [0 0 0 0]       [1]                                
                          [0 1 1 1] x_1 + [0]                                
                          [0 1 1 1]       [0]                                
                          [0 1 0 1]       [1]                                
                   p(g) = [0]                                                
                          [1]                                                
                          [1]                                                
                          [1]                                                
                p(main) = [0]                                                
                          [0]                                                
                          [0]                                                
                          [0]                                                
              p(plus#2) = [0 0 1 1]       [1 0 0 1]       [0]                
                          [0 0 0 0] x_1 + [0 0 0 0] x_2 + [0]                
                          [0 0 0 0]       [0 0 0 0]       [1]                
                          [0 0 0 0]       [1 0 0 0]       [0]                
          p(abfoldr#4#) = [0 0 0 1]       [0 0 0 0]       [0 1 0 0]       [0]
                          [0 0 1 0] x_1 + [0 1 0 1] x_2 + [0 0 0 0] x_3 + [0]
                          [0 0 0 0]       [0 1 1 1]       [0 0 0 0]       [0]
                          [1 0 0 1]       [0 1 0 0]       [0 0 0 0]       [0]
               p(main#) = [0 1 1 0]       [1]                                
                          [0 0 0 0] x_1 + [1]                                
                          [0 0 0 0]       [1]                                
                          [0 0 0 0]       [1]                                
             p(plus#2#) = [0]                                                
                          [0]                                                
                          [0]                                                
                          [0]                                                
                 p(c_1) = [1 0 0 0]       [1]                                
                          [0 1 0 0] x_1 + [0]                                
                          [0 0 0 0]       [1]                                
                          [0 0 0 0]       [0]                                
                 p(c_2) = [1 0 0 0]       [0]                                
                          [0 1 0 0] x_1 + [0]                                
                          [0 0 0 0]       [0]                                
                          [0 0 0 0]       [0]                                
                 p(c_3) = [0]                                                
                          [0]                                                
                          [0]                                                
                          [0]                                                
                 p(c_4) = [1 0 0 0]       [1 0 0 0]       [0]                
                          [0 0 0 0] x_1 + [0 0 0 0] x_2 + [0]                
                          [0 0 0 0]       [0 1 0 0]       [0]                
                          [0 0 0 0]       [0 0 0 0]       [0]                
                 p(c_5) = [1 0 0 0]       [0]                                
                          [0 0 0 0] x_1 + [0]                                
                          [0 0 0 0]       [0]                                
                          [0 0 0 0]       [0]                                
                 p(c_6) = [0]                                                
                          [0]                                                
                          [0]                                                
                          [0]                                                
                 p(c_7) = [0]                                                
                          [0]                                                
                          [0]                                                
                          [0]                                                
        
        Following rules are strictly oriented:
        abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) = [0 0 0 0]       [0 0 0 1]       [0 1 0 0]      [1]
                                               [0 2 1 2] x12 + [0 0 1 0] x41 + [0 0 0 0] x9 + [1]
                                               [0 3 2 3]       [0 0 0 0]       [0 0 0 0]      [1]
                                               [0 1 1 1]       [1 0 0 1]       [0 0 0 0]      [0]
                                             > [0 0 0 0]       [0 0 0 1]       [0 1 0 0]      [0]
                                               [0 2 1 2] x12 + [0 0 1 0] x41 + [0 0 0 0] x9 + [1]
                                               [0 0 0 0]       [0 0 0 0]       [0 0 0 0]      [0]
                                               [0 0 0 0]       [0 0 0 0]       [0 0 0 0]      [0]
                                             = c_2(abfoldr#4#(x41,fb(x12),x9))                   
        
        
        Following rules are (at-least) weakly oriented:
          abfoldr#4#(x25,g(),Bcons(x20,x9)) =  [0 0 0 1]       [0 1 0 0]      [1]                                       
                                               [0 0 1 0] x25 + [0 0 0 0] x9 + [2]                                       
                                               [0 0 0 0]       [0 0 0 0]      [3]                                       
                                               [1 0 0 1]       [0 0 0 0]      [1]                                       
                                            >= [0 0 0 1]       [0 1 0 0]      [1]                                       
                                               [0 0 1 0] x25 + [0 0 0 0] x9 + [2]                                       
                                               [0 0 0 0]       [0 0 0 0]      [1]                                       
                                               [0 0 0 0]       [0 0 0 0]      [0]                                       
                                            =  c_1(abfoldr#4#(x25,g(),x9))                                              
        
           abfoldr#4#(f(),x25,Acons(x8,x9)) =  [0 0 0 0]       [0 1 1 0]      [2]                                       
                                               [0 1 0 1] x25 + [0 0 0 0] x9 + [0]                                       
                                               [0 1 1 1]       [0 0 0 0]      [0]                                       
                                               [0 1 0 0]       [0 0 0 0]      [2]                                       
                                            >= [0 0 0 0]       [0 1 1 0]      [2]                                       
                                               [0 0 0 0] x25 + [0 0 0 0] x9 + [0]                                       
                                               [0 1 0 1]       [0 0 0 0]      [0]                                       
                                               [0 0 0 0]       [0 0 0 0]      [0]                                       
                                            =  c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)),abfoldr#4#(f(),x25,x9))
        
                                  main#(x1) =  [0 1 1 0]      [1]                                                       
                                               [0 0 0 0] x1 + [1]                                                       
                                               [0 0 0 0]      [1]                                                       
                                               [0 0 0 0]      [1]                                                       
                                            >= [0 1 0 0]      [1]                                                       
                                               [0 0 0 0] x1 + [0]                                                       
                                               [0 0 0 0]      [0]                                                       
                                               [0 0 0 0]      [0]                                                       
                                            =  c_5(abfoldr#4#(f(),g(),x1))                                              
        
           abfoldr#4(x25,g(),Bcons(x20,x9)) =  [0 0 0 0]       [0 0 0 0]      [0]                                       
                                               [1 0 0 0] x25 + [0 0 1 0] x9 + [1]                                       
                                               [0 1 0 0]       [0 0 1 0]      [1]                                       
                                               [0 0 0 0]       [0 0 0 0]      [1]                                       
                                            >= [0 0 0 0]       [0 0 0 0]      [0]                                       
                                               [1 0 0 0] x25 + [0 0 1 0] x9 + [1]                                       
                                               [0 1 0 0]       [0 0 1 0]      [1]                                       
                                               [0 0 0 0]       [0 0 0 0]      [0]                                       
                                            =  Bcons(x20,abfoldr#4(x25,g(),x9))                                         
        
        abfoldr#4(x41,fb(x12),Bcons(x8,x9)) =  [0 0 0 0]       [0 0 0 0]      [1]                                       
                                               [1 0 0 0] x41 + [0 0 1 0] x9 + [1]                                       
                                               [0 1 0 0]       [0 0 1 0]      [1]                                       
                                               [0 0 0 0]       [0 0 0 0]      [2]                                       
                                            >= [0 0 0 0]       [0 0 0 0]      [0]                                       
                                               [1 0 0 0] x41 + [0 0 1 0] x9 + [1]                                       
                                               [0 1 0 0]       [0 0 1 0]      [1]                                       
                                               [0 0 0 0]       [0 0 0 0]      [0]                                       
                                            =  Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9))                          
        
                     abfoldr#4(x8,x4,Nil()) =  [1 0 0 0]      [0 0 0 0]      [1]                                        
                                               [0 0 0 0] x4 + [1 0 0 0] x8 + [0]                                        
                                               [0 0 0 0]      [0 1 0 0]      [0]                                        
                                               [1 0 0 0]      [0 0 0 0]      [2]                                        
                                            >= [1]                                                                      
                                               [0]                                                                      
                                               [0]                                                                      
                                               [0]                                                                      
                                            =  Nil()                                                                    
        
            abfoldr#4(f(),x25,Acons(x8,x9)) =  [1 0 0 0]       [1 0 0 0]      [1]                                       
                                               [0 0 0 0] x25 + [0 0 1 0] x9 + [1]                                       
                                               [0 0 0 0]       [0 0 1 0]      [0]                                       
                                               [1 0 0 0]       [1 0 0 0]      [2]                                       
                                            >= [1 0 0 0]       [1 0 0 0]      [1]                                       
                                               [0 0 0 0] x25 + [0 0 1 0] x9 + [0]                                       
                                               [0 0 0 0]       [0 0 1 0]      [0]                                       
                                               [1 0 0 0]       [1 0 0 0]      [2]                                       
                                            =  abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9))                             
        
** Step 28.a:6: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9))
            abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(abfoldr#4#(x41,fb(x12),x9))
            abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
                                                   ,abfoldr#4#(f(),x25,x9))
            main#(x1) -> c_5(abfoldr#4#(f(),g(),x1))
        - Weak TRS:
            abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9))
            abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9))
            abfoldr#4(x8,x4,Nil()) -> Nil()
            abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9))
            plus#2(x4,0()) -> x4
            plus#2(x4,S(x2)) -> S(plus#2(x4,x2))
        - Signature:
            {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1
            ,g/0,c_1/1,c_2/1,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,Nil,S}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

** Step 28.b:1: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2))
        - Weak DPs:
            abfoldr#4#(x25,g(),Bcons(x20,x9)) -> abfoldr#4#(x25,g(),x9)
            abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> abfoldr#4#(x41,fb(x12),x9)
            abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> plus#2#(x8,x12)
            abfoldr#4#(f(),x25,Acons(x8,x9)) -> abfoldr#4#(f(),x25,x9)
            abfoldr#4#(f(),x25,Acons(x8,x9)) -> abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
            main#(x1) -> abfoldr#4#(f(),g(),x1)
        - Weak TRS:
            abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9))
            abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9))
            abfoldr#4(x8,x4,Nil()) -> Nil()
            abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9))
            plus#2(x4,0()) -> x4
            plus#2(x4,S(x2)) -> S(plus#2(x4,x2))
        - Signature:
            {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1
            ,g/0,c_1/1,c_2/2,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,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(c_7) = {1}
        
        Following symbols are considered usable:
          {abfoldr#4,abfoldr#4#,main#,plus#2#}
        TcT has computed the following interpretation:
                   p(0) = [0]                           
               p(Acons) = [1] x1 + [1] x2 + [0]         
               p(Bcons) = [1] x2 + [0]                  
                 p(Nil) = [0]                           
                   p(S) = [1] x1 + [8]                  
           p(abfoldr#4) = [0]                           
                   p(f) = [2]                           
                  p(fa) = [1]                           
                  p(fb) = [2] x1 + [2]                  
                   p(g) = [1]                           
                p(main) = [1] x1 + [2]                  
              p(plus#2) = [0]                           
          p(abfoldr#4#) = [2] x1 + [1] x2 + [2] x3 + [7]
               p(main#) = [2] x1 + [14]                 
             p(plus#2#) = [1] x2 + [0]                  
                 p(c_1) = [0]                           
                 p(c_2) = [0]                           
                 p(c_3) = [0]                           
                 p(c_4) = [0]                           
                 p(c_5) = [0]                           
                 p(c_6) = [0]                           
                 p(c_7) = [1] x1 + [7]                  
        
        Following rules are strictly oriented:
        plus#2#(x4,S(x2)) = [1] x2 + [8]       
                          > [1] x2 + [7]       
                          = c_7(plus#2#(x4,x2))
        
        
        Following rules are (at-least) weakly oriented:
           abfoldr#4#(x25,g(),Bcons(x20,x9)) =  [2] x25 + [2] x9 + [8]                         
                                             >= [2] x25 + [2] x9 + [8]                         
                                             =  abfoldr#4#(x25,g(),x9)                         
        
        abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) =  [2] x12 + [2] x41 + [2] x9 + [9]               
                                             >= [2] x12 + [2] x41 + [2] x9 + [9]               
                                             =  abfoldr#4#(x41,fb(x12),x9)                     
        
        abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) =  [2] x12 + [2] x41 + [2] x9 + [9]               
                                             >= [1] x12 + [0]                                  
                                             =  plus#2#(x8,x12)                                
        
            abfoldr#4#(f(),x25,Acons(x8,x9)) =  [1] x25 + [2] x8 + [2] x9 + [11]               
                                             >= [1] x25 + [2] x9 + [11]                        
                                             =  abfoldr#4#(f(),x25,x9)                         
        
            abfoldr#4#(f(),x25,Acons(x8,x9)) =  [1] x25 + [2] x8 + [2] x9 + [11]               
                                             >= [2] x8 + [11]                                  
                                             =  abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))  
        
                                   main#(x1) =  [2] x1 + [14]                                  
                                             >= [2] x1 + [12]                                  
                                             =  abfoldr#4#(f(),g(),x1)                         
        
            abfoldr#4(x25,g(),Bcons(x20,x9)) =  [0]                                            
                                             >= [0]                                            
                                             =  Bcons(x20,abfoldr#4(x25,g(),x9))               
        
         abfoldr#4(x41,fb(x12),Bcons(x8,x9)) =  [0]                                            
                                             >= [0]                                            
                                             =  Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9))
        
                      abfoldr#4(x8,x4,Nil()) =  [0]                                            
                                             >= [0]                                            
                                             =  Nil()                                          
        
             abfoldr#4(f(),x25,Acons(x8,x9)) =  [0]                                            
                                             >= [0]                                            
                                             =  abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9))   
        
** Step 28.b:2: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            abfoldr#4#(x25,g(),Bcons(x20,x9)) -> abfoldr#4#(x25,g(),x9)
            abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> abfoldr#4#(x41,fb(x12),x9)
            abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> plus#2#(x8,x12)
            abfoldr#4#(f(),x25,Acons(x8,x9)) -> abfoldr#4#(f(),x25,x9)
            abfoldr#4#(f(),x25,Acons(x8,x9)) -> abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9))
            main#(x1) -> abfoldr#4#(f(),g(),x1)
            plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2))
        - Weak TRS:
            abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9))
            abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9))
            abfoldr#4(x8,x4,Nil()) -> Nil()
            abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9))
            plus#2(x4,0()) -> x4
            plus#2(x4,S(x2)) -> S(plus#2(x4,x2))
        - Signature:
            {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1
            ,g/0,c_1/1,c_2/2,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,Nil,S}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^3))