WORST_CASE(?,O(n^1))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  concat(A,B) -> m4(A,B)                        [A >= 0 && B >= 0]                                                 (1,1)
          1.  m0(A,B)     -> m1(A,B)                        [A >= 0 && B >= A]                                                 (?,1)
          2.  m2(A,B)     -> m3(A,B)                        [B >= A]                                                           (?,1)
          3.  m8(A,B)     -> m0(C,B)                        [A >= 0 && B >= 1 + A && 1 + A >= C && C >= 1 + A]                 (?,1)
          4.  m1(A,B)     -> m8(A,B)                        True                                                               (?,1)
          5.  m1(A,B)     -> m6(A,B)                        True                                                               (?,1)
          6.  m9(A,B)     -> m2(C,B)                        [B >= C && 1 + A >= C && C >= 1 + A]                               (?,1)
          7.  m3(A,B)     -> m9(A,B)                        True                                                               (?,1)
          8.  m3(A,B)     -> m7(A,B)                        True                                                               (?,1)
          9.  n00(A,B)    -> m5(A,B)                        True                                                               (?,1)
          10. n01(A,B)    -> m0(0,B)                        True                                                               (?,1)
          11. n02(A,B)    -> m2(B,A)                        True                                                               (?,1)
          12. n0(A,B)     -> c3(n00(D,C),n01(D,C),n02(D,C)) [C >= 0 && D >= C && B >= C && C >= B && A + C >= D && D >= A + C] (?,1)
          13. m4(A,B)     -> n0(A,B)                        [A >= 0 && B >= 0]                                                 (?,1)
        Signature:
          {(concat,2)
          ;(m0,2)
          ;(m1,2)
          ;(m2,2)
          ;(m3,2)
          ;(m4,2)
          ;(m5,2)
          ;(m6,2)
          ;(m7,2)
          ;(m8,2)
          ;(m9,2)
          ;(n0,2)
          ;(n00,2)
          ;(n01,2)
          ;(n02,2)}
        Flow Graph:
          [0->{13},1->{4,5},2->{7,8},3->{1},4->{3},5->{},6->{2},7->{6},8->{},9->{},10->{1},11->{2},12->{9,10,11}
          ,13->{12}]
        
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (< 0,0,A>,         A, .= 0) (< 0,0,B>, B, .= 0) 
          (< 1,0,A>,         A, .= 0) (< 1,0,B>, B, .= 0) 
          (< 2,0,A>,         A, .= 0) (< 2,0,B>, B, .= 0) 
          (< 3,0,A>, 1 + A + B, .* 1) (< 3,0,B>, B, .= 0) 
          (< 4,0,A>,         A, .= 0) (< 4,0,B>, B, .= 0) 
          (< 5,0,A>,         A, .= 0) (< 5,0,B>, B, .= 0) 
          (< 6,0,A>, 1 + A + B, .* 1) (< 6,0,B>, B, .= 0) 
          (< 7,0,A>,         A, .= 0) (< 7,0,B>, B, .= 0) 
          (< 8,0,A>,         A, .= 0) (< 8,0,B>, B, .= 0) 
          (< 9,0,A>,         A, .= 0) (< 9,0,B>, B, .= 0) 
          (<10,0,A>,         0, .= 0) (<10,0,B>, B, .= 0) 
          (<11,0,A>,         B, .= 0) (<11,0,B>, A, .= 0) 
          (<12,0,A>,     A + B, .* 0) (<12,0,B>, B, .= 0) 
          (<12,1,A>,     A + B, .* 0) (<12,1,B>, B, .= 0) 
          (<12,2,A>,     A + B, .* 0) (<12,2,B>, B, .= 0) 
          (<13,0,A>,         A, .= 0) (<13,0,B>, B, .= 0) 
