WORST_CASE(?,O(n^2))
* Step 1: Desugar WORST_CASE(?,O(n^2))
    + Considered Problem:
        type bool = True | False
        ;;
        type 'a option = None | Some of 'a
        ;;
        type 'a list = Nil | Cons of 'a * 'a list
        ;;
        type Unit = Unit
        
        ;;
        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)
        ;;
        type ('a,'b) pair = Pair of 'a * 'b
        
        (* * * * * * * * * * *
         * Resource Aware ML *
         * * * * * * * * * * *
         *
         * * *  Use Cases * *
         *
         * File:
         *   example/calculator.raml
         *
         * Author:
         *   Jan Hoffmann (S(S(0))015)
         *
         * Description:
         *   An evaluator for simple arithmetic expressions.
         *
         *)
        
        
        ;;
        type nat = Zero | Succ of nat
        ;;
        type expr = Nat of nat
                  | Add of expr * expr
                  | Sub of expr * expr
        ;;
        let rec add n1 n2 =
          match n1 with
            | Zero()-> n2
            | Succ(n) -> Succ(add n n2)
        
        ;;
        let rec sub n1 n2 =
          match n2 with
            | Zero()-> n1
            | Succ(n2') ->
              match n1 with
        	| Zero()-> Zero
        	| Succ(n1') ->
        	  sub n1' n2'
        
        ;;
        let rec mult n1 n2 =
          match n1 with
            | Zero()-> Zero
            | Succ(n) ->
              add n (mult n n2)
        
        ;;
        let eval_simpl expr =
          let rec eval expr =
            match expr with
              | Nat(n) -> n
              | Add(e1,e2) ->
        	let n1 = eval e1 in
        	let n2 = eval e2 in
        	add n1 n2
              | Sub(e1,e2) ->
        	let n1 = eval e1 in
        	let n2 = eval e2 in
        	sub n1 n2
          in
          eval expr
        
        ;;
        
        let main e = eval_simpl e
                  ;;
    + Applied Processor:
        Desugar {analysedFunction = Nothing}
    + Details:
        none
* Step 2: Defunctionalization WORST_CASE(?,O(n^2))
    + Considered Problem:
        λe : expr.
          (λadd : nat -> nat -> nat.
             (λsub : nat -> nat -> nat.
                (λeval_simpl : expr -> nat. (λmain : expr -> nat. main e) (λe : expr. eval_simpl e))
                  (λexpr : expr.
                     (λeval : expr -> nat. eval expr)
                       (μeval : expr -> nat.
                          λexpr : expr.
                            case expr of
                             | Nat -> λn : nat.
                                        n
                             | Add -> λe1 : expr.
                                        λe2 : expr. (λn1 : nat. (λn2 : nat. add n1 n2) (eval e2)) (eval e1)
                             | Sub -> λe1 : expr.
                                        λe2 : expr. (λn1 : nat. (λn2 : nat. sub n1 n2) (eval e2)) (eval e1))))
               (μsub : nat -> nat -> nat.
                  λn1 : nat.
                    λn2 : nat.
                      case n2 of
                       | Zero -> n1
                       | Succ -> λn2' : nat.
                                   case n1 of  | Zero -> Zero | Succ -> λn1' : nat. sub n1' n2'))
            (μadd : nat -> nat -> nat.
               λn1 : nat. λn2 : nat. case n1 of  | Zero -> n2 | Succ -> λn : nat. Succ(add n n2)) : expr -> nat
        where
          Add    :: expr -> expr -> expr
          Cons   :: 'a -> 'a list -> 'a list
          False  :: bool
          Nat    :: nat -> expr
          Nil    :: 'a list
          None   :: 'a option
          Pair   :: 'a -> 'b -> ('a,'b) pair
          Some   :: 'a -> 'a option
          Sub    :: expr -> expr -> expr
          Succ   :: nat -> nat
          Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple
          True   :: bool
          Unit   :: Unit
          Zero   :: nat
    + Applied Processor:
        Defunctionalization
    + Details:
        none
* Step 3: Inline WORST_CASE(?,O(n^2))
    + 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: eval_simpl_expr(x3) x4 -> x4 x3
        5: eval_expr_4(x1, x7) x8 -> x1 x7 x8
        6: eval_expr_3(x1, x2, x6) x7 -> eval_expr_4(x1, x7) (eval(x1, x2) x6)
        7: eval_expr_8(x2, x7) x8 -> x2 x7 x8
        8: eval_expr_7(x1, x2, x6) x7 -> eval_expr_8(x2, x7) (eval(x1, x2) x6)
        9: cond_eval_expr(Nat(x5), x1, x2) -> x5
        10: cond_eval_expr(Add(x5, x6), x1, x2) -> eval_expr_3(x1, x2, x6) (eval(x1, x2) x5)
        11: cond_eval_expr(Sub(x5, x6), x1, x2) -> eval_expr_7(x1, x2, x6) (eval(x1, x2) x5)
        12: eval_1(x1, x2) x4 -> cond_eval_expr(x4, x1, x2)
        13: eval(x1, x2) x3 -> eval_1(x1, x2) x3
        14: eval_simpl(x1, x2) x3 -> eval_simpl_expr(x3) eval(x1, x2)
        15: main_2(x0, x1) x2 -> main_3(x0) eval_simpl(x1, x2)
        16: cond_sub_n1_n2_1(Zero(), x4) -> Zero()
        17: cond_sub_n1_n2_1(Succ(x5), x4) -> sub() x5 x4
        18: cond_sub_n1_n2(Zero(), x2) -> x2
        19: cond_sub_n1_n2(Succ(x4), x2) -> cond_sub_n1_n2_1(x2, x4)
        20: sub_n1(x2) x3 -> cond_sub_n1_n2(x3, x2)
        21: sub_1() x2 -> sub_n1(x2)
        22: sub() x0 -> sub_1() x0
        23: main_1(x0) x1 -> main_2(x0, x1) sub()
        24: cond_add_n1_n2(Zero(), x2) -> x2
        25: cond_add_n1_n2(Succ(x3), x2) -> Succ(add() x3 x2)
        26: add_n1(x1) x2 -> cond_add_n1_n2(x1, x2)
        27: add_1() x1 -> add_n1(x1)
        28: add() x0 -> add_1() x0
        29: main(x0) -> main_1(x0) add()
        where
          Add              :: expr -> expr -> expr
          Nat              :: nat -> expr
          Sub              :: expr -> expr -> expr
          Succ             :: nat -> nat
          Zero             :: nat
          eval_simpl       :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          eval_simpl_expr  :: expr -> (expr -> nat) -> nat
          add_n1           :: nat -> nat -> nat
          sub_n1           :: nat -> nat -> nat
          add_1            :: nat -> nat -> nat
          eval_1           :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          main_1           :: expr -> (nat -> nat -> nat) -> nat
          sub_1            :: nat -> nat -> nat
          main_2           :: expr -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat
          eval_expr_3      :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat -> nat
          main_3           :: expr -> (expr -> nat) -> nat
          eval_expr_4      :: (nat -> nat -> nat) -> nat -> nat -> nat
          main_4           :: expr -> (expr -> nat) -> nat
          main_5           :: (expr -> nat) -> expr -> nat
          eval_expr_7      :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat -> nat
          eval_expr_8      :: (nat -> nat -> nat) -> nat -> nat -> nat
          cond_eval_expr   :: expr -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat
          cond_add_n1_n2   :: nat -> nat -> nat
          cond_sub_n1_n2   :: nat -> nat -> nat
          cond_sub_n1_n2_1 :: nat -> nat -> nat
          add              :: nat -> nat -> nat
          eval             :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          sub              :: nat -> nat -> nat
          main             :: expr -> nat
    + Applied Processor:
        Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
    + Details:
        none
* Step 4: Inline WORST_CASE(?,O(n^2))
    + 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: eval_simpl_expr(x3) x4 -> x4 x3
        5: eval_expr_4(x1, x7) x8 -> x1 x7 x8
        6: eval_expr_3(x2, x5, x13) x14 -> x2 x14 (eval(x2, x5) x13)
        7: eval_expr_8(x2, x7) x8 -> x2 x7 x8
        8: eval_expr_7(x3, x4, x13) x14 -> x4 x14 (eval(x3, x4) x13)
        9: cond_eval_expr(Nat(x5), x1, x2) -> x5
        10: cond_eval_expr(Add(x11, x12), x2, x4) -> eval_expr_4(x2, eval(x2, x4) x11) (eval(x2, x4) x12)
        11: cond_eval_expr(Sub(x11, x12), x2, x4) -> eval_expr_8(x4, eval(x2, x4) x11) (eval(x2, x4) x12)
        12: eval_1(x1, x2) x4 -> cond_eval_expr(x4, x1, x2)
        13: eval(x2, x4) x8 -> cond_eval_expr(x8, x2, x4)
        14: eval_simpl(x3, x5) x6 -> eval(x3, x5) x6
        15: main_2(x0, x3) x5 -> main_4(x0) main_5(eval_simpl(x3, x5))
        16: cond_sub_n1_n2_1(Zero(), x4) -> Zero()
        17: cond_sub_n1_n2_1(Succ(x5), x4) -> sub() x5 x4
        18: cond_sub_n1_n2(Zero(), x2) -> x2
        19: cond_sub_n1_n2(Succ(x4), x2) -> cond_sub_n1_n2_1(x2, x4)
        20: sub_n1(x2) x3 -> cond_sub_n1_n2(x3, x2)
        21: sub_1() x2 -> sub_n1(x2)
        22: sub() x4 -> sub_n1(x4)
        23: main_1(x0) x2 -> main_3(x0) eval_simpl(x2, sub())
        24: cond_add_n1_n2(Zero(), x2) -> x2
        25: cond_add_n1_n2(Succ(x3), x2) -> Succ(add() x3 x2)
        26: add_n1(x1) x2 -> cond_add_n1_n2(x1, x2)
        27: add_1() x1 -> add_n1(x1)
        28: add() x2 -> add_n1(x2)
        29: main(x0) -> main_2(x0, add()) sub()
        where
          Add              :: expr -> expr -> expr
          Nat              :: nat -> expr
          Sub              :: expr -> expr -> expr
          Succ             :: nat -> nat
          Zero             :: nat
          eval_simpl       :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          eval_simpl_expr  :: expr -> (expr -> nat) -> nat
          add_n1           :: nat -> nat -> nat
          sub_n1           :: nat -> nat -> nat
          add_1            :: nat -> nat -> nat
          eval_1           :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          main_1           :: expr -> (nat -> nat -> nat) -> nat
          sub_1            :: nat -> nat -> nat
          main_2           :: expr -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat
          eval_expr_3      :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat -> nat
          main_3           :: expr -> (expr -> nat) -> nat
          eval_expr_4      :: (nat -> nat -> nat) -> nat -> nat -> nat
          main_4           :: expr -> (expr -> nat) -> nat
          main_5           :: (expr -> nat) -> expr -> nat
          eval_expr_7      :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat -> nat
          eval_expr_8      :: (nat -> nat -> nat) -> nat -> nat -> nat
          cond_eval_expr   :: expr -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat
          cond_add_n1_n2   :: nat -> nat -> nat
          cond_sub_n1_n2   :: nat -> nat -> nat
          cond_sub_n1_n2_1 :: nat -> nat -> nat
          add              :: nat -> nat -> nat
          eval             :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          sub              :: nat -> nat -> nat
          main             :: expr -> nat
    + Applied Processor:
        Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
    + Details:
        none
* Step 5: Inline WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: main_4(x0) x4 -> x4 x0
        2: main_5(x3) x4 -> x3 x4
        3: main_3(x8) x6 -> x6 x8
        4: eval_simpl_expr(x3) x4 -> x4 x3
        5: eval_expr_4(x1, x7) x8 -> x1 x7 x8
        6: eval_expr_3(x2, x5, x13) x14 -> x2 x14 (eval(x2, x5) x13)
        7: eval_expr_8(x2, x7) x8 -> x2 x7 x8
        8: eval_expr_7(x3, x4, x13) x14 -> x4 x14 (eval(x3, x4) x13)
        9: cond_eval_expr(Nat(x5), x1, x2) -> x5
        10: cond_eval_expr(Add(x23, x25), x2, x9) -> x2 (eval(x2, x9) x23) (eval(x2, x9) x25)
        11: cond_eval_expr(Sub(x23, x25), x5, x4) -> x4 (eval(x5, x4) x23) (eval(x5, x4) x25)
        12: eval_1(x1, x2) x4 -> cond_eval_expr(x4, x1, x2)
        13: eval(x2, x4) x8 -> cond_eval_expr(x8, x2, x4)
        14: eval_simpl(x3, x5) x6 -> eval(x3, x5) x6
        15: main_2(x0, x7) x11 -> main_5(eval_simpl(x7, x11)) x0
        16: cond_sub_n1_n2_1(Zero(), x4) -> Zero()
        17: cond_sub_n1_n2_1(Succ(x5), x4) -> sub() x5 x4
        18: cond_sub_n1_n2(Zero(), x2) -> x2
        19: cond_sub_n1_n2(Succ(x4), x2) -> cond_sub_n1_n2_1(x2, x4)
        20: sub_n1(x2) x3 -> cond_sub_n1_n2(x3, x2)
        21: sub_1() x2 -> sub_n1(x2)
        22: sub() x4 -> sub_n1(x4)
        23: main_1(x0) x5 -> main_5(eval_simpl(x5, sub())) x0
        24: cond_add_n1_n2(Zero(), x2) -> x2
        25: cond_add_n1_n2(Succ(x3), x2) -> Succ(add() x3 x2)
        26: add_n1(x1) x2 -> cond_add_n1_n2(x1, x2)
        27: add_1() x1 -> add_n1(x1)
        28: add() x2 -> add_n1(x2)
        29: main(x0) -> main_4(x0) main_5(eval_simpl(add(), sub()))
        where
          Add              :: expr -> expr -> expr
          Nat              :: nat -> expr
          Sub              :: expr -> expr -> expr
          Succ             :: nat -> nat
          Zero             :: nat
          eval_simpl       :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          eval_simpl_expr  :: expr -> (expr -> nat) -> nat
          add_n1           :: nat -> nat -> nat
          sub_n1           :: nat -> nat -> nat
          add_1            :: nat -> nat -> nat
          eval_1           :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          main_1           :: expr -> (nat -> nat -> nat) -> nat
          sub_1            :: nat -> nat -> nat
          main_2           :: expr -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat
          eval_expr_3      :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat -> nat
          main_3           :: expr -> (expr -> nat) -> nat
          eval_expr_4      :: (nat -> nat -> nat) -> nat -> nat -> nat
          main_4           :: expr -> (expr -> nat) -> nat
          main_5           :: (expr -> nat) -> expr -> nat
          eval_expr_7      :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat -> nat
          eval_expr_8      :: (nat -> nat -> nat) -> nat -> nat -> nat
          cond_eval_expr   :: expr -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat
          cond_add_n1_n2   :: nat -> nat -> nat
          cond_sub_n1_n2   :: nat -> nat -> nat
          cond_sub_n1_n2_1 :: nat -> nat -> nat
          add              :: nat -> nat -> nat
          eval             :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          sub              :: nat -> nat -> nat
          main             :: expr -> nat
    + Applied Processor:
        Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
    + Details:
        none
* Step 6: Inline WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: main_4(x0) x4 -> x4 x0
        2: main_5(x3) x4 -> x3 x4
        3: main_3(x8) x6 -> x6 x8
        4: eval_simpl_expr(x3) x4 -> x4 x3
        5: eval_expr_4(x1, x7) x8 -> x1 x7 x8
        6: eval_expr_3(x2, x5, x13) x14 -> x2 x14 (eval(x2, x5) x13)
        7: eval_expr_8(x2, x7) x8 -> x2 x7 x8
        8: eval_expr_7(x3, x4, x13) x14 -> x4 x14 (eval(x3, x4) x13)
        9: cond_eval_expr(Nat(x5), x1, x2) -> x5
        10: cond_eval_expr(Add(x23, x25), x2, x9) -> x2 (eval(x2, x9) x23) (eval(x2, x9) x25)
        11: cond_eval_expr(Sub(x23, x25), x5, x4) -> x4 (eval(x5, x4) x23) (eval(x5, x4) x25)
        12: eval_1(x1, x2) x4 -> cond_eval_expr(x4, x1, x2)
        13: eval(x2, x4) x8 -> cond_eval_expr(x8, x2, x4)
        14: eval_simpl(x3, x5) x6 -> eval(x3, x5) x6
        15: main_2(x8, x15) x23 -> eval_simpl(x15, x23) x8
        16: cond_sub_n1_n2_1(Zero(), x4) -> Zero()
        17: cond_sub_n1_n2_1(Succ(x5), x4) -> sub() x5 x4
        18: cond_sub_n1_n2(Zero(), x2) -> x2
        19: cond_sub_n1_n2(Succ(x4), x2) -> cond_sub_n1_n2_1(x2, x4)
        20: sub_n1(x2) x3 -> cond_sub_n1_n2(x3, x2)
        21: sub_1() x2 -> sub_n1(x2)
        22: sub() x4 -> sub_n1(x4)
        23: main_1(x8) x11 -> eval_simpl(x11, sub()) x8
        24: cond_add_n1_n2(Zero(), x2) -> x2
        25: cond_add_n1_n2(Succ(x3), x2) -> Succ(add() x3 x2)
        26: add_n1(x1) x2 -> cond_add_n1_n2(x1, x2)
        27: add_1() x1 -> add_n1(x1)
        28: add() x2 -> add_n1(x2)
        29: main(x0) -> main_5(eval_simpl(add(), sub())) x0
        where
          Add              :: expr -> expr -> expr
          Nat              :: nat -> expr
          Sub              :: expr -> expr -> expr
          Succ             :: nat -> nat
          Zero             :: nat
          eval_simpl       :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          eval_simpl_expr  :: expr -> (expr -> nat) -> nat
          add_n1           :: nat -> nat -> nat
          sub_n1           :: nat -> nat -> nat
          add_1            :: nat -> nat -> nat
          eval_1           :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          main_1           :: expr -> (nat -> nat -> nat) -> nat
          sub_1            :: nat -> nat -> nat
          main_2           :: expr -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat
          eval_expr_3      :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat -> nat
          main_3           :: expr -> (expr -> nat) -> nat
          eval_expr_4      :: (nat -> nat -> nat) -> nat -> nat -> nat
          main_4           :: expr -> (expr -> nat) -> nat
          main_5           :: (expr -> nat) -> expr -> nat
          eval_expr_7      :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat -> nat
          eval_expr_8      :: (nat -> nat -> nat) -> nat -> nat -> nat
          cond_eval_expr   :: expr -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat
          cond_add_n1_n2   :: nat -> nat -> nat
          cond_sub_n1_n2   :: nat -> nat -> nat
          cond_sub_n1_n2_1 :: nat -> nat -> nat
          add              :: nat -> nat -> nat
          eval             :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          sub              :: nat -> nat -> nat
          main             :: expr -> nat
    + Applied Processor:
        Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
    + Details:
        none
* Step 7: Inline WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: main_4(x0) x4 -> x4 x0
        2: main_5(x3) x4 -> x3 x4
        3: main_3(x8) x6 -> x6 x8
        4: eval_simpl_expr(x3) x4 -> x4 x3
        5: eval_expr_4(x1, x7) x8 -> x1 x7 x8
        6: eval_expr_3(x2, x5, x13) x14 -> x2 x14 (eval(x2, x5) x13)
        7: eval_expr_8(x2, x7) x8 -> x2 x7 x8
        8: eval_expr_7(x3, x4, x13) x14 -> x4 x14 (eval(x3, x4) x13)
        9: cond_eval_expr(Nat(x5), x1, x2) -> x5
        10: cond_eval_expr(Add(x23, x25), x2, x9) -> x2 (eval(x2, x9) x23) (eval(x2, x9) x25)
        11: cond_eval_expr(Sub(x23, x25), x5, x4) -> x4 (eval(x5, x4) x23) (eval(x5, x4) x25)
        12: eval_1(x1, x2) x4 -> cond_eval_expr(x4, x1, x2)
        13: eval(x2, x4) x8 -> cond_eval_expr(x8, x2, x4)
        14: eval_simpl(x3, x5) x6 -> eval(x3, x5) x6
        15: main_2(x12, x6) x10 -> eval(x6, x10) x12
        16: cond_sub_n1_n2_1(Zero(), x4) -> Zero()
        17: cond_sub_n1_n2_1(Succ(x5), x4) -> sub() x5 x4
        18: cond_sub_n1_n2(Zero(), x2) -> x2
        19: cond_sub_n1_n2(Succ(x4), x2) -> cond_sub_n1_n2_1(x2, x4)
        20: sub_n1(x2) x3 -> cond_sub_n1_n2(x3, x2)
        21: sub_1() x2 -> sub_n1(x2)
        22: sub() x4 -> sub_n1(x4)
        23: main_1(x12) x6 -> eval(x6, sub()) x12
        24: cond_add_n1_n2(Zero(), x2) -> x2
        25: cond_add_n1_n2(Succ(x3), x2) -> Succ(add() x3 x2)
        26: add_n1(x1) x2 -> cond_add_n1_n2(x1, x2)
        27: add_1() x1 -> add_n1(x1)
        28: add() x2 -> add_n1(x2)
        29: main(x8) -> eval_simpl(add(), sub()) x8
        where
          Add              :: expr -> expr -> expr
          Nat              :: nat -> expr
          Sub              :: expr -> expr -> expr
          Succ             :: nat -> nat
          Zero             :: nat
          eval_simpl       :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          eval_simpl_expr  :: expr -> (expr -> nat) -> nat
          add_n1           :: nat -> nat -> nat
          sub_n1           :: nat -> nat -> nat
          add_1            :: nat -> nat -> nat
          eval_1           :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          main_1           :: expr -> (nat -> nat -> nat) -> nat
          sub_1            :: nat -> nat -> nat
          main_2           :: expr -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat
          eval_expr_3      :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat -> nat
          main_3           :: expr -> (expr -> nat) -> nat
          eval_expr_4      :: (nat -> nat -> nat) -> nat -> nat -> nat
          main_4           :: expr -> (expr -> nat) -> nat
          main_5           :: (expr -> nat) -> expr -> nat
          eval_expr_7      :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat -> nat
          eval_expr_8      :: (nat -> nat -> nat) -> nat -> nat -> nat
          cond_eval_expr   :: expr -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat
          cond_add_n1_n2   :: nat -> nat -> nat
          cond_sub_n1_n2   :: nat -> nat -> nat
          cond_sub_n1_n2_1 :: nat -> nat -> nat
          add              :: nat -> nat -> nat
          eval             :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          sub              :: nat -> nat -> nat
          main             :: expr -> nat
    + Applied Processor:
        Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
    + Details:
        none
* Step 8: Inline WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: main_4(x0) x4 -> x4 x0
        2: main_5(x3) x4 -> x3 x4
        3: main_3(x8) x6 -> x6 x8
        4: eval_simpl_expr(x3) x4 -> x4 x3
        5: eval_expr_4(x1, x7) x8 -> x1 x7 x8
        6: eval_expr_3(x2, x5, x13) x14 -> x2 x14 (eval(x2, x5) x13)
        7: eval_expr_8(x2, x7) x8 -> x2 x7 x8
        8: eval_expr_7(x3, x4, x13) x14 -> x4 x14 (eval(x3, x4) x13)
        9: cond_eval_expr(Nat(x5), x1, x2) -> x5
        10: cond_eval_expr(Add(x23, x25), x2, x9) -> x2 (eval(x2, x9) x23) (eval(x2, x9) x25)
        11: cond_eval_expr(Sub(x23, x25), x5, x4) -> x4 (eval(x5, x4) x23) (eval(x5, x4) x25)
        12: eval_1(x1, x2) x4 -> cond_eval_expr(x4, x1, x2)
        13: eval(x2, x4) x8 -> cond_eval_expr(x8, x2, x4)
        14: eval_simpl(x3, x5) x6 -> eval(x3, x5) x6
        15: main_2(x12, x6) x10 -> eval(x6, x10) x12
        16: cond_sub_n1_n2_1(Zero(), x4) -> Zero()
        17: cond_sub_n1_n2_1(Succ(x5), x4) -> sub() x5 x4
        18: cond_sub_n1_n2(Zero(), x2) -> x2
        19: cond_sub_n1_n2(Succ(x4), x2) -> cond_sub_n1_n2_1(x2, x4)
        20: sub_n1(x2) x3 -> cond_sub_n1_n2(x3, x2)
        21: sub_1() x2 -> sub_n1(x2)
        22: sub() x4 -> sub_n1(x4)
        23: main_1(x12) x6 -> eval(x6, sub()) x12
        24: cond_add_n1_n2(Zero(), x2) -> x2
        25: cond_add_n1_n2(Succ(x3), x2) -> Succ(add() x3 x2)
        26: add_n1(x1) x2 -> cond_add_n1_n2(x1, x2)
        27: add_1() x1 -> add_n1(x1)
        28: add() x2 -> add_n1(x2)
        29: main(x12) -> eval(add(), sub()) x12
        where
          Add              :: expr -> expr -> expr
          Nat              :: nat -> expr
          Sub              :: expr -> expr -> expr
          Succ             :: nat -> nat
          Zero             :: nat
          eval_simpl       :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          eval_simpl_expr  :: expr -> (expr -> nat) -> nat
          add_n1           :: nat -> nat -> nat
          sub_n1           :: nat -> nat -> nat
          add_1            :: nat -> nat -> nat
          eval_1           :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          main_1           :: expr -> (nat -> nat -> nat) -> nat
          sub_1            :: nat -> nat -> nat
          main_2           :: expr -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat
          eval_expr_3      :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat -> nat
          main_3           :: expr -> (expr -> nat) -> nat
          eval_expr_4      :: (nat -> nat -> nat) -> nat -> nat -> nat
          main_4           :: expr -> (expr -> nat) -> nat
          main_5           :: (expr -> nat) -> expr -> nat
          eval_expr_7      :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat -> nat
          eval_expr_8      :: (nat -> nat -> nat) -> nat -> nat -> nat
          cond_eval_expr   :: expr -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat
          cond_add_n1_n2   :: nat -> nat -> nat
          cond_sub_n1_n2   :: nat -> nat -> nat
          cond_sub_n1_n2_1 :: nat -> nat -> nat
          add              :: nat -> nat -> nat
          eval             :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          sub              :: nat -> nat -> nat
          main             :: expr -> nat
    + Applied Processor:
        Inline {inlineType = InlineFull, inlineSelect = <inline case-expression>}
    + Details:
        none
* Step 9: Inline WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: main_4(x0) x4 -> x4 x0
        2: main_5(x3) x4 -> x3 x4
        3: main_3(x8) x6 -> x6 x8
        4: eval_simpl_expr(x3) x4 -> x4 x3
        5: eval_expr_4(x1, x7) x8 -> x1 x7 x8
        6: eval_expr_3(x2, x5, x13) x14 -> x2 x14 (eval(x2, x5) x13)
        7: eval_expr_8(x2, x7) x8 -> x2 x7 x8
        8: eval_expr_7(x3, x4, x13) x14 -> x4 x14 (eval(x3, x4) x13)
        9: cond_eval_expr(Nat(x5), x1, x2) -> x5
        10: cond_eval_expr(Add(x23, x25), x2, x9) -> x2 (eval(x2, x9) x23) (eval(x2, x9) x25)
        11: cond_eval_expr(Sub(x23, x25), x5, x4) -> x4 (eval(x5, x4) x23) (eval(x5, x4) x25)
        12: eval_1(x2, x4) Nat(x10) -> x10
        13: eval_1(x4, x18) Add(x46, x50) -> x4 (eval(x4, x18) x46) (eval(x4, x18) x50)
        14: eval_1(x10, x8) Sub(x46, x50) -> x8 (eval(x10, x8) x46) (eval(x10, x8) x50)
        15: eval(x2, x4) Nat(x10) -> x10
        16: eval(x4, x18) Add(x46, x50) -> x4 (eval(x4, x18) x46) (eval(x4, x18) x50)
        17: eval(x10, x8) Sub(x46, x50) -> x8 (eval(x10, x8) x46) (eval(x10, x8) x50)
        18: eval_simpl(x3, x5) x6 -> eval(x3, x5) x6
        19: main_2(x12, x6) x10 -> eval(x6, x10) x12
        20: cond_sub_n1_n2_1(Zero(), x4) -> Zero()
        21: cond_sub_n1_n2_1(Succ(x5), x4) -> sub() x5 x4
        22: cond_sub_n1_n2(Zero(), x2) -> x2
        23: cond_sub_n1_n2(Succ(x8), Zero()) -> Zero()
        24: cond_sub_n1_n2(Succ(x8), Succ(x10)) -> sub() x10 x8
        25: sub_n1(x4) Zero() -> x4
        26: sub_n1(x4) Succ(x8) -> cond_sub_n1_n2_1(x4, x8)
        27: sub_1() x2 -> sub_n1(x2)
        28: sub() x4 -> sub_n1(x4)
        29: main_1(x12) x6 -> eval(x6, sub()) x12
        30: cond_add_n1_n2(Zero(), x2) -> x2
        31: cond_add_n1_n2(Succ(x3), x2) -> Succ(add() x3 x2)
        32: add_n1(Zero()) x4 -> x4
        33: add_n1(Succ(x6)) x4 -> Succ(add() x6 x4)
        34: add_1() x1 -> add_n1(x1)
        35: add() x2 -> add_n1(x2)
        36: main(x12) -> eval(add(), sub()) x12
        where
          Add              :: expr -> expr -> expr
          Nat              :: nat -> expr
          Sub              :: expr -> expr -> expr
          Succ             :: nat -> nat
          Zero             :: nat
          eval_simpl       :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          eval_simpl_expr  :: expr -> (expr -> nat) -> nat
          add_n1           :: nat -> nat -> nat
          sub_n1           :: nat -> nat -> nat
          add_1            :: nat -> nat -> nat
          eval_1           :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          main_1           :: expr -> (nat -> nat -> nat) -> nat
          sub_1            :: nat -> nat -> nat
          main_2           :: expr -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat
          eval_expr_3      :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat -> nat
          main_3           :: expr -> (expr -> nat) -> nat
          eval_expr_4      :: (nat -> nat -> nat) -> nat -> nat -> nat
          main_4           :: expr -> (expr -> nat) -> nat
          main_5           :: (expr -> nat) -> expr -> nat
          eval_expr_7      :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat -> nat
          eval_expr_8      :: (nat -> nat -> nat) -> nat -> nat -> nat
          cond_eval_expr   :: expr -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat
          cond_add_n1_n2   :: nat -> nat -> nat
          cond_sub_n1_n2   :: nat -> nat -> nat
          cond_sub_n1_n2_1 :: nat -> nat -> nat
          add              :: nat -> nat -> nat
          eval             :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          sub              :: nat -> nat -> nat
          main             :: expr -> nat
    + Applied Processor:
        Inline {inlineType = InlineFull, inlineSelect = <inline case-expression>}
    + Details:
        none
* Step 10: UsableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: main_4(x0) x4 -> x4 x0
        2: main_5(x3) x4 -> x3 x4
        3: main_3(x8) x6 -> x6 x8
        4: eval_simpl_expr(x3) x4 -> x4 x3
        5: eval_expr_4(x1, x7) x8 -> x1 x7 x8
        6: eval_expr_3(x2, x5, x13) x14 -> x2 x14 (eval(x2, x5) x13)
        7: eval_expr_8(x2, x7) x8 -> x2 x7 x8
        8: eval_expr_7(x3, x4, x13) x14 -> x4 x14 (eval(x3, x4) x13)
        9: cond_eval_expr(Nat(x5), x1, x2) -> x5
        10: cond_eval_expr(Add(x23, x25), x2, x9) -> x2 (eval(x2, x9) x23) (eval(x2, x9) x25)
        11: cond_eval_expr(Sub(x23, x25), x5, x4) -> x4 (eval(x5, x4) x23) (eval(x5, x4) x25)
        12: eval_1(x2, x4) Nat(x10) -> x10
        13: eval_1(x4, x18) Add(x46, x50) -> x4 (eval(x4, x18) x46) (eval(x4, x18) x50)
        14: eval_1(x10, x8) Sub(x46, x50) -> x8 (eval(x10, x8) x46) (eval(x10, x8) x50)
        15: eval(x2, x4) Nat(x10) -> x10
        16: eval(x4, x18) Add(x46, x50) -> x4 (eval(x4, x18) x46) (eval(x4, x18) x50)
        17: eval(x10, x8) Sub(x46, x50) -> x8 (eval(x10, x8) x46) (eval(x10, x8) x50)
        18: eval_simpl(x3, x5) x6 -> eval(x3, x5) x6
        19: main_2(x12, x6) x10 -> eval(x6, x10) x12
        20: cond_sub_n1_n2_1(Zero(), x4) -> Zero()
        21: cond_sub_n1_n2_1(Succ(x5), x4) -> sub() x5 x4
        22: cond_sub_n1_n2(Zero(), x2) -> x2
        23: cond_sub_n1_n2(Succ(x8), Zero()) -> Zero()
        24: cond_sub_n1_n2(Succ(x8), Succ(x10)) -> sub() x10 x8
        25: sub_n1(x4) Zero() -> x4
        26: sub_n1(Zero()) Succ(x8) -> Zero()
        27: sub_n1(Succ(x10)) Succ(x8) -> sub() x10 x8
        28: sub_1() x2 -> sub_n1(x2)
        29: sub() x4 -> sub_n1(x4)
        30: main_1(x12) x6 -> eval(x6, sub()) x12
        31: cond_add_n1_n2(Zero(), x2) -> x2
        32: cond_add_n1_n2(Succ(x3), x2) -> Succ(add() x3 x2)
        33: add_n1(Zero()) x4 -> x4
        34: add_n1(Succ(x6)) x4 -> Succ(add() x6 x4)
        35: add_1() x1 -> add_n1(x1)
        36: add() x2 -> add_n1(x2)
        37: main(x12) -> eval(add(), sub()) x12
        where
          Add              :: expr -> expr -> expr
          Nat              :: nat -> expr
          Sub              :: expr -> expr -> expr
          Succ             :: nat -> nat
          Zero             :: nat
          eval_simpl       :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          eval_simpl_expr  :: expr -> (expr -> nat) -> nat
          add_n1           :: nat -> nat -> nat
          sub_n1           :: nat -> nat -> nat
          add_1            :: nat -> nat -> nat
          eval_1           :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          main_1           :: expr -> (nat -> nat -> nat) -> nat
          sub_1            :: nat -> nat -> nat
          main_2           :: expr -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat
          eval_expr_3      :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat -> nat
          main_3           :: expr -> (expr -> nat) -> nat
          eval_expr_4      :: (nat -> nat -> nat) -> nat -> nat -> nat
          main_4           :: expr -> (expr -> nat) -> nat
          main_5           :: (expr -> nat) -> expr -> nat
          eval_expr_7      :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat -> nat
          eval_expr_8      :: (nat -> nat -> nat) -> nat -> nat -> nat
          cond_eval_expr   :: expr -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat
          cond_add_n1_n2   :: nat -> nat -> nat
          cond_sub_n1_n2   :: nat -> nat -> nat
          cond_sub_n1_n2_1 :: nat -> nat -> nat
          add              :: nat -> nat -> nat
          eval             :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          sub              :: nat -> nat -> nat
          main             :: expr -> nat
    + Applied Processor:
        UsableRules {urType = Syntactic}
    + Details:
        none
* Step 11: NeededRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: main_4(x0) x4 -> x4 x0
        2: main_5(x3) x4 -> x3 x4
        3: main_3(x8) x6 -> x6 x8
        4: eval_simpl_expr(x3) x4 -> x4 x3
        5: eval_expr_4(x1, x7) x8 -> x1 x7 x8
        6: eval_expr_3(x2, x5, x13) x14 -> x2 x14 (eval(x2, x5) x13)
        7: eval_expr_8(x2, x7) x8 -> x2 x7 x8
        8: eval_expr_7(x3, x4, x13) x14 -> x4 x14 (eval(x3, x4) x13)
        12: eval_1(x2, x4) Nat(x10) -> x10
        13: eval_1(x4, x18) Add(x46, x50) -> x4 (eval(x4, x18) x46) (eval(x4, x18) x50)
        14: eval_1(x10, x8) Sub(x46, x50) -> x8 (eval(x10, x8) x46) (eval(x10, x8) x50)
        15: eval(x2, x4) Nat(x10) -> x10
        16: eval(x4, x18) Add(x46, x50) -> x4 (eval(x4, x18) x46) (eval(x4, x18) x50)
        17: eval(x10, x8) Sub(x46, x50) -> x8 (eval(x10, x8) x46) (eval(x10, x8) x50)
        18: eval_simpl(x3, x5) x6 -> eval(x3, x5) x6
        19: main_2(x12, x6) x10 -> eval(x6, x10) x12
        25: sub_n1(x4) Zero() -> x4
        26: sub_n1(Zero()) Succ(x8) -> Zero()
        27: sub_n1(Succ(x10)) Succ(x8) -> sub() x10 x8
        28: sub_1() x2 -> sub_n1(x2)
        29: sub() x4 -> sub_n1(x4)
        30: main_1(x12) x6 -> eval(x6, sub()) x12
        33: add_n1(Zero()) x4 -> x4
        34: add_n1(Succ(x6)) x4 -> Succ(add() x6 x4)
        35: add_1() x1 -> add_n1(x1)
        36: add() x2 -> add_n1(x2)
        37: main(x12) -> eval(add(), sub()) x12
        where
          Add             :: expr -> expr -> expr
          Nat             :: nat -> expr
          Sub             :: expr -> expr -> expr
          Succ            :: nat -> nat
          Zero            :: nat
          eval_simpl      :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          eval_simpl_expr :: expr -> (expr -> nat) -> nat
          add_n1          :: nat -> nat -> nat
          sub_n1          :: nat -> nat -> nat
          add_1           :: nat -> nat -> nat
          eval_1          :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          main_1          :: expr -> (nat -> nat -> nat) -> nat
          sub_1           :: nat -> nat -> nat
          main_2          :: expr -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat
          eval_expr_3     :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat -> nat
          main_3          :: expr -> (expr -> nat) -> nat
          eval_expr_4     :: (nat -> nat -> nat) -> nat -> nat -> nat
          main_4          :: expr -> (expr -> nat) -> nat
          main_5          :: (expr -> nat) -> expr -> nat
          eval_expr_7     :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat -> nat
          eval_expr_8     :: (nat -> nat -> nat) -> nat -> nat -> nat
          add             :: nat -> nat -> nat
          eval            :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          sub             :: nat -> nat -> nat
          main            :: expr -> nat
    + Applied Processor:
        NeededRules
    + Details:
        none
* Step 12: CFA WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: main_4(x0) x4 -> x4 x0
        2: main_5(x3) x4 -> x3 x4
        3: main_3(x8) x6 -> x6 x8
        4: eval_simpl_expr(x3) x4 -> x4 x3
        5: eval_expr_4(x1, x7) x8 -> x1 x7 x8
        6: eval_expr_3(x2, x5, x13) x14 -> x2 x14 (eval(x2, x5) x13)
        7: eval_expr_8(x2, x7) x8 -> x2 x7 x8
        8: eval_expr_7(x3, x4, x13) x14 -> x4 x14 (eval(x3, x4) x13)
        9: eval_1(x2, x4) Nat(x10) -> x10
        10: eval_1(x4, x18) Add(x46, x50) -> x4 (eval(x4, x18) x46) (eval(x4, x18) x50)
        11: eval_1(x10, x8) Sub(x46, x50) -> x8 (eval(x10, x8) x46) (eval(x10, x8) x50)
        12: eval(x2, x4) Nat(x10) -> x10
        13: eval(x4, x18) Add(x46, x50) -> x4 (eval(x4, x18) x46) (eval(x4, x18) x50)
        14: eval(x10, x8) Sub(x46, x50) -> x8 (eval(x10, x8) x46) (eval(x10, x8) x50)
        15: eval_simpl(x3, x5) x6 -> eval(x3, x5) x6
        16: main_2(x12, x6) x10 -> eval(x6, x10) x12
        17: sub_n1(x4) Zero() -> x4
        18: sub_n1(Zero()) Succ(x8) -> Zero()
        19: sub_n1(Succ(x10)) Succ(x8) -> sub() x10 x8
        20: sub_1() x2 -> sub_n1(x2)
        21: sub() x4 -> sub_n1(x4)
        22: main_1(x12) x6 -> eval(x6, sub()) x12
        23: add_n1(Zero()) x4 -> x4
        24: add_n1(Succ(x6)) x4 -> Succ(add() x6 x4)
        25: add_1() x1 -> add_n1(x1)
        26: add() x2 -> add_n1(x2)
        27: main(x12) -> eval(add(), sub()) x12
        where
          Add             :: expr -> expr -> expr
          Nat             :: nat -> expr
          Sub             :: expr -> expr -> expr
          Succ            :: nat -> nat
          Zero            :: nat
          eval_simpl      :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          eval_simpl_expr :: expr -> (expr -> nat) -> nat
          add_n1          :: nat -> nat -> nat
          sub_n1          :: nat -> nat -> nat
          add_1           :: nat -> nat -> nat
          eval_1          :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          main_1          :: expr -> (nat -> nat -> nat) -> nat
          sub_1           :: nat -> nat -> nat
          main_2          :: expr -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> nat
          eval_expr_3     :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat -> nat
          main_3          :: expr -> (expr -> nat) -> nat
          eval_expr_4     :: (nat -> nat -> nat) -> nat -> nat -> nat
          main_4          :: expr -> (expr -> nat) -> nat
          main_5          :: (expr -> nat) -> expr -> nat
          eval_expr_7     :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat -> nat
          eval_expr_8     :: (nat -> nat -> nat) -> nat -> nat -> nat
          add             :: nat -> nat -> nat
          eval            :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          sub             :: nat -> nat -> nat
          main            :: expr -> nat
    + Applied Processor:
        CFA {cfaRefinement = <control flow analysis>}
    + Details:
        {X{*} -> Succ(X{*})
              |  Succ(X{*})
              |  Zero()
              |  Succ(X{*})
              |  Succ(X{*})
              |  Zero()
              |  Succ(X{*})
              |  Zero()
              |  Zero()
              |  Sub(X{*},X{*})
              |  Add(X{*},X{*})
              |  Nat(X{*})
              |  Sub(X{*},X{*})
              |  Add(X{*},X{*})
              |  Nat(X{*})
        ,V{x2_12} -> V{x10_14}
                  |  V{x4_13}
                  |  add()
        ,V{x2_26} -> V{x6_24}
                  |  R{13}
                  |  R{14}
                  |  R{12}
        ,V{x4_12} -> V{x8_14}
                  |  V{x18_13}
                  |  sub()
        ,V{x4_13} -> V{x10_14}
                  |  V{x4_13}
                  |  add()
        ,V{x4_17} -> V{x4_21}
        ,V{x4_21} -> V{x10_19}
                  |  R{13}
                  |  R{14}
                  |  R{12}
        ,V{x4_23} -> V{x4_24}
                  |  R{12}
                  |  R{13}
                  |  R{14}
        ,V{x4_24} -> V{x4_24}
                  |  R{12}
                  |  R{13}
                  |  R{14}
        ,V{x6_24} -> R{24}
                  |  R{23}
                  |  @(R{26},V{x4_24})
                  |  @(@(add(),V{x6_24}),V{x4_24})
                  |  X{*}
        ,V{x8_14} -> V{x8_14}
                  |  V{x18_13}
                  |  sub()
        ,V{x8_18} -> R{24}
                  |  R{23}
                  |  @(R{26},V{x4_24})
                  |  X{*}
                  |  @(@(add(),V{x6_24}),V{x4_24})
        ,V{x8_19} -> R{24}
                  |  R{23}
                  |  @(R{26},V{x4_24})
                  |  X{*}
                  |  @(@(add(),V{x6_24}),V{x4_24})
        ,V{x10_12} -> X{*}
        ,V{x10_14} -> V{x10_14}
                   |  V{x4_13}
                   |  add()
        ,V{x10_19} -> R{24}
                   |  R{23}
                   |  @(R{26},V{x4_24})
                   |  @(@(add(),V{x6_24}),V{x4_24})
                   |  X{*}
        ,V{x12_27} -> X{*}
        ,V{x18_13} -> V{x8_14}
                   |  V{x18_13}
                   |  sub()
        ,V{x46_13} -> X{*}
        ,V{x46_14} -> X{*}
        ,V{x50_13} -> X{*}
        ,V{x50_14} -> X{*}
        ,R{0} -> R{27}
              |  main(X{*})
        ,R{12} -> V{x10_12}
        ,R{13} -> R{24}
               |  R{23}
               |  @(R{26},R{14})
               |  @(R{26},R{13})
               |  @(R{26},R{12})
               |  @(R{26},@(eval(V{x4_13},V{x18_13}),V{x50_13}))
               |  @(@(V{x4_13},R{14}),R{12})
               |  @(@(V{x4_13},R{13}),R{12})
               |  @(@(V{x4_13},R{12}),R{12})
               |  @(@(V{x4_13},R{14}),R{13})
               |  @(@(V{x4_13},R{13}),R{13})
               |  @(@(V{x4_13},R{12}),R{13})
               |  @(@(V{x4_13},R{14}),R{14})
               |  @(@(V{x4_13},R{13}),R{14})
               |  @(@(V{x4_13},R{12}),R{14})
               |  @(@(V{x4_13},@(eval(V{x4_13},V{x18_13}),V{x46_13})),R{14})
               |  @(@(V{x4_13},@(eval(V{x4_13},V{x18_13}),V{x46_13})),R{13})
               |  @(@(V{x4_13},@(eval(V{x4_13},V{x18_13}),V{x46_13})),R{12})
               |  @(@(V{x4_13},R{14}),@(eval(V{x4_13},V{x18_13}),V{x50_13}))
               |  @(@(V{x4_13},R{13}),@(eval(V{x4_13},V{x18_13}),V{x50_13}))
               |  @(@(V{x4_13},R{12}),@(eval(V{x4_13},V{x18_13}),V{x50_13}))
               |  @(@(V{x4_13},@(eval(V{x4_13},V{x18_13}),V{x46_13})),@(eval(V{x4_13},V{x18_13}),V{x50_13}))
        ,R{14} -> R{19}
               |  R{18}
               |  R{17}
               |  @(R{21},R{14})
               |  @(R{21},R{13})
               |  @(R{21},R{12})
               |  @(R{21},@(eval(V{x10_14},V{x8_14}),V{x50_14}))
               |  @(@(V{x8_14},R{14}),R{12})
               |  @(@(V{x8_14},R{13}),R{12})
               |  @(@(V{x8_14},R{12}),R{12})
               |  @(@(V{x8_14},R{14}),R{13})
               |  @(@(V{x8_14},R{13}),R{13})
               |  @(@(V{x8_14},R{12}),R{13})
               |  @(@(V{x8_14},R{14}),R{14})
               |  @(@(V{x8_14},R{13}),R{14})
               |  @(@(V{x8_14},R{12}),R{14})
               |  @(@(V{x8_14},@(eval(V{x10_14},V{x8_14}),V{x46_14})),R{14})
               |  @(@(V{x8_14},@(eval(V{x10_14},V{x8_14}),V{x46_14})),R{13})
               |  @(@(V{x8_14},@(eval(V{x10_14},V{x8_14}),V{x46_14})),R{12})
               |  @(@(V{x8_14},R{14}),@(eval(V{x10_14},V{x8_14}),V{x50_14}))
               |  @(@(V{x8_14},R{13}),@(eval(V{x10_14},V{x8_14}),V{x50_14}))
               |  @(@(V{x8_14},R{12}),@(eval(V{x10_14},V{x8_14}),V{x50_14}))
               |  @(@(V{x8_14},@(eval(V{x10_14},V{x8_14}),V{x46_14})),@(eval(V{x10_14},V{x8_14}),V{x50_14}))
        ,R{17} -> V{x4_17}
        ,R{18} -> Zero()
        ,R{19} -> R{19}
               |  R{18}
               |  R{17}
               |  @(R{21},V{x8_19})
               |  @(@(sub(),V{x10_19}),V{x8_19})
        ,R{21} -> sub_n1(V{x4_21})
        ,R{23} -> V{x4_23}
        ,R{24} -> Succ(R{24})
               |  Succ(R{23})
               |  Succ(@(R{26},V{x4_24}))
               |  Succ(@(@(add(),V{x6_24}),V{x4_24}))
        ,R{26} -> add_n1(V{x2_26})
        ,R{27} -> R{14}
               |  R{13}
               |  R{12}
               |  @(eval(add(),sub()),V{x12_27})}
* Step 13: UncurryATRS WORST_CASE(?,O(n^2))
    + Considered Problem:
        12: eval(add(), sub()) Nat(x1) -> x1
        13: eval(add(), sub()) Add(x2, x1) -> add() (eval(add(), sub()) x2) (eval(add(), sub()) x1)
        14: eval(add(), sub()) Sub(x2, x1) -> sub() (eval(add(), sub()) x2) (eval(add(), sub()) x1)
        17: sub_n1(x4) Zero() -> x4
        18: sub_n1(Zero()) Succ(x8) -> Zero()
        19: sub_n1(Succ(x2)) Succ(x1) -> sub() x2 x1
        21: sub() x4 -> sub_n1(x4)
        23: add_n1(Zero()) x4 -> x4
        24: add_n1(Succ(x2)) x1 -> Succ(add() x2 x1)
        26: add() x2 -> add_n1(x2)
        27: main(x12) -> eval(add(), sub()) x12
        where
          Add    :: expr -> expr -> expr
          Nat    :: nat -> expr
          Sub    :: expr -> expr -> expr
          Succ   :: nat -> nat
          Zero   :: nat
          add_n1 :: nat -> nat -> nat
          sub_n1 :: nat -> nat -> nat
          add    :: nat -> nat -> nat
          eval   :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          sub    :: nat -> nat -> nat
          main   :: expr -> nat
    + Applied Processor:
        UncurryATRS
    + Details:
        none
* Step 14: UsableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: eval#1(add(), sub(), Nat(x1)) -> x1
        2: eval#1(add(), sub(), Add(x2, x1)) -> add#2(eval#1(add(), sub(), x2), eval#1(add(), sub(), x1))
        3: eval#1(add(), sub(), Sub(x2, x1)) -> sub#2(eval#1(add(), sub(), x2), eval#1(add(), sub(), x1))
        4: sub_n1#1(x4, Zero()) -> x4
        5: sub_n1#1(Zero(), Succ(x8)) -> Zero()
        6: sub_n1#1(Succ(x2), Succ(x1)) -> sub#2(x2, x1)
        7: sub#1(x4) -> sub_n1(x4)
        8: sub#2(x4, x5) -> sub_n1#1(x4, x5)
        9: add_n1#1(Zero(), x4) -> x4
        10: add_n1#1(Succ(x2), x1) -> Succ(add#2(x2, x1))
        11: add#1(x2) -> add_n1(x2)
        12: add#2(x2, x3) -> add_n1#1(x2, x3)
        13: main(x12) -> eval#1(add(), sub(), x12)
        where
          Add      :: expr -> expr -> expr
          Nat      :: nat -> expr
          Sub      :: expr -> expr -> expr
          Succ     :: nat -> nat
          Zero     :: nat
          add      :: nat -> nat -> nat
          add#1    :: nat -> nat -> nat
          add#2    :: nat -> nat -> nat
          add_n1   :: nat -> nat -> nat
          add_n1#1 :: nat -> nat -> nat
          eval#1   :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          main     :: expr -> nat
          sub      :: nat -> nat -> nat
          sub#1    :: nat -> nat -> nat
          sub#2    :: nat -> nat -> nat
          sub_n1   :: nat -> nat -> nat
          sub_n1#1 :: nat -> nat -> nat
    + Applied Processor:
        UsableRules {urType = DFA}
    + Details:
        none
* Step 15: Inline WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: eval#1(add(), sub(), Nat(x1)) -> x1
        2: eval#1(add(), sub(), Add(x2, x1)) -> add#2(eval#1(add(), sub(), x2), eval#1(add(), sub(), x1))
        3: eval#1(add(), sub(), Sub(x2, x1)) -> sub#2(eval#1(add(), sub(), x2), eval#1(add(), sub(), x1))
        4: sub_n1#1(x4, Zero()) -> x4
        5: sub_n1#1(Zero(), Succ(x8)) -> Zero()
        6: sub_n1#1(Succ(x2), Succ(x1)) -> sub#2(x2, x1)
        8: sub#2(x4, x5) -> sub_n1#1(x4, x5)
        9: add_n1#1(Zero(), x4) -> x4
        10: add_n1#1(Succ(x2), x1) -> Succ(add#2(x2, x1))
        12: add#2(x2, x3) -> add_n1#1(x2, x3)
        13: main(x12) -> eval#1(add(), sub(), x12)
        where
          Add      :: expr -> expr -> expr
          Nat      :: nat -> expr
          Sub      :: expr -> expr -> expr
          Succ     :: nat -> nat
          Zero     :: nat
          add      :: nat -> nat -> nat
          add#2    :: nat -> nat -> nat
          add_n1#1 :: nat -> nat -> nat
          eval#1   :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          main     :: expr -> nat
          sub      :: nat -> nat -> nat
          sub#2    :: nat -> nat -> nat
          sub_n1#1 :: nat -> nat -> nat
    + Applied Processor:
        Inline {inlineType = InlineFull, inlineSelect = <inline decreasing>}
    + Details:
        none
* Step 16: UsableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: eval#1(add(), sub(), Nat(x1)) -> x1
        2: eval#1(add(), sub(), Add(x2, x1)) -> add#2(eval#1(add(), sub(), x2), eval#1(add(), sub(), x1))
        3: eval#1(add(), sub(), Sub(x2, x1)) -> sub#2(eval#1(add(), sub(), x2), eval#1(add(), sub(), x1))
        4: sub_n1#1(x4, Zero()) -> x4
        5: sub_n1#1(Zero(), Succ(x8)) -> Zero()
        6: sub_n1#1(Succ(x2), Succ(x1)) -> sub#2(x2, x1)
        7: sub#2(x8, Zero()) -> x8
        8: sub#2(Zero(), Succ(x16)) -> Zero()
        9: sub#2(Succ(x4), Succ(x2)) -> sub#2(x4, x2)
        10: add_n1#1(Zero(), x4) -> x4
        11: add_n1#1(Succ(x2), x1) -> Succ(add#2(x2, x1))
        12: add#2(Zero(), x8) -> x8
        13: add#2(Succ(x4), x2) -> Succ(add#2(x4, x2))
        14: main(x12) -> eval#1(add(), sub(), x12)
        where
          Add      :: expr -> expr -> expr
          Nat      :: nat -> expr
          Sub      :: expr -> expr -> expr
          Succ     :: nat -> nat
          Zero     :: nat
          add      :: nat -> nat -> nat
          add#2    :: nat -> nat -> nat
          add_n1#1 :: nat -> nat -> nat
          eval#1   :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          main     :: expr -> nat
          sub      :: nat -> nat -> nat
          sub#2    :: nat -> nat -> nat
          sub_n1#1 :: nat -> nat -> nat
    + Applied Processor:
        UsableRules {urType = Syntactic}
    + Details:
        none
* Step 17: Compression WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: eval#1(add(), sub(), Nat(x1)) -> x1
        2: eval#1(add(), sub(), Add(x2, x1)) -> add#2(eval#1(add(), sub(), x2), eval#1(add(), sub(), x1))
        3: eval#1(add(), sub(), Sub(x2, x1)) -> sub#2(eval#1(add(), sub(), x2), eval#1(add(), sub(), x1))
        7: sub#2(x8, Zero()) -> x8
        8: sub#2(Zero(), Succ(x16)) -> Zero()
        9: sub#2(Succ(x4), Succ(x2)) -> sub#2(x4, x2)
        12: add#2(Zero(), x8) -> x8
        13: add#2(Succ(x4), x2) -> Succ(add#2(x4, x2))
        14: main(x12) -> eval#1(add(), sub(), x12)
        where
          Add    :: expr -> expr -> expr
          Nat    :: nat -> expr
          Sub    :: expr -> expr -> expr
          Succ   :: nat -> nat
          Zero   :: nat
          add    :: nat -> nat -> nat
          add#2  :: nat -> nat -> nat
          eval#1 :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> expr -> nat
          main   :: expr -> nat
          sub    :: nat -> nat -> nat
          sub#2  :: nat -> nat -> nat
    + Applied Processor:
        Compression
    + Details:
        none
* Step 18: ToTctProblem WORST_CASE(?,O(n^2))
    + Considered Problem:
        1: eval#1(Nat(x1)) -> x1
        2: eval#1(Add(x2, x1)) -> add#2(eval#1(x2), eval#1(x1))
        3: eval#1(Sub(x2, x1)) -> sub#2(eval#1(x2), eval#1(x1))
        4: sub#2(x8, Zero()) -> x8
        5: sub#2(Zero(), Succ(x16)) -> Zero()
        6: sub#2(Succ(x4), Succ(x2)) -> sub#2(x4, x2)
        7: add#2(Zero(), x8) -> x8
        8: add#2(Succ(x4), x2) -> Succ(add#2(x4, x2))
        9: main(x12) -> eval#1(x12)
        where
          Add    :: expr -> expr -> expr
          Nat    :: nat -> expr
          Sub    :: expr -> expr -> expr
          Succ   :: nat -> nat
          Zero   :: nat
          add#2  :: nat -> nat -> nat
          eval#1 :: expr -> nat
          main   :: expr -> nat
          sub#2  :: nat -> nat -> nat
    + Applied Processor:
        ToTctProblem
    + Details:
        none
* Step 19: DependencyPairs WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
            add#2(Zero(),x8) -> x8
            eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
            eval#1(Nat(x1)) -> x1
            eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
            main(x12) -> eval#1(x12)
            sub#2(x8,Zero()) -> x8
            sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
            sub#2(Zero(),Succ(x16)) -> Zero()
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main} and constructors {Add,Nat,Sub,Succ,Zero}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
          add#2#(Zero(),x8) -> c_2()
          eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
          eval#1#(Nat(x1)) -> c_4()
          eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
          main#(x12) -> c_6(eval#1#(x12))
          sub#2#(x8,Zero()) -> c_7()
          sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
          sub#2#(Zero(),Succ(x16)) -> c_9()
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 20: PredecessorEstimation WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
            add#2#(Zero(),x8) -> c_2()
            eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
            eval#1#(Nat(x1)) -> c_4()
            eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
            main#(x12) -> c_6(eval#1#(x12))
            sub#2#(x8,Zero()) -> c_7()
            sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
            sub#2#(Zero(),Succ(x16)) -> c_9()
        - Weak TRS:
            add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
            add#2(Zero(),x8) -> x8
            eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
            eval#1(Nat(x1)) -> x1
            eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
            main(x12) -> eval#1(x12)
            sub#2(x8,Zero()) -> x8
            sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
            sub#2(Zero(),Succ(x16)) -> Zero()
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {2,4,7,9}
        by application of
          Pre({2,4,7,9}) = {1,3,5,6,8}.
        Here rules are labelled as follows:
          1: add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
          2: add#2#(Zero(),x8) -> c_2()
          3: eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
          4: eval#1#(Nat(x1)) -> c_4()
          5: eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
          6: main#(x12) -> c_6(eval#1#(x12))
          7: sub#2#(x8,Zero()) -> c_7()
          8: sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
          9: sub#2#(Zero(),Succ(x16)) -> c_9()
* Step 21: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
            eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
            eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
            main#(x12) -> c_6(eval#1#(x12))
            sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
        - Weak DPs:
            add#2#(Zero(),x8) -> c_2()
            eval#1#(Nat(x1)) -> c_4()
            sub#2#(x8,Zero()) -> c_7()
            sub#2#(Zero(),Succ(x16)) -> c_9()
        - Weak TRS:
            add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
            add#2(Zero(),x8) -> x8
            eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
            eval#1(Nat(x1)) -> x1
            eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
            main(x12) -> eval#1(x12)
            sub#2(x8,Zero()) -> x8
            sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
            sub#2(Zero(),Succ(x16)) -> Zero()
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
             -->_1 add#2#(Zero(),x8) -> c_2():6
             -->_1 add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2)):1
          
          2:S:eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
             -->_3 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
             -->_2 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
             -->_3 eval#1#(Nat(x1)) -> c_4():7
             -->_2 eval#1#(Nat(x1)) -> c_4():7
             -->_1 add#2#(Zero(),x8) -> c_2():6
             -->_3 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
             -->_2 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
             -->_1 add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2)):1
          
          3:S:eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
             -->_1 sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2)):5
             -->_1 sub#2#(Zero(),Succ(x16)) -> c_9():9
             -->_1 sub#2#(x8,Zero()) -> c_7():8
             -->_3 eval#1#(Nat(x1)) -> c_4():7
             -->_2 eval#1#(Nat(x1)) -> c_4():7
             -->_3 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
             -->_2 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
             -->_3 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
             -->_2 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
          
          4:S:main#(x12) -> c_6(eval#1#(x12))
             -->_1 eval#1#(Nat(x1)) -> c_4():7
             -->_1 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):3
             -->_1 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
          
          5:S:sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
             -->_1 sub#2#(Zero(),Succ(x16)) -> c_9():9
             -->_1 sub#2#(x8,Zero()) -> c_7():8
             -->_1 sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2)):5
          
          6:W:add#2#(Zero(),x8) -> c_2()
             
          
          7:W:eval#1#(Nat(x1)) -> c_4()
             
          
          8:W:sub#2#(x8,Zero()) -> c_7()
             
          
          9:W:sub#2#(Zero(),Succ(x16)) -> c_9()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          7: eval#1#(Nat(x1)) -> c_4()
          8: sub#2#(x8,Zero()) -> c_7()
          9: sub#2#(Zero(),Succ(x16)) -> c_9()
          6: add#2#(Zero(),x8) -> c_2()
