WORST_CASE(?,O(log(n)))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          0. start(A) -> a(A) [A >= 1]                  (1,1)
          1. start(A) -> a(A) [A >= 2]                  (1,1)
          2. start(A) -> a(A) [A >= 4]                  (1,1)
          3. a(A)     -> a(B) [2*B >= 2 && A = 2*B]     (?,1)
          4. a(A)     -> a(B) [2*B >= 1 && A = 1 + 2*B] (?,1)
        Signature:
          {(a,1);(start,1)}
        Flow Graph:
          [0->{3,4},1->{3,4},2->{3,4},3->{3,4},4->{3,4}]
        
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (<0,0,A>, A, .= 0) 
          (<1,0,A>, A, .= 0) 
          (<2,0,A>, A, .= 0) 
          (<3,0,A>, ?,   .?) 
          (<4,0,A>, ?,   .?) 
* Step 2: SizeboundsProc WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          0. start(A) -> a(A) [A >= 1]                  (1,1)
          1. start(A) -> a(A) [A >= 2]                  (1,1)
          2. start(A) -> a(A) [A >= 4]                  (1,1)
          3. a(A)     -> a(B) [2*B >= 2 && A = 2*B]     (?,1)
          4. a(A)     -> a(B) [2*B >= 1 && A = 1 + 2*B] (?,1)
        Signature:
          {(a,1);(start,1)}
        Flow Graph:
          [0->{3,4},1->{3,4},2->{3,4},3->{3,4},4->{3,4}]
        Sizebounds:
          (<0,0,A>, ?) 
          (<1,0,A>, ?) 
          (<2,0,A>, ?) 
          (<3,0,A>, ?) 
          (<4,0,A>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (<0,0,A>, A) 
          (<1,0,A>, A) 
          (<2,0,A>, A) 
          (<3,0,A>, ?) 
          (<4,0,A>, ?) 
* Step 3: LocationConstraintsProc WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          0. start(A) -> a(A) [A >= 1]                  (1,1)
          1. start(A) -> a(A) [A >= 2]                  (1,1)
          2. start(A) -> a(A) [A >= 4]                  (1,1)
          3. a(A)     -> a(B) [2*B >= 2 && A = 2*B]     (?,1)
          4. a(A)     -> a(B) [2*B >= 1 && A = 1 + 2*B] (?,1)
        Signature:
          {(a,1);(start,1)}
        Flow Graph:
          [0->{3,4},1->{3,4},2->{3,4},3->{3,4},4->{3,4}]
        Sizebounds:
          (<0,0,A>, A) 
          (<1,0,A>, A) 
          (<2,0,A>, A) 
          (<3,0,A>, ?) 
          (<4,0,A>, ?) 
    + Applied Processor:
        LocationConstraintsProc
    + Details:
        We computed the location constraints  0 :  True 1 :  True 2 :  True 3 :  [2*B >= 1] 4 :  [2*B >= 1] .
* Step 4: PolyRank WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          0. start(A) -> a(A) [A >= 1]                  (1,1)
          1. start(A) -> a(A) [A >= 2]                  (1,1)
          2. start(A) -> a(A) [A >= 4]                  (1,1)
          3. a(A)     -> a(B) [2*B >= 2 && A = 2*B]     (?,1)
          4. a(A)     -> a(B) [2*B >= 1 && A = 1 + 2*B] (?,1)
        Signature:
          {(a,1);(start,1)}
        Flow Graph:
          [0->{3,4},1->{3,4},2->{3,4},3->{3,4},4->{3,4}]
        Sizebounds:
          (<0,0,A>, A) 
          (<1,0,A>, A) 
          (<2,0,A>, A) 
          (<3,0,A>, ?) 
          (<4,0,A>, ?) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
              p(a) = -1 + 2*x1
          p(start) = 2*x1     
        
        The following rules are strictly oriented:
                         [A >= 4] ==>         
                         start(A)   = 2*A     
                                    > -1 + 2*A
                                    = a(A)    
        
        [2*B >= 1 && A = 1 + 2*B] ==>         
                             a(A)   = -1 + 2*A
                                    > -1 + 2*B
                                    = a(B)    
        
        
        The following rules are weakly oriented:
                     [A >= 1] ==>         
                     start(A)   = 2*A     
                               >= -1 + 2*A
                                = a(A)    
        
                     [A >= 2] ==>         
                     start(A)   = 2*A     
                               >= -1 + 2*A
                                = a(A)    
        
        [2*B >= 2 && A = 2*B] ==>         
                         a(A)   = -1 + 2*A
                               >= -1 + 2*B
                                = a(B)    
        
        
* Step 5: PolyRank WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          0. start(A) -> a(A) [A >= 1]                  (1,1)  
          1. start(A) -> a(A) [A >= 2]                  (1,1)  
          2. start(A) -> a(A) [A >= 4]                  (1,1)  
          3. a(A)     -> a(B) [2*B >= 2 && A = 2*B]     (?,1)  
          4. a(A)     -> a(B) [2*B >= 1 && A = 1 + 2*B] (2*A,1)
        Signature:
          {(a,1);(start,1)}
        Flow Graph:
          [0->{3,4},1->{3,4},2->{3,4},3->{3,4},4->{3,4}]
        Sizebounds:
          (<0,0,A>, A) 
          (<1,0,A>, A) 
          (<2,0,A>, A) 
          (<3,0,A>, ?) 
          (<4,0,A>, ?) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
              p(a) = -3 + 2*x1
          p(start) = -1 + 2*x1
        
        The following rules are strictly oriented:
                         [A >= 1] ==>         
                         start(A)   = -1 + 2*A
                                    > -3 + 2*A
                                    = a(A)    
        
                         [A >= 2] ==>         
                         start(A)   = -1 + 2*A
                                    > -3 + 2*A
                                    = a(A)    
        
                         [A >= 4] ==>         
                         start(A)   = -1 + 2*A
                                    > -3 + 2*A
                                    = a(A)    
        
            [2*B >= 2 && A = 2*B] ==>         
                             a(A)   = -3 + 2*A
                                    > -3 + 2*B
                                    = a(B)    
        
        [2*B >= 1 && A = 1 + 2*B] ==>         
                             a(A)   = -3 + 2*A
                                    > -3 + 2*B
                                    = a(B)    
        
        
        The following rules are weakly oriented:
        
        
* Step 6: CombineProcessor WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          0. start(A) -> a(A) [A >= 1]                  (1,1)      
          1. start(A) -> a(A) [A >= 2]                  (1,1)      
          2. start(A) -> a(A) [A >= 4]                  (1,1)      
          3. a(A)     -> a(B) [2*B >= 2 && A = 2*B]     (1 + 2*A,1)
          4. a(A)     -> a(B) [2*B >= 1 && A = 1 + 2*B] (2*A,1)    
        Signature:
          {(a,1);(start,1)}
        Flow Graph:
          [0->{3,4},1->{3,4},2->{3,4},3->{3,4},4->{3,4}]
        Sizebounds:
          (<0,0,A>, A) 
          (<1,0,A>, A) 
          (<2,0,A>, A) 
          (<3,0,A>, ?) 
          (<4,0,A>, ?) 
    + Applied Processor:
        CombineProcessor [0,1,2,3,4]
    + Details:
        We combined rules [0,1] to obtain the rule 5 .
* Step 7: CombineProcessor WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          2. start(A) -> a(A) [A >= 4]                  (1,1)      
          3. a(A)     -> a(B) [2*B >= 2 && A = 2*B]     (1 + 2*A,1)
          4. a(A)     -> a(B) [2*B >= 1 && A = 1 + 2*B] (2*A,1)    
          5. start(A) -> a(A) [(A >= 2 || A >= 1)]      (2,2)      
        Signature:
          {(a,1);(start,1)}
        Flow Graph:
          [2->{3,4},3->{3,4},4->{3,4},5->{3,4}]
        Sizebounds:
          (<2,0,A>, A) 
          (<3,0,A>, ?) 
          (<4,0,A>, ?) 
          (<5,0,A>, A) 
    + Applied Processor:
        CombineProcessor [2,3,4,5]
    + Details:
        We combined rules [2,5] to obtain the rule 6 .
* Step 8: CombineProcessor WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          3. a(A)     -> a(B) [2*B >= 2 && A = 2*B]          (1 + 2*A,1)
          4. a(A)     -> a(B) [2*B >= 1 && A = 1 + 2*B]      (2*A,1)    
          6. start(A) -> a(A) [(A >= 2 || A >= 1 || A >= 4)] (3,3)      
        Signature:
          {(a,1);(start,1)}
        Flow Graph:
          [3->{3,4},4->{3,4},6->{3,4}]
        Sizebounds:
          (<3,0,A>, ?) 
          (<4,0,A>, ?) 
          (<6,0,A>, A) 
    + Applied Processor:
        CombineProcessor [3,4,6]
    + Details:
        We combined rules [3,4] to obtain the rule 7 .
* Step 9: LoopRecurrenceProcessor WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          6. start(A) -> a(A) [(A >= 2 || A >= 1 || A >= 4)]                                                                             (3,3)      
          7. a(A)     -> a(B) [(2*B >= 1 || 2*B >= 2) && (2*B >= 1 || A = 2*B) && (A = 1 + 2*B || 2*B >= 2) && (A = 1 + 2*B || A = 2*B)] (1 + 4*A,2)
        Signature:
          {(a,1);(start,1)}
        Flow Graph:
          [6->{7},7->{7}]
        Sizebounds:
          (<6,0,A>, A) 
          (<7,0,A>, ?) 
    + Applied Processor:
        LoopRecurrenceProcessor [7]
    + Details:
        Applying the recurrence pattern log to the expression A yields the solution log(A)^1*(1) + 0 .
* Step 10: UnsatPaths WORST_CASE(?,O(log(n)))
    + Considered Problem:
        Rules:
          6. start(A) -> a(A) [(A >= 2 || A >= 1 || A >= 4)]                                                                             (3,3)               
          7. a(A)     -> a(B) [(2*B >= 1 || 2*B >= 2) && (2*B >= 1 || A = 2*B) && (A = 1 + 2*B || 2*B >= 2) && (A = 1 + 2*B || A = 2*B)] (log(A)^1*(3) + 0,2)
        Signature:
          {(a,1);(start,1)}
        Flow Graph:
          [6->{7},7->{7}]
        Sizebounds:
          (<6,0,A>, A) 
          (<7,0,A>, ?) 
    + Applied Processor:
        UnsatPaths
    + Details:
        The problem is already solved.

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