* Step 2: SizeboundsProc WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  concat(A,B) -> m4(A,B)                        [A >= 0 && B >= 0]                                                 (1,1)
          1.  m0(A,B)     -> m1(A,B)                        [A >= 0 && B >= A]                                                 (?,1)
          2.  m2(A,B)     -> m3(A,B)                        [B >= A]                                                           (?,1)
          3.  m8(A,B)     -> m0(C,B)                        [A >= 0 && B >= 1 + A && 1 + A >= C && C >= 1 + A]                 (?,1)
          4.  m1(A,B)     -> m8(A,B)                        True                                                               (?,1)
          5.  m1(A,B)     -> m6(A,B)                        True                                                               (?,1)
          6.  m9(A,B)     -> m2(C,B)                        [B >= C && 1 + A >= C && C >= 1 + A]                               (?,1)
          7.  m3(A,B)     -> m9(A,B)                        True                                                               (?,1)
          8.  m3(A,B)     -> m7(A,B)                        True                                                               (?,1)
          9.  n00(A,B)    -> m5(A,B)                        True                                                               (?,1)
          10. n01(A,B)    -> m0(0,B)                        True                                                               (?,1)
          11. n02(A,B)    -> m2(B,A)                        True                                                               (?,1)
          12. n0(A,B)     -> c3(n00(D,C),n01(D,C),n02(D,C)) [C >= 0 && D >= C && B >= C && C >= B && A + C >= D && D >= A + C] (?,1)
          13. m4(A,B)     -> n0(A,B)                        [A >= 0 && B >= 0]                                                 (?,1)
        Signature:
          {(concat,2)
          ;(m0,2)
          ;(m1,2)
          ;(m2,2)
          ;(m3,2)
          ;(m4,2)
          ;(m5,2)
          ;(m6,2)
          ;(m7,2)
          ;(m8,2)
          ;(m9,2)
          ;(n0,2)
          ;(n00,2)
          ;(n01,2)
          ;(n02,2)}
        Flow Graph:
          [0->{13},1->{4,5},2->{7,8},3->{1},4->{3},5->{},6->{2},7->{6},8->{},9->{},10->{1},11->{2},12->{9,10,11}
          ,13->{12}]
        Sizebounds:
          (< 0,0,A>, ?) (< 0,0,B>, ?) 
          (< 1,0,A>, ?) (< 1,0,B>, ?) 
          (< 2,0,A>, ?) (< 2,0,B>, ?) 
          (< 3,0,A>, ?) (< 3,0,B>, ?) 
          (< 4,0,A>, ?) (< 4,0,B>, ?) 
          (< 5,0,A>, ?) (< 5,0,B>, ?) 
          (< 6,0,A>, ?) (< 6,0,B>, ?) 
          (< 7,0,A>, ?) (< 7,0,B>, ?) 
          (< 8,0,A>, ?) (< 8,0,B>, ?) 
          (< 9,0,A>, ?) (< 9,0,B>, ?) 
          (<10,0,A>, ?) (<10,0,B>, ?) 
          (<11,0,A>, ?) (<11,0,B>, ?) 
          (<12,0,A>, ?) (<12,0,B>, ?) 
          (<12,1,A>, ?) (<12,1,B>, ?) 
          (<12,2,A>, ?) (<12,2,B>, ?) 
          (<13,0,A>, ?) (<13,0,B>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (< 0,0,A>,     A) (< 0,0,B>,     B) 
          (< 1,0,A>,     B) (< 1,0,B>,     B) 
          (< 2,0,A>, A + B) (< 2,0,B>, A + B) 
          (< 3,0,A>,     1) (< 3,0,B>,     B) 
          (< 4,0,A>,     B) (< 4,0,B>,     B) 
          (< 5,0,A>,     B) (< 5,0,B>,     B) 
          (< 6,0,A>,     1) (< 6,0,B>, A + B) 
          (< 7,0,A>, A + B) (< 7,0,B>, A + B) 
          (< 8,0,A>, A + B) (< 8,0,B>, A + B) 
          (< 9,0,A>, A + B) (< 9,0,B>,     B) 
          (<10,0,A>,     0) (<10,0,B>,     B) 
          (<11,0,A>,     B) (<11,0,B>, A + B) 
          (<12,0,A>, A + B) (<12,0,B>,     B) 
          (<12,1,A>, A + B) (<12,1,B>,     B) 
          (<12,2,A>, A + B) (<12,2,B>,     B) 
          (<13,0,A>,     A) (<13,0,B>,     B) 
* Step 3: LeafRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  concat(A,B) -> m4(A,B)                        [A >= 0 && B >= 0]                                                 (1,1)
          1.  m0(A,B)     -> m1(A,B)                        [A >= 0 && B >= A]                                                 (?,1)
          2.  m2(A,B)     -> m3(A,B)                        [B >= A]                                                           (?,1)
          3.  m8(A,B)     -> m0(C,B)                        [A >= 0 && B >= 1 + A && 1 + A >= C && C >= 1 + A]                 (?,1)
          4.  m1(A,B)     -> m8(A,B)                        True                                                               (?,1)
          5.  m1(A,B)     -> m6(A,B)                        True                                                               (?,1)
          6.  m9(A,B)     -> m2(C,B)                        [B >= C && 1 + A >= C && C >= 1 + A]                               (?,1)
          7.  m3(A,B)     -> m9(A,B)                        True                                                               (?,1)
          8.  m3(A,B)     -> m7(A,B)                        True                                                               (?,1)
          9.  n00(A,B)    -> m5(A,B)                        True                                                               (?,1)
          10. n01(A,B)    -> m0(0,B)                        True                                                               (?,1)
          11. n02(A,B)    -> m2(B,A)                        True                                                               (?,1)
          12. n0(A,B)     -> c3(n00(D,C),n01(D,C),n02(D,C)) [C >= 0 && D >= C && B >= C && C >= B && A + C >= D && D >= A + C] (?,1)
          13. m4(A,B)     -> n0(A,B)                        [A >= 0 && B >= 0]                                                 (?,1)
        Signature:
          {(concat,2)
          ;(m0,2)
          ;(m1,2)
          ;(m2,2)
          ;(m3,2)
          ;(m4,2)
          ;(m5,2)
          ;(m6,2)
          ;(m7,2)
          ;(m8,2)
          ;(m9,2)
          ;(n0,2)
          ;(n00,2)
          ;(n01,2)
          ;(n02,2)}
        Flow Graph:
          [0->{13},1->{4,5},2->{7,8},3->{1},4->{3},5->{},6->{2},7->{6},8->{},9->{},10->{1},11->{2},12->{9,10,11}
          ,13->{12}]
        Sizebounds:
          (< 0,0,A>,     A) (< 0,0,B>,     B) 
          (< 1,0,A>,     B) (< 1,0,B>,     B) 
          (< 2,0,A>, A + B) (< 2,0,B>, A + B) 
          (< 3,0,A>,     1) (< 3,0,B>,     B) 
          (< 4,0,A>,     B) (< 4,0,B>,     B) 
          (< 5,0,A>,     B) (< 5,0,B>,     B) 
          (< 6,0,A>,     1) (< 6,0,B>, A + B) 
          (< 7,0,A>, A + B) (< 7,0,B>, A + B) 
          (< 8,0,A>, A + B) (< 8,0,B>, A + B) 
          (< 9,0,A>, A + B) (< 9,0,B>,     B) 
          (<10,0,A>,     0) (<10,0,B>,     B) 
          (<11,0,A>,     B) (<11,0,B>, A + B) 
          (<12,0,A>, A + B) (<12,0,B>,     B) 
          (<12,1,A>, A + B) (<12,1,B>,     B) 
          (<12,2,A>, A + B) (<12,2,B>,     B) 
          (<13,0,A>,     A) (<13,0,B>,     B) 
    + Applied Processor:
        LeafRules
    + Details:
        The following transitions are estimated by its predecessors and are removed [5,8,9]
* Step 4: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  concat(A,B) -> m4(A,B)                        [A >= 0 && B >= 0]                                                 (1,1)
          1.  m0(A,B)     -> m1(A,B)                        [A >= 0 && B >= A]                                                 (?,1)
          2.  m2(A,B)     -> m3(A,B)                        [B >= A]                                                           (?,1)
          3.  m8(A,B)     -> m0(C,B)                        [A >= 0 && B >= 1 + A && 1 + A >= C && C >= 1 + A]                 (?,1)
          4.  m1(A,B)     -> m8(A,B)                        True                                                               (?,1)
          6.  m9(A,B)     -> m2(C,B)                        [B >= C && 1 + A >= C && C >= 1 + A]                               (?,1)
          7.  m3(A,B)     -> m9(A,B)                        True                                                               (?,1)
          10. n01(A,B)    -> m0(0,B)                        True                                                               (?,1)
          11. n02(A,B)    -> m2(B,A)                        True                                                               (?,1)
          12. n0(A,B)     -> c3(n00(D,C),n01(D,C),n02(D,C)) [C >= 0 && D >= C && B >= C && C >= B && A + C >= D && D >= A + C] (?,1)
          13. m4(A,B)     -> n0(A,B)                        [A >= 0 && B >= 0]                                                 (?,1)
        Signature:
          {(concat,2)
          ;(m0,2)
          ;(m1,2)
          ;(m2,2)
          ;(m3,2)
          ;(m4,2)
          ;(m5,2)
          ;(m6,2)
          ;(m7,2)
          ;(m8,2)
          ;(m9,2)
          ;(n0,2)
          ;(n00,2)
          ;(n01,2)
          ;(n02,2)}
        Flow Graph:
          [0->{13},1->{4},2->{7},3->{1},4->{3},6->{2},7->{6},10->{1},11->{2},12->{10,11},13->{12}]
        Sizebounds:
          (< 0,0,A>,     A) (< 0,0,B>,     B) 
          (< 1,0,A>,     B) (< 1,0,B>,     B) 
          (< 2,0,A>, A + B) (< 2,0,B>, A + B) 
          (< 3,0,A>,     1) (< 3,0,B>,     B) 
          (< 4,0,A>,     B) (< 4,0,B>,     B) 
          (< 6,0,A>,     1) (< 6,0,B>, A + B) 
          (< 7,0,A>, A + B) (< 7,0,B>, A + B) 
          (<10,0,A>,     0) (<10,0,B>,     B) 
          (<11,0,A>,     B) (<11,0,B>, A + B) 
          (<12,0,A>, A + B) (<12,0,B>,     B) 
          (<12,1,A>, A + B) (<12,1,B>,     B) 
          (<12,2,A>, A + B) (<12,2,B>,     B) 
          (<13,0,A>,     A) (<13,0,B>,     B) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(concat) = 1
              p(m0) = 0
              p(m1) = 0
              p(m2) = 0
              p(m3) = 0
              p(m4) = 1
              p(m8) = 0
              p(m9) = 0
              p(n0) = 0
             p(n00) = 0
             p(n01) = 0
             p(n02) = 0
        
        The following rules are strictly oriented:
        [A >= 0 && B >= 0] ==>        
                   m4(A,B)   = 1      
                             > 0      
                             = n0(A,B)
        
        
        The following rules are weakly oriented:
                                                        [A >= 0 && B >= 0] ==>                               
                                                               concat(A,B)   = 1                             
                                                                            >= 1                             
                                                                             = m4(A,B)                       
        
                                                        [A >= 0 && B >= A] ==>                               
                                                                   m0(A,B)   = 0                             
                                                                            >= 0                             
                                                                             = m1(A,B)                       
        
                                                                  [B >= A] ==>                               
                                                                   m2(A,B)   = 0                             
                                                                            >= 0                             
                                                                             = m3(A,B)                       
        
                        [A >= 0 && B >= 1 + A && 1 + A >= C && C >= 1 + A] ==>                               
                                                                   m8(A,B)   = 0                             
                                                                            >= 0                             
                                                                             = m0(C,B)                       
        
                                                                      True ==>                               
                                                                   m1(A,B)   = 0                             
                                                                            >= 0                             
                                                                             = m8(A,B)                       
        
                                      [B >= C && 1 + A >= C && C >= 1 + A] ==>                               
                                                                   m9(A,B)   = 0                             
                                                                            >= 0                             
                                                                             = m2(C,B)                       
        
                                                                      True ==>                               
                                                                   m3(A,B)   = 0                             
                                                                            >= 0                             
                                                                             = m9(A,B)                       
        
                                                                      True ==>                               
                                                                  n01(A,B)   = 0                             
                                                                            >= 0                             
                                                                             = m0(0,B)                       
        
                                                                      True ==>                               
                                                                  n02(A,B)   = 0                             
                                                                            >= 0                             
                                                                             = m2(B,A)                       
        
        [C >= 0 && D >= C && B >= C && C >= B && A + C >= D && D >= A + C] ==>                               
                                                                   n0(A,B)   = 0                             
                                                                            >= 0                             
                                                                             = c3(n00(D,C),n01(D,C),n02(D,C))
        
        
* Step 5: KnowledgePropagation WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  concat(A,B) -> m4(A,B)                        [A >= 0 && B >= 0]                                                 (1,1)
          1.  m0(A,B)     -> m1(A,B)                        [A >= 0 && B >= A]                                                 (?,1)
          2.  m2(A,B)     -> m3(A,B)                        [B >= A]                                                           (?,1)
          3.  m8(A,B)     -> m0(C,B)                        [A >= 0 && B >= 1 + A && 1 + A >= C && C >= 1 + A]                 (?,1)
          4.  m1(A,B)     -> m8(A,B)                        True                                                               (?,1)
          6.  m9(A,B)     -> m2(C,B)                        [B >= C && 1 + A >= C && C >= 1 + A]                               (?,1)
          7.  m3(A,B)     -> m9(A,B)                        True                                                               (?,1)
          10. n01(A,B)    -> m0(0,B)                        True                                                               (?,1)
          11. n02(A,B)    -> m2(B,A)                        True                                                               (?,1)
          12. n0(A,B)     -> c3(n00(D,C),n01(D,C),n02(D,C)) [C >= 0 && D >= C && B >= C && C >= B && A + C >= D && D >= A + C] (?,1)
          13. m4(A,B)     -> n0(A,B)                        [A >= 0 && B >= 0]                                                 (1,1)
        Signature:
          {(concat,2)
          ;(m0,2)
          ;(m1,2)
          ;(m2,2)
          ;(m3,2)
          ;(m4,2)
          ;(m5,2)
          ;(m6,2)
          ;(m7,2)
          ;(m8,2)
          ;(m9,2)
          ;(n0,2)
          ;(n00,2)
          ;(n01,2)
          ;(n02,2)}
        Flow Graph:
          [0->{13},1->{4},2->{7},3->{1},4->{3},6->{2},7->{6},10->{1},11->{2},12->{10,11},13->{12}]
        Sizebounds:
          (< 0,0,A>,     A) (< 0,0,B>,     B) 
          (< 1,0,A>,     B) (< 1,0,B>,     B) 
          (< 2,0,A>, A + B) (< 2,0,B>, A + B) 
          (< 3,0,A>,     1) (< 3,0,B>,     B) 
          (< 4,0,A>,     B) (< 4,0,B>,     B) 
          (< 6,0,A>,     1) (< 6,0,B>, A + B) 
          (< 7,0,A>, A + B) (< 7,0,B>, A + B) 
          (<10,0,A>,     0) (<10,0,B>,     B) 
          (<11,0,A>,     B) (<11,0,B>, A + B) 
          (<12,0,A>, A + B) (<12,0,B>,     B) 
          (<12,1,A>, A + B) (<12,1,B>,     B) 
          (<12,2,A>, A + B) (<12,2,B>,     B) 
          (<13,0,A>,     A) (<13,0,B>,     B) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        We propagate bounds from predecessors.
* Step 6: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  concat(A,B) -> m4(A,B)                        [A >= 0 && B >= 0]                                                 (1,1)
          1.  m0(A,B)     -> m1(A,B)                        [A >= 0 && B >= A]                                                 (?,1)
          2.  m2(A,B)     -> m3(A,B)                        [B >= A]                                                           (?,1)
          3.  m8(A,B)     -> m0(C,B)                        [A >= 0 && B >= 1 + A && 1 + A >= C && C >= 1 + A]                 (?,1)
          4.  m1(A,B)     -> m8(A,B)                        True                                                               (?,1)
          6.  m9(A,B)     -> m2(C,B)                        [B >= C && 1 + A >= C && C >= 1 + A]                               (?,1)
          7.  m3(A,B)     -> m9(A,B)                        True                                                               (?,1)
          10. n01(A,B)    -> m0(0,B)                        True                                                               (1,1)
          11. n02(A,B)    -> m2(B,A)                        True                                                               (1,1)
          12. n0(A,B)     -> c3(n00(D,C),n01(D,C),n02(D,C)) [C >= 0 && D >= C && B >= C && C >= B && A + C >= D && D >= A + C] (1,1)
          13. m4(A,B)     -> n0(A,B)                        [A >= 0 && B >= 0]                                                 (1,1)
        Signature:
          {(concat,2)
          ;(m0,2)
          ;(m1,2)
          ;(m2,2)
          ;(m3,2)
          ;(m4,2)
          ;(m5,2)
          ;(m6,2)
          ;(m7,2)
          ;(m8,2)
          ;(m9,2)
          ;(n0,2)
          ;(n00,2)
          ;(n01,2)
          ;(n02,2)}
        Flow Graph:
          [0->{13},1->{4},2->{7},3->{1},4->{3},6->{2},7->{6},10->{1},11->{2},12->{10,11},13->{12}]
        Sizebounds:
          (< 0,0,A>,     A) (< 0,0,B>,     B) 
          (< 1,0,A>,     B) (< 1,0,B>,     B) 
          (< 2,0,A>, A + B) (< 2,0,B>, A + B) 
          (< 3,0,A>,     1) (< 3,0,B>,     B) 
          (< 4,0,A>,     B) (< 4,0,B>,     B) 
          (< 6,0,A>,     1) (< 6,0,B>, A + B) 
          (< 7,0,A>, A + B) (< 7,0,B>, A + B) 
          (<10,0,A>,     0) (<10,0,B>,     B) 
          (<11,0,A>,     B) (<11,0,B>, A + B) 
          (<12,0,A>, A + B) (<12,0,B>,     B) 
          (<12,1,A>, A + B) (<12,1,B>,     B) 
          (<12,2,A>, A + B) (<12,2,B>,     B) 
          (<13,0,A>,     A) (<13,0,B>,     B) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [2,6,7], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(m2) = 1 + -1*x1 + x2
          p(m3) = 1 + -1*x1 + x2
          p(m9) = 1 + -1*x1 + x2
        
        The following rules are strictly oriented:
        [B >= C && 1 + A >= C && C >= 1 + A] ==>             
                                     m9(A,B)   = 1 + -1*A + B
                                               > 1 + B + -1*C
                                               = m2(C,B)     
        
        
        The following rules are weakly oriented:
         [B >= A] ==>             
          m2(A,B)   = 1 + -1*A + B
                   >= 1 + -1*A + B
                    = m3(A,B)     
        
             True ==>             
          m3(A,B)   = 1 + -1*A + B
                   >= 1 + -1*A + B
                    = m9(A,B)     
        
        We use the following global sizebounds:
        (< 0,0,A>,     A) (< 0,0,B>,     B) 
        (< 1,0,A>,     B) (< 1,0,B>,     B) 
        (< 2,0,A>, A + B) (< 2,0,B>, A + B) 
        (< 3,0,A>,     1) (< 3,0,B>,     B) 
        (< 4,0,A>,     B) (< 4,0,B>,     B) 
        (< 6,0,A>,     1) (< 6,0,B>, A + B) 
        (< 7,0,A>, A + B) (< 7,0,B>, A + B) 
        (<10,0,A>,     0) (<10,0,B>,     B) 
        (<11,0,A>,     B) (<11,0,B>, A + B) 
        (<12,0,A>, A + B) (<12,0,B>,     B) 
        (<12,1,A>, A + B) (<12,1,B>,     B) 
        (<12,2,A>, A + B) (<12,2,B>,     B) 
        (<13,0,A>,     A) (<13,0,B>,     B) 
* Step 7: KnowledgePropagation WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  concat(A,B) -> m4(A,B)                        [A >= 0 && B >= 0]                                                 (1,1)          
          1.  m0(A,B)     -> m1(A,B)                        [A >= 0 && B >= A]                                                 (?,1)          
          2.  m2(A,B)     -> m3(A,B)                        [B >= A]                                                           (?,1)          
          3.  m8(A,B)     -> m0(C,B)                        [A >= 0 && B >= 1 + A && 1 + A >= C && C >= 1 + A]                 (?,1)          
          4.  m1(A,B)     -> m8(A,B)                        True                                                               (?,1)          
          6.  m9(A,B)     -> m2(C,B)                        [B >= C && 1 + A >= C && C >= 1 + A]                               (1 + A + 2*B,1)
          7.  m3(A,B)     -> m9(A,B)                        True                                                               (?,1)          
          10. n01(A,B)    -> m0(0,B)                        True                                                               (1,1)          
          11. n02(A,B)    -> m2(B,A)                        True                                                               (1,1)          
          12. n0(A,B)     -> c3(n00(D,C),n01(D,C),n02(D,C)) [C >= 0 && D >= C && B >= C && C >= B && A + C >= D && D >= A + C] (1,1)          
          13. m4(A,B)     -> n0(A,B)                        [A >= 0 && B >= 0]                                                 (1,1)          
        Signature:
          {(concat,2)
          ;(m0,2)
          ;(m1,2)
          ;(m2,2)
          ;(m3,2)
          ;(m4,2)
          ;(m5,2)
          ;(m6,2)
          ;(m7,2)
          ;(m8,2)
          ;(m9,2)
          ;(n0,2)
          ;(n00,2)
          ;(n01,2)
          ;(n02,2)}
        Flow Graph:
          [0->{13},1->{4},2->{7},3->{1},4->{3},6->{2},7->{6},10->{1},11->{2},12->{10,11},13->{12}]
        Sizebounds:
          (< 0,0,A>,     A) (< 0,0,B>,     B) 
          (< 1,0,A>,     B) (< 1,0,B>,     B) 
          (< 2,0,A>, A + B) (< 2,0,B>, A + B) 
          (< 3,0,A>,     1) (< 3,0,B>,     B) 
          (< 4,0,A>,     B) (< 4,0,B>,     B) 
          (< 6,0,A>,     1) (< 6,0,B>, A + B) 
          (< 7,0,A>, A + B) (< 7,0,B>, A + B) 
          (<10,0,A>,     0) (<10,0,B>,     B) 
          (<11,0,A>,     B) (<11,0,B>, A + B) 
          (<12,0,A>, A + B) (<12,0,B>,     B) 
          (<12,1,A>, A + B) (<12,1,B>,     B) 
          (<12,2,A>, A + B) (<12,2,B>,     B) 
          (<13,0,A>,     A) (<13,0,B>,     B) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        We propagate bounds from predecessors.
* Step 8: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  concat(A,B) -> m4(A,B)                        [A >= 0 && B >= 0]                                                 (1,1)          
          1.  m0(A,B)     -> m1(A,B)                        [A >= 0 && B >= A]                                                 (?,1)          
          2.  m2(A,B)     -> m3(A,B)                        [B >= A]                                                           (2 + A + 2*B,1)
          3.  m8(A,B)     -> m0(C,B)                        [A >= 0 && B >= 1 + A && 1 + A >= C && C >= 1 + A]                 (?,1)          
          4.  m1(A,B)     -> m8(A,B)                        True                                                               (?,1)          
          6.  m9(A,B)     -> m2(C,B)                        [B >= C && 1 + A >= C && C >= 1 + A]                               (1 + A + 2*B,1)
          7.  m3(A,B)     -> m9(A,B)                        True                                                               (2 + A + 2*B,1)
          10. n01(A,B)    -> m0(0,B)                        True                                                               (1,1)          
          11. n02(A,B)    -> m2(B,A)                        True                                                               (1,1)          
          12. n0(A,B)     -> c3(n00(D,C),n01(D,C),n02(D,C)) [C >= 0 && D >= C && B >= C && C >= B && A + C >= D && D >= A + C] (1,1)          
          13. m4(A,B)     -> n0(A,B)                        [A >= 0 && B >= 0]                                                 (1,1)          
        Signature:
          {(concat,2)
          ;(m0,2)
          ;(m1,2)
          ;(m2,2)
          ;(m3,2)
          ;(m4,2)
          ;(m5,2)
          ;(m6,2)
          ;(m7,2)
          ;(m8,2)
          ;(m9,2)
          ;(n0,2)
          ;(n00,2)
          ;(n01,2)
          ;(n02,2)}
        Flow Graph:
          [0->{13},1->{4},2->{7},3->{1},4->{3},6->{2},7->{6},10->{1},11->{2},12->{10,11},13->{12}]
        Sizebounds:
          (< 0,0,A>,     A) (< 0,0,B>,     B) 
          (< 1,0,A>,     B) (< 1,0,B>,     B) 
          (< 2,0,A>, A + B) (< 2,0,B>, A + B) 
          (< 3,0,A>,     1) (< 3,0,B>,     B) 
          (< 4,0,A>,     B) (< 4,0,B>,     B) 
          (< 6,0,A>,     1) (< 6,0,B>, A + B) 
          (< 7,0,A>, A + B) (< 7,0,B>, A + B) 
          (<10,0,A>,     0) (<10,0,B>,     B) 
          (<11,0,A>,     B) (<11,0,B>, A + B) 
          (<12,0,A>, A + B) (<12,0,B>,     B) 
          (<12,1,A>, A + B) (<12,1,B>,     B) 
          (<12,2,A>, A + B) (<12,2,B>,     B) 
          (<13,0,A>,     A) (<13,0,B>,     B) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [1,3,4], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(m0) = 1 + -1*x1 + x2
          p(m1) = 1 + -1*x1 + x2
          p(m8) = 1 + -1*x1 + x2
        
        The following rules are strictly oriented:
        [A >= 0 && B >= 1 + A && 1 + A >= C && C >= 1 + A] ==>             
                                                   m8(A,B)   = 1 + -1*A + B
                                                             > 1 + B + -1*C
                                                             = m0(C,B)     
        
        
        The following rules are weakly oriented:
        [A >= 0 && B >= A] ==>             
                   m0(A,B)   = 1 + -1*A + B
                            >= 1 + -1*A + B
                             = m1(A,B)     
        
                      True ==>             
                   m1(A,B)   = 1 + -1*A + B
                            >= 1 + -1*A + B
                             = m8(A,B)     
        
        We use the following global sizebounds:
        (< 0,0,A>,     A) (< 0,0,B>,     B) 
        (< 1,0,A>,     B) (< 1,0,B>,     B) 
        (< 2,0,A>, A + B) (< 2,0,B>, A + B) 
        (< 3,0,A>,     1) (< 3,0,B>,     B) 
        (< 4,0,A>,     B) (< 4,0,B>,     B) 
        (< 6,0,A>,     1) (< 6,0,B>, A + B) 
        (< 7,0,A>, A + B) (< 7,0,B>, A + B) 
        (<10,0,A>,     0) (<10,0,B>,     B) 
        (<11,0,A>,     B) (<11,0,B>, A + B) 
        (<12,0,A>, A + B) (<12,0,B>,     B) 
        (<12,1,A>, A + B) (<12,1,B>,     B) 
        (<12,2,A>, A + B) (<12,2,B>,     B) 
        (<13,0,A>,     A) (<13,0,B>,     B) 
* Step 9: KnowledgePropagation WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  concat(A,B) -> m4(A,B)                        [A >= 0 && B >= 0]                                                 (1,1)          
          1.  m0(A,B)     -> m1(A,B)                        [A >= 0 && B >= A]                                                 (?,1)          
          2.  m2(A,B)     -> m3(A,B)                        [B >= A]                                                           (2 + A + 2*B,1)
          3.  m8(A,B)     -> m0(C,B)                        [A >= 0 && B >= 1 + A && 1 + A >= C && C >= 1 + A]                 (1 + B,1)      
          4.  m1(A,B)     -> m8(A,B)                        True                                                               (?,1)          
          6.  m9(A,B)     -> m2(C,B)                        [B >= C && 1 + A >= C && C >= 1 + A]                               (1 + A + 2*B,1)
          7.  m3(A,B)     -> m9(A,B)                        True                                                               (2 + A + 2*B,1)
          10. n01(A,B)    -> m0(0,B)                        True                                                               (1,1)          
          11. n02(A,B)    -> m2(B,A)                        True                                                               (1,1)          
          12. n0(A,B)     -> c3(n00(D,C),n01(D,C),n02(D,C)) [C >= 0 && D >= C && B >= C && C >= B && A + C >= D && D >= A + C] (1,1)          
          13. m4(A,B)     -> n0(A,B)                        [A >= 0 && B >= 0]                                                 (1,1)          
        Signature:
          {(concat,2)
          ;(m0,2)
          ;(m1,2)
          ;(m2,2)
          ;(m3,2)
          ;(m4,2)
          ;(m5,2)
          ;(m6,2)
          ;(m7,2)
          ;(m8,2)
          ;(m9,2)
          ;(n0,2)
          ;(n00,2)
          ;(n01,2)
          ;(n02,2)}
        Flow Graph:
          [0->{13},1->{4},2->{7},3->{1},4->{3},6->{2},7->{6},10->{1},11->{2},12->{10,11},13->{12}]
        Sizebounds:
          (< 0,0,A>,     A) (< 0,0,B>,     B) 
          (< 1,0,A>,     B) (< 1,0,B>,     B) 
          (< 2,0,A>, A + B) (< 2,0,B>, A + B) 
          (< 3,0,A>,     1) (< 3,0,B>,     B) 
          (< 4,0,A>,     B) (< 4,0,B>,     B) 
          (< 6,0,A>,     1) (< 6,0,B>, A + B) 
          (< 7,0,A>, A + B) (< 7,0,B>, A + B) 
          (<10,0,A>,     0) (<10,0,B>,     B) 
          (<11,0,A>,     B) (<11,0,B>, A + B) 
          (<12,0,A>, A + B) (<12,0,B>,     B) 
          (<12,1,A>, A + B) (<12,1,B>,     B) 
          (<12,2,A>, A + B) (<12,2,B>,     B) 
          (<13,0,A>,     A) (<13,0,B>,     B) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        We propagate bounds from predecessors.
* Step 10: LocalSizeboundsProc WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  concat(A,B) -> m4(A,B)                        [A >= 0 && B >= 0]                                                 (1,1)          
          1.  m0(A,B)     -> m1(A,B)                        [A >= 0 && B >= A]                                                 (2 + B,1)      
          2.  m2(A,B)     -> m3(A,B)                        [B >= A]                                                           (2 + A + 2*B,1)
          3.  m8(A,B)     -> m0(C,B)                        [A >= 0 && B >= 1 + A && 1 + A >= C && C >= 1 + A]                 (1 + B,1)      
          4.  m1(A,B)     -> m8(A,B)                        True                                                               (2 + B,1)      
          6.  m9(A,B)     -> m2(C,B)                        [B >= C && 1 + A >= C && C >= 1 + A]                               (1 + A + 2*B,1)
          7.  m3(A,B)     -> m9(A,B)                        True                                                               (2 + A + 2*B,1)
          10. n01(A,B)    -> m0(0,B)                        True                                                               (1,1)          
          11. n02(A,B)    -> m2(B,A)                        True                                                               (1,1)          
          12. n0(A,B)     -> c3(n00(D,C),n01(D,C),n02(D,C)) [C >= 0 && D >= C && B >= C && C >= B && A + C >= D && D >= A + C] (1,1)          
          13. m4(A,B)     -> n0(A,B)                        [A >= 0 && B >= 0]                                                 (1,1)          
        Signature:
          {(concat,2)
          ;(m0,2)
          ;(m1,2)
          ;(m2,2)
          ;(m3,2)
          ;(m4,2)
          ;(m5,2)
          ;(m6,2)
          ;(m7,2)
          ;(m8,2)
          ;(m9,2)
          ;(n0,2)
          ;(n00,2)
          ;(n01,2)
          ;(n02,2)}
        Flow Graph:
          [0->{13},1->{4},2->{7},3->{1},4->{3},6->{2},7->{6},10->{1},11->{2},12->{10,11},13->{12}]
        Sizebounds:
          (< 0,0,A>,     A) (< 0,0,B>,     B) 
          (< 1,0,A>,     B) (< 1,0,B>,     B) 
          (< 2,0,A>, A + B) (< 2,0,B>, A + B) 
          (< 3,0,A>,     1) (< 3,0,B>,     B) 
          (< 4,0,A>,     B) (< 4,0,B>,     B) 
          (< 6,0,A>,     1) (< 6,0,B>, A + B) 
          (< 7,0,A>, A + B) (< 7,0,B>, A + B) 
          (<10,0,A>,     0) (<10,0,B>,     B) 
          (<11,0,A>,     B) (<11,0,B>, A + B) 
          (<12,0,A>, A + B) (<12,0,B>,     B) 
          (<12,1,A>, A + B) (<12,1,B>,     B) 
          (<12,2,A>, A + B) (<12,2,B>,     B) 
          (<13,0,A>,     A) (<13,0,B>,     B) 
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        The problem is already solved.

WORST_CASE(?,O(n^1))