* Step 22: UsableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
            eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
            eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
            main#(x12) -> c_6(eval#1#(x12))
            sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
        - Weak TRS:
            add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
            add#2(Zero(),x8) -> x8
            eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
            eval#1(Nat(x1)) -> x1
            eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
            main(x12) -> eval#1(x12)
            sub#2(x8,Zero()) -> x8
            sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
            sub#2(Zero(),Succ(x16)) -> Zero()
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
          add#2(Zero(),x8) -> x8
          eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
          eval#1(Nat(x1)) -> x1
          eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
          sub#2(x8,Zero()) -> x8
          sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
          sub#2(Zero(),Succ(x16)) -> Zero()
          add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
          eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
          eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
          main#(x12) -> c_6(eval#1#(x12))
          sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
* Step 23: DecomposeDG WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
            eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
            eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
            main#(x12) -> c_6(eval#1#(x12))
            sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
        - Weak TRS:
            add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
            add#2(Zero(),x8) -> x8
            eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
            eval#1(Nat(x1)) -> x1
            eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
            sub#2(x8,Zero()) -> x8
            sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
            sub#2(Zero(),Succ(x16)) -> Zero()
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero}
    + 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
          eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
          eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
          main#(x12) -> c_6(eval#1#(x12))
        and a lower component
          add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
          sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
        Further, following extension rules are added to the lower component.
          eval#1#(Add(x2,x1)) -> add#2#(eval#1(x2),eval#1(x1))
          eval#1#(Add(x2,x1)) -> eval#1#(x1)
          eval#1#(Add(x2,x1)) -> eval#1#(x2)
          eval#1#(Sub(x2,x1)) -> eval#1#(x1)
          eval#1#(Sub(x2,x1)) -> eval#1#(x2)
          eval#1#(Sub(x2,x1)) -> sub#2#(eval#1(x2),eval#1(x1))
          main#(x12) -> eval#1#(x12)
