WORST_CASE(?,O(log(n)))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          0. divByTwo(A) -> m2(A)           [A >= 1]             (1,1)
          1. m0(A)       -> m1(A)           True                 (?,1)
          2. m5(A)       -> c2(m3(A),m0(A)) [A >= 1]             (?,1)
          3. m2(A)       -> m5(A)           [A >= 1]             (?,1)
          4. m6(A)       -> m0(B)           [A >= 2*B && A >= 1] (?,1)
          5. m1(A)       -> m6(A)           True                 (?,1)
          6. m1(A)       -> m4(A)           True                 (?,1)
        Signature:
          {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
        Flow Graph:
          [0->{3},1->{5,6},2->{1},3->{2},4->{1},5->{4},6->{}]
        
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (<0,0,A>, A, .= 0) 
          (<1,0,A>, A, .= 0) 
          (<2,0,A>, A, .= 0) 
          (<2,1,A>, A, .= 0) 
          (<3,0,A>, A, .= 0) 
          (<4,0,A>, ?,   .?) 
          (<5,0,A>, A, .= 0) 
          (<6,0,A>, A, .= 0) 
* Step 2: SizeboundsProc WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          0. divByTwo(A) -> m2(A)           [A >= 1]             (1,1)
          1. m0(A)       -> m1(A)           True                 (?,1)
          2. m5(A)       -> c2(m3(A),m0(A)) [A >= 1]             (?,1)
          3. m2(A)       -> m5(A)           [A >= 1]             (?,1)
          4. m6(A)       -> m0(B)           [A >= 2*B && A >= 1] (?,1)
          5. m1(A)       -> m6(A)           True                 (?,1)
          6. m1(A)       -> m4(A)           True                 (?,1)
        Signature:
          {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
        Flow Graph:
          [0->{3},1->{5,6},2->{1},3->{2},4->{1},5->{4},6->{}]
        Sizebounds:
          (<0,0,A>, ?) 
          (<1,0,A>, ?) 
          (<2,0,A>, ?) 
          (<2,1,A>, ?) 
          (<3,0,A>, ?) 
          (<4,0,A>, ?) 
          (<5,0,A>, ?) 
          (<6,0,A>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (<0,0,A>, A) 
          (<1,0,A>, ?) 
          (<2,0,A>, A) 
          (<2,1,A>, A) 
          (<3,0,A>, A) 
          (<4,0,A>, ?) 
          (<5,0,A>, ?) 
          (<6,0,A>, ?) 
* Step 3: ChainProcessor WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          0. divByTwo(A) -> m2(A)           [A >= 1]             (1,1)
          1. m0(A)       -> m1(A)           True                 (?,1)
          2. m5(A)       -> c2(m3(A),m0(A)) [A >= 1]             (?,1)
          3. m2(A)       -> m5(A)           [A >= 1]             (?,1)
          4. m6(A)       -> m0(B)           [A >= 2*B && A >= 1] (?,1)
          5. m1(A)       -> m6(A)           True                 (?,1)
          6. m1(A)       -> m4(A)           True                 (?,1)
        Signature:
          {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
        Flow Graph:
          [0->{3},1->{5,6},2->{1},3->{2},4->{1},5->{4},6->{}]
        Sizebounds:
          (<0,0,A>, A) 
          (<1,0,A>, ?) 
          (<2,0,A>, A) 
          (<2,1,A>, A) 
          (<3,0,A>, A) 
          (<4,0,A>, ?) 
          (<5,0,A>, ?) 
          (<6,0,A>, ?) 
    + Applied Processor:
        ChainProcessor False [0,1,2,3,4,5,6]
    + Details:
        We chained rule 0 to obtain the rules [7] .
* Step 4: UnreachableRules WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          1. m0(A)       -> m1(A)           True                 (?,1)
          2. m5(A)       -> c2(m3(A),m0(A)) [A >= 1]             (?,1)
          3. m2(A)       -> m5(A)           [A >= 1]             (?,1)
          4. m6(A)       -> m0(B)           [A >= 2*B && A >= 1] (?,1)
          5. m1(A)       -> m6(A)           True                 (?,1)
          6. m1(A)       -> m4(A)           True                 (?,1)
          7. divByTwo(A) -> m5(A)           [A >= 1 && A >= 1]   (1,2)
        Signature:
          {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
        Flow Graph:
          [1->{5,6},2->{1},3->{2},4->{1},5->{4},6->{},7->{2}]
        Sizebounds:
          (<1,0,A>, ?) 
          (<2,0,A>, A) 
          (<2,1,A>, A) 
          (<3,0,A>, A) 
          (<4,0,A>, ?) 
          (<5,0,A>, ?) 
          (<6,0,A>, ?) 
          (<7,0,A>, A) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [3]
* Step 5: ChainProcessor WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          1. m0(A)       -> m1(A)           True                 (?,1)
          2. m5(A)       -> c2(m3(A),m0(A)) [A >= 1]             (?,1)
          4. m6(A)       -> m0(B)           [A >= 2*B && A >= 1] (?,1)
          5. m1(A)       -> m6(A)           True                 (?,1)
          6. m1(A)       -> m4(A)           True                 (?,1)
          7. divByTwo(A) -> m5(A)           [A >= 1 && A >= 1]   (1,2)
        Signature:
          {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
        Flow Graph:
          [1->{5,6},2->{1},4->{1},5->{4},6->{},7->{2}]
        Sizebounds:
          (<1,0,A>, ?) 
          (<2,0,A>, A) 
          (<2,1,A>, A) 
          (<4,0,A>, ?) 
          (<5,0,A>, ?) 
          (<6,0,A>, ?) 
          (<7,0,A>, A) 
    + Applied Processor:
        ChainProcessor False [1,2,4,5,6,7]
    + Details:
        We chained rule 1 to obtain the rules [8,9] .
* Step 6: UnreachableRules WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          2. m5(A)       -> c2(m3(A),m0(A)) [A >= 1]             (?,1)
          4. m6(A)       -> m0(B)           [A >= 2*B && A >= 1] (?,1)
          5. m1(A)       -> m6(A)           True                 (?,1)
          6. m1(A)       -> m4(A)           True                 (?,1)
          7. divByTwo(A) -> m5(A)           [A >= 1 && A >= 1]   (1,2)
          8. m0(A)       -> m6(A)           True                 (?,2)
          9. m0(A)       -> m4(A)           True                 (?,2)
        Signature:
          {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
        Flow Graph:
          [2->{8,9},4->{8,9},5->{4},6->{},7->{2},8->{4},9->{}]
        Sizebounds:
          (<2,0,A>, A) 
          (<2,1,A>, A) 
          (<4,0,A>, ?) 
          (<5,0,A>, ?) 
          (<6,0,A>, ?) 
          (<7,0,A>, A) 
          (<8,0,A>, ?) 
          (<9,0,A>, ?) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [5,6]
* Step 7: ChainProcessor WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          2. m5(A)       -> c2(m3(A),m0(A)) [A >= 1]             (?,1)
          4. m6(A)       -> m0(B)           [A >= 2*B && A >= 1] (?,1)
          7. divByTwo(A) -> m5(A)           [A >= 1 && A >= 1]   (1,2)
          8. m0(A)       -> m6(A)           True                 (?,2)
          9. m0(A)       -> m4(A)           True                 (?,2)
        Signature:
          {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
        Flow Graph:
          [2->{8,9},4->{8,9},7->{2},8->{4},9->{}]
        Sizebounds:
          (<2,0,A>, A) 
          (<2,1,A>, A) 
          (<4,0,A>, ?) 
          (<7,0,A>, A) 
          (<8,0,A>, ?) 
          (<9,0,A>, ?) 
    + Applied Processor:
        ChainProcessor False [2,4,7,8,9]
    + Details:
        We chained rule 2 to obtain the rules [10,11] .
* Step 8: ChainProcessor WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          4.  m6(A)       -> m0(B)           [A >= 2*B && A >= 1] (?,1)
          7.  divByTwo(A) -> m5(A)           [A >= 1 && A >= 1]   (1,2)
          8.  m0(A)       -> m6(A)           True                 (?,2)
          9.  m0(A)       -> m4(A)           True                 (?,2)
          10. m5(A)       -> c2(m3(A),m6(A)) [A >= 1]             (?,3)
          11. m5(A)       -> c2(m3(A),m4(A)) [A >= 1]             (?,3)
        Signature:
          {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
        Flow Graph:
          [4->{8,9},7->{10,11},8->{4},9->{},10->{4},11->{}]
        Sizebounds:
          (< 4,0,A>, ?) 
          (< 7,0,A>, A) 
          (< 8,0,A>, ?) 
          (< 9,0,A>, ?) 
          (<10,0,A>, ?) 
          (<11,0,A>, ?) 
    + Applied Processor:
        ChainProcessor False [4,7,8,9,10,11]
    + Details:
        We chained rule 4 to obtain the rules [12,13] .
* Step 9: UnreachableRules WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          7.  divByTwo(A) -> m5(A)           [A >= 1 && A >= 1]   (1,2)
          8.  m0(A)       -> m6(A)           True                 (?,2)
          9.  m0(A)       -> m4(A)           True                 (?,2)
          10. m5(A)       -> c2(m3(A),m6(A)) [A >= 1]             (?,3)
          11. m5(A)       -> c2(m3(A),m4(A)) [A >= 1]             (?,3)
          12. m6(A)       -> m6(B)           [A >= 2*B && A >= 1] (?,3)
          13. m6(A)       -> m4(B)           [A >= 2*B && A >= 1] (?,3)
        Signature:
          {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
        Flow Graph:
          [7->{10,11},8->{12,13},9->{},10->{12,13},11->{},12->{12,13},13->{}]
        Sizebounds:
          (< 7,0,A>, A) 
          (< 8,0,A>, ?) 
          (< 9,0,A>, ?) 
          (<10,0,A>, ?) 
          (<11,0,A>, ?) 
          (<12,0,A>, ?) 
          (<13,0,A>, ?) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [8,9]
* Step 10: LeafRules WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          7.  divByTwo(A) -> m5(A)           [A >= 1 && A >= 1]   (1,2)
          10. m5(A)       -> c2(m3(A),m6(A)) [A >= 1]             (?,3)
          11. m5(A)       -> c2(m3(A),m4(A)) [A >= 1]             (?,3)
          12. m6(A)       -> m6(B)           [A >= 2*B && A >= 1] (?,3)
          13. m6(A)       -> m4(B)           [A >= 2*B && A >= 1] (?,3)
        Signature:
          {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
        Flow Graph:
          [7->{10,11},10->{12,13},11->{},12->{12,13},13->{}]
        Sizebounds:
          (< 7,0,A>, A) 
          (<10,0,A>, ?) 
          (<11,0,A>, ?) 
          (<12,0,A>, ?) 
          (<13,0,A>, ?) 
    + Applied Processor:
        LeafRules
    + Details:
        The following transitions are estimated by its predecessors and are removed [11,13]
* Step 11: LocalSizeboundsProc WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          7.  divByTwo(A) -> m5(A)           [A >= 1 && A >= 1]   (1,2)
          10. m5(A)       -> c2(m3(A),m6(A)) [A >= 1]             (?,3)
          12. m6(A)       -> m6(B)           [A >= 2*B && A >= 1] (?,3)
        Signature:
          {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
        Flow Graph:
          [7->{10},10->{12},12->{12}]
        Sizebounds:
          (< 7,0,A>, A) 
          (<10,0,A>, ?) 
          (<12,0,A>, ?) 
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (< 7,0,A>, A, .= 0) 
          (<10,0,A>, A, .= 0) 
          (<10,1,A>, A, .= 0) 
          (<12,0,A>, ?,   .?) 
* Step 12: SizeboundsProc WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          7.  divByTwo(A) -> m5(A)           [A >= 1 && A >= 1]   (1,2)
          10. m5(A)       -> c2(m3(A),m6(A)) [A >= 1]             (?,3)
          12. m6(A)       -> m6(B)           [A >= 2*B && A >= 1] (?,3)
        Signature:
          {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
        Flow Graph:
          [7->{10},10->{12},12->{12}]
        Sizebounds:
          (< 7,0,A>, ?) 
          (<10,0,A>, ?) 
          (<10,1,A>, ?) 
          (<12,0,A>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (< 7,0,A>, A) 
          (<10,0,A>, A) 
          (<10,1,A>, A) 
          (<12,0,A>, ?) 
* Step 13: LocationConstraintsProc WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          7.  divByTwo(A) -> m5(A)           [A >= 1 && A >= 1]   (1,2)
          10. m5(A)       -> c2(m3(A),m6(A)) [A >= 1]             (?,3)
          12. m6(A)       -> m6(B)           [A >= 2*B && A >= 1] (?,3)
        Signature:
          {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
        Flow Graph:
          [7->{10},10->{12},12->{12}]
        Sizebounds:
          (< 7,0,A>, A) 
          (<10,0,A>, A) 
          (<10,1,A>, A) 
          (<12,0,A>, ?) 
    + Applied Processor:
        LocationConstraintsProc
    + Details:
        We computed the location constraints  7 :  True 10 :  [A >= 1] 12 :  True .
* Step 14: PolyRank WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          7.  divByTwo(A) -> m5(A)           [A >= 1 && A >= 1]   (1,2)
          10. m5(A)       -> c2(m3(A),m6(A)) [A >= 1]             (?,3)
          12. m6(A)       -> m6(B)           [A >= 2*B && A >= 1] (?,3)
        Signature:
          {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
        Flow Graph:
          [7->{10},10->{12},12->{12}]
        Sizebounds:
          (< 7,0,A>, A) 
          (<10,0,A>, A) 
          (<10,1,A>, A) 
          (<12,0,A>, ?) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Constant}
    + Details:
        We apply a polynomial interpretation of shape constant:
          p(divByTwo) = 1
                p(m3) = 0
                p(m5) = 1
                p(m6) = 0
        
        The following rules are strictly oriented:
        [A >= 1] ==>                
           m5(A)   = 1              
                   > 0              
                   = c2(m3(A),m6(A))
        
        
        The following rules are weakly oriented:
          [A >= 1 && A >= 1] ==>      
                 divByTwo(A)   = 1    
                              >= 1    
                               = m5(A)
        
        [A >= 2*B && A >= 1] ==>      
                       m6(A)   = 0    
                              >= 0    
                               = m6(B)
        
        
* Step 15: LoopRecurrenceProcessor WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          7.  divByTwo(A) -> m5(A)           [A >= 1 && A >= 1]   (1,2)
          10. m5(A)       -> c2(m3(A),m6(A)) [A >= 1]             (1,3)
          12. m6(A)       -> m6(B)           [A >= 2*B && A >= 1] (?,3)
        Signature:
          {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
        Flow Graph:
          [7->{10},10->{12},12->{12}]
        Sizebounds:
          (< 7,0,A>, A) 
          (<10,0,A>, A) 
          (<10,1,A>, A) 
          (<12,0,A>, ?) 
    + Applied Processor:
        LoopRecurrenceProcessor [12]
    + Details:
        Applying the recurrence pattern log to the expression A yields the solution log(A)^1*(1) + 0 .
* Step 16: UnsatPaths WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          7.  divByTwo(A) -> m5(A)           [A >= 1 && A >= 1]   (1,2)               
          10. m5(A)       -> c2(m3(A),m6(A)) [A >= 1]             (1,3)               
          12. m6(A)       -> m6(B)           [A >= 2*B && A >= 1] (log(A)^1*(1) + 0,3)
        Signature:
          {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)}
        Flow Graph:
          [7->{10},10->{12},12->{12}]
        Sizebounds:
          (< 7,0,A>, A) 
          (<10,0,A>, A) 
          (<10,1,A>, A) 
          (<12,0,A>, ?) 
    + Applied Processor:
        UnsatPaths
    + Details:
        The problem is already solved.

WORST_CASE(?,O(log(n)))