** Step 23.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
            eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
            main#(x12) -> c_6(eval#1#(x12))
        - Weak TRS:
            add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
            add#2(Zero(),x8) -> x8
            eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
            eval#1(Nat(x1)) -> x1
            eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
            sub#2(x8,Zero()) -> x8
            sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
            sub#2(Zero(),Succ(x16)) -> Zero()
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
             -->_3 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
             -->_2 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
             -->_3 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):1
             -->_2 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):1
          
          2:S:eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1))
             -->_3 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
             -->_2 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
             -->_3 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):1
             -->_2 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):1
          
          3:S:main#(x12) -> c_6(eval#1#(x12))
             -->_1 eval#1#(Sub(x2,x1)) -> c_5(sub#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):2
             -->_1 eval#1#(Add(x2,x1)) -> c_3(add#2#(eval#1(x2),eval#1(x1)),eval#1#(x2),eval#1#(x1)):1
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          eval#1#(Add(x2,x1)) -> c_3(eval#1#(x2),eval#1#(x1))
          eval#1#(Sub(x2,x1)) -> c_5(eval#1#(x2),eval#1#(x1))
** Step 23.a:2: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            eval#1#(Add(x2,x1)) -> c_3(eval#1#(x2),eval#1#(x1))
            eval#1#(Sub(x2,x1)) -> c_5(eval#1#(x2),eval#1#(x1))
            main#(x12) -> c_6(eval#1#(x12))
        - Weak TRS:
            add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
            add#2(Zero(),x8) -> x8
            eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
            eval#1(Nat(x1)) -> x1
            eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
            sub#2(x8,Zero()) -> x8
            sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
            sub#2(Zero(),Succ(x16)) -> Zero()
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/2,c_4/0,c_5/2,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          eval#1#(Add(x2,x1)) -> c_3(eval#1#(x2),eval#1#(x1))
          eval#1#(Sub(x2,x1)) -> c_5(eval#1#(x2),eval#1#(x1))
          main#(x12) -> c_6(eval#1#(x12))
** Step 23.a:3: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            eval#1#(Add(x2,x1)) -> c_3(eval#1#(x2),eval#1#(x1))
            eval#1#(Sub(x2,x1)) -> c_5(eval#1#(x2),eval#1#(x1))
            main#(x12) -> c_6(eval#1#(x12))
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/2,c_4/0,c_5/2,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero}
    + 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_3) = {1,2},
          uargs(c_5) = {1,2},
          uargs(c_6) = {1}
        
        Following symbols are considered usable:
          {eval#1#,main#}
        TcT has computed the following interpretation:
              p(Add) = [1] x2 + [0]         
              p(Nat) = [1] x1 + [0]         
              p(Sub) = [1] x1 + [0]         
             p(Succ) = [1] x1 + [1]         
             p(Zero) = [1]                  
            p(add#2) = [8] x2 + [0]         
           p(eval#1) = [1] x1 + [1]         
             p(main) = [1] x1 + [1]         
            p(sub#2) = [1]                  
           p(add#2#) = [1] x1 + [1] x2 + [1]
          p(eval#1#) = [0]                  
            p(main#) = [4] x1 + [5]         
           p(sub#2#) = [2] x1 + [1] x2 + [1]
              p(c_1) = [1] x1 + [8]         
              p(c_2) = [1]                  
              p(c_3) = [2] x1 + [4] x2 + [0]
              p(c_4) = [1]                  
              p(c_5) = [1] x1 + [4] x2 + [0]
              p(c_6) = [2] x1 + [4]         
              p(c_7) = [2]                  
              p(c_8) = [0]                  
              p(c_9) = [0]                  
        
        Following rules are strictly oriented:
        main#(x12) = [4] x12 + [5]    
                   > [4]              
                   = c_6(eval#1#(x12))
        
        
        Following rules are (at-least) weakly oriented:
        eval#1#(Add(x2,x1)) =  [0]                         
                            >= [0]                         
                            =  c_3(eval#1#(x2),eval#1#(x1))
        
        eval#1#(Sub(x2,x1)) =  [0]                         
                            >= [0]                         
                            =  c_5(eval#1#(x2),eval#1#(x1))
        
** Step 23.a:4: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            eval#1#(Add(x2,x1)) -> c_3(eval#1#(x2),eval#1#(x1))
            eval#1#(Sub(x2,x1)) -> c_5(eval#1#(x2),eval#1#(x1))
        - Weak DPs:
            main#(x12) -> c_6(eval#1#(x12))
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/2,c_4/0,c_5/2,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero}
    + 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_3) = {1,2},
          uargs(c_5) = {1,2},
          uargs(c_6) = {1}
        
        Following symbols are considered usable:
          {eval#1#,main#}
        TcT has computed the following interpretation:
              p(Add) = [1] x1 + [1] x2 + [0]
              p(Nat) = [1] x1 + [0]         
              p(Sub) = [1] x1 + [1] x2 + [2]
             p(Succ) = [1] x1 + [2]         
             p(Zero) = [1]                  
            p(add#2) = [1] x2 + [1]         
           p(eval#1) = [0]                  
             p(main) = [2]                  
            p(sub#2) = [1] x1 + [1]         
           p(add#2#) = [1] x1 + [1]         
          p(eval#1#) = [4] x1 + [0]         
            p(main#) = [9] x1 + [8]         
           p(sub#2#) = [1] x2 + [0]         
              p(c_1) = [1]                  
              p(c_2) = [0]                  
              p(c_3) = [1] x1 + [1] x2 + [0]
              p(c_4) = [1]                  
              p(c_5) = [1] x1 + [1] x2 + [7]
              p(c_6) = [2] x1 + [5]         
              p(c_7) = [0]                  
              p(c_8) = [1]                  
              p(c_9) = [2]                  
        
        Following rules are strictly oriented:
        eval#1#(Sub(x2,x1)) = [4] x1 + [4] x2 + [8]       
                            > [4] x1 + [4] x2 + [7]       
                            = c_5(eval#1#(x2),eval#1#(x1))
        
        
        Following rules are (at-least) weakly oriented:
        eval#1#(Add(x2,x1)) =  [4] x1 + [4] x2 + [0]       
                            >= [4] x1 + [4] x2 + [0]       
                            =  c_3(eval#1#(x2),eval#1#(x1))
        
                 main#(x12) =  [9] x12 + [8]               
                            >= [8] x12 + [5]               
                            =  c_6(eval#1#(x12))           
        
** Step 23.a:5: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            eval#1#(Add(x2,x1)) -> c_3(eval#1#(x2),eval#1#(x1))
        - Weak DPs:
            eval#1#(Sub(x2,x1)) -> c_5(eval#1#(x2),eval#1#(x1))
            main#(x12) -> c_6(eval#1#(x12))
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/2,c_4/0,c_5/2,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero}
    + 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_3) = {1,2},
          uargs(c_5) = {1,2},
          uargs(c_6) = {1}
        
        Following symbols are considered usable:
          {eval#1#,main#}
        TcT has computed the following interpretation:
              p(Add) = [1] x1 + [1] x2 + [8] 
              p(Nat) = [0]                   
              p(Sub) = [1] x1 + [1] x2 + [1] 
             p(Succ) = [1]                   
             p(Zero) = [2]                   
            p(add#2) = [2] x1 + [2] x2 + [0] 
           p(eval#1) = [1]                   
             p(main) = [2]                   
            p(sub#2) = [1] x2 + [1]          
           p(add#2#) = [1]                   
          p(eval#1#) = [2] x1 + [0]          
            p(main#) = [8] x1 + [8]          
           p(sub#2#) = [1]                   
              p(c_1) = [1] x1 + [1]          
              p(c_2) = [1]                   
              p(c_3) = [1] x1 + [1] x2 + [12]
              p(c_4) = [0]                   
              p(c_5) = [1] x1 + [1] x2 + [0] 
              p(c_6) = [4] x1 + [8]          
              p(c_7) = [2]                   
              p(c_8) = [1] x1 + [1]          
              p(c_9) = [1]                   
        
        Following rules are strictly oriented:
        eval#1#(Add(x2,x1)) = [2] x1 + [2] x2 + [16]      
                            > [2] x1 + [2] x2 + [12]      
                            = c_3(eval#1#(x2),eval#1#(x1))
        
        
        Following rules are (at-least) weakly oriented:
        eval#1#(Sub(x2,x1)) =  [2] x1 + [2] x2 + [2]       
                            >= [2] x1 + [2] x2 + [0]       
                            =  c_5(eval#1#(x2),eval#1#(x1))
        
                 main#(x12) =  [8] x12 + [8]               
                            >= [8] x12 + [8]               
                            =  c_6(eval#1#(x12))           
        
** Step 23.a:6: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            eval#1#(Add(x2,x1)) -> c_3(eval#1#(x2),eval#1#(x1))
            eval#1#(Sub(x2,x1)) -> c_5(eval#1#(x2),eval#1#(x1))
            main#(x12) -> c_6(eval#1#(x12))
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/2,c_4/0,c_5/2,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

** Step 23.b:1: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
            sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
        - Weak DPs:
            eval#1#(Add(x2,x1)) -> add#2#(eval#1(x2),eval#1(x1))
            eval#1#(Add(x2,x1)) -> eval#1#(x1)
            eval#1#(Add(x2,x1)) -> eval#1#(x2)
            eval#1#(Sub(x2,x1)) -> eval#1#(x1)
            eval#1#(Sub(x2,x1)) -> eval#1#(x2)
            eval#1#(Sub(x2,x1)) -> sub#2#(eval#1(x2),eval#1(x1))
            main#(x12) -> eval#1#(x12)
        - Weak TRS:
            add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
            add#2(Zero(),x8) -> x8
            eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
            eval#1(Nat(x1)) -> x1
            eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
            sub#2(x8,Zero()) -> x8
            sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
            sub#2(Zero(),Succ(x16)) -> Zero()
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(Succ) = {1},
            uargs(add#2) = {1,2},
            uargs(sub#2) = {1,2},
            uargs(add#2#) = {1,2},
            uargs(sub#2#) = {1,2},
            uargs(c_1) = {1},
            uargs(c_8) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                p(Add) = [1] x1 + [1] x2 + [2]
                p(Nat) = [1] x1 + [1]         
                p(Sub) = [1] x1 + [1] x2 + [2]
               p(Succ) = [1] x1 + [2]         
               p(Zero) = [3]                  
              p(add#2) = [1] x1 + [1] x2 + [2]
             p(eval#1) = [2] x1 + [2]         
               p(main) = [2] x1 + [0]         
              p(sub#2) = [1] x1 + [1] x2 + [0]
             p(add#2#) = [1] x1 + [1] x2 + [6]
            p(eval#1#) = [5] x1 + [1]         
              p(main#) = [7] x1 + [1]         
             p(sub#2#) = [1] x1 + [1] x2 + [2]
                p(c_1) = [1] x1 + [0]         
                p(c_2) = [0]                  
                p(c_3) = [0]                  
                p(c_4) = [0]                  
                p(c_5) = [0]                  
                p(c_6) = [0]                  
                p(c_7) = [0]                  
                p(c_8) = [1] x1 + [3]         
                p(c_9) = [0]                  
          
          Following rules are strictly oriented:
                add#2#(Succ(x4),x2) = [1] x2 + [1] x4 + [8]
                                    > [1] x2 + [1] x4 + [6]
                                    = c_1(add#2#(x4,x2))   
          
          sub#2#(Succ(x4),Succ(x2)) = [1] x2 + [1] x4 + [6]
                                    > [1] x2 + [1] x4 + [5]
                                    = c_8(sub#2#(x4,x2))   
          
          
          Following rules are (at-least) weakly oriented:
               eval#1#(Add(x2,x1)) =  [5] x1 + [5] x2 + [11]       
                                   >= [2] x1 + [2] x2 + [10]       
                                   =  add#2#(eval#1(x2),eval#1(x1))
          
               eval#1#(Add(x2,x1)) =  [5] x1 + [5] x2 + [11]       
                                   >= [5] x1 + [1]                 
                                   =  eval#1#(x1)                  
          
               eval#1#(Add(x2,x1)) =  [5] x1 + [5] x2 + [11]       
                                   >= [5] x2 + [1]                 
                                   =  eval#1#(x2)                  
          
               eval#1#(Sub(x2,x1)) =  [5] x1 + [5] x2 + [11]       
                                   >= [5] x1 + [1]                 
                                   =  eval#1#(x1)                  
          
               eval#1#(Sub(x2,x1)) =  [5] x1 + [5] x2 + [11]       
                                   >= [5] x2 + [1]                 
                                   =  eval#1#(x2)                  
          
               eval#1#(Sub(x2,x1)) =  [5] x1 + [5] x2 + [11]       
                                   >= [2] x1 + [2] x2 + [6]        
                                   =  sub#2#(eval#1(x2),eval#1(x1))
          
                        main#(x12) =  [7] x12 + [1]                
                                   >= [5] x12 + [1]                
                                   =  eval#1#(x12)                 
          
                add#2(Succ(x4),x2) =  [1] x2 + [1] x4 + [4]        
                                   >= [1] x2 + [1] x4 + [4]        
                                   =  Succ(add#2(x4,x2))           
          
                  add#2(Zero(),x8) =  [1] x8 + [5]                 
                                   >= [1] x8 + [0]                 
                                   =  x8                           
          
                eval#1(Add(x2,x1)) =  [2] x1 + [2] x2 + [6]        
                                   >= [2] x1 + [2] x2 + [6]        
                                   =  add#2(eval#1(x2),eval#1(x1)) 
          
                   eval#1(Nat(x1)) =  [2] x1 + [4]                 
                                   >= [1] x1 + [0]                 
                                   =  x1                           
          
                eval#1(Sub(x2,x1)) =  [2] x1 + [2] x2 + [6]        
                                   >= [2] x1 + [2] x2 + [4]        
                                   =  sub#2(eval#1(x2),eval#1(x1)) 
          
                  sub#2(x8,Zero()) =  [1] x8 + [3]                 
                                   >= [1] x8 + [0]                 
                                   =  x8                           
          
          sub#2(Succ(x4),Succ(x2)) =  [1] x2 + [1] x4 + [4]        
                                   >= [1] x2 + [1] x4 + [0]        
                                   =  sub#2(x4,x2)                 
          
           sub#2(Zero(),Succ(x16)) =  [1] x16 + [5]                
                                   >= [3]                          
                                   =  Zero()                       
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 23.b:2: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            add#2#(Succ(x4),x2) -> c_1(add#2#(x4,x2))
            eval#1#(Add(x2,x1)) -> add#2#(eval#1(x2),eval#1(x1))
            eval#1#(Add(x2,x1)) -> eval#1#(x1)
            eval#1#(Add(x2,x1)) -> eval#1#(x2)
            eval#1#(Sub(x2,x1)) -> eval#1#(x1)
            eval#1#(Sub(x2,x1)) -> eval#1#(x2)
            eval#1#(Sub(x2,x1)) -> sub#2#(eval#1(x2),eval#1(x1))
            main#(x12) -> eval#1#(x12)
            sub#2#(Succ(x4),Succ(x2)) -> c_8(sub#2#(x4,x2))
        - Weak TRS:
            add#2(Succ(x4),x2) -> Succ(add#2(x4,x2))
            add#2(Zero(),x8) -> x8
            eval#1(Add(x2,x1)) -> add#2(eval#1(x2),eval#1(x1))
            eval#1(Nat(x1)) -> x1
            eval#1(Sub(x2,x1)) -> sub#2(eval#1(x2),eval#1(x1))
            sub#2(x8,Zero()) -> x8
            sub#2(Succ(x4),Succ(x2)) -> sub#2(x4,x2)
            sub#2(Zero(),Succ(x16)) -> Zero()
        - Signature:
            {add#2/2,eval#1/1,main/1,sub#2/2,add#2#/2,eval#1#/1,main#/1,sub#2#/2} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0
            ,c_1/1,c_2/0,c_3/3,c_4/0,c_5/3,c_6/1,c_7/0,c_8/1,c_9/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main#} and constructors {Add,Nat,Sub,Succ,Zero}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^2))