WORST_CASE(?,O(n^1))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. start(A,B,C,D)  -> stop1(A,B,C,D)      [A >= 0 && B >= 0 && C >= 0 && D = 0]                      (?,1)
          1. start(A,B,C,D)  -> cont1(A,B,C,D)      [D >= 1 && A >= 0 && B >= 0 && C >= 0 && D >= 0 && A >= D] (?,1)
          2. cont1(A,B,C,D)  -> stop2(A,B,1,-1 + D) [D >= 1 && B >= 0 && A >= D && C = 0]                      (?,1)
          3. cont1(A,B,C,D)  -> a(A,B,-1 + C,D)     [C >= 1 && D >= 1 && C >= 0 && B >= 0 && A >= D]           (?,1)
          4. a(A,B,C,D)      -> b(A,B,E,-1 + D)     [A >= D && B >= 0 && C >= 0 && D >= 1]                     (?,1)
          5. b(A,B,C,D)      -> start(A,B,C,D)      [C >= 0 && D >= 0 && B >= 0 && A >= 1 + D]                 (?,1)
          6. b(A,B,C,D)      -> stop3(A,B,C,D)      [0 >= 1 + C && D >= 0 && B >= 0 && A >= 1 + D]             (?,1)
          7. start0(A,B,C,D) -> start(A,B,B,A)      [A >= 0 && B >= 0]                                         (1,1)
        Signature:
          {(a,4);(b,4);(cont1,4);(start,4);(start0,4);(stop1,4);(stop2,4);(stop3,4)}
        Flow Graph:
          [0->{},1->{2,3},2->{},3->{4},4->{5,6},5->{0,1},6->{},7->{0,1}]
        
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (<0,0,A>, A, .= 0) (<0,0,B>, B, .= 0) (<0,0,C>,     C, .= 0) (<0,0,D>,         D, .= 0) 
          (<1,0,A>, A, .= 0) (<1,0,B>, B, .= 0) (<1,0,C>,     C, .= 0) (<1,0,D>,         D, .= 0) 
          (<2,0,A>, A, .= 0) (<2,0,B>, B, .= 0) (<2,0,C>,     1, .= 1) (<2,0,D>,     1 + D, .+ 1) 
          (<3,0,A>, A, .= 0) (<3,0,B>, B, .= 0) (<3,0,C>, 1 + C, .+ 1) (<3,0,D>,         D, .= 0) 
          (<4,0,A>, A, .= 0) (<4,0,B>, B, .= 0) (<4,0,C>,     ?,   .?) (<4,0,D>, 1 + A + D, .* 1) 
          (<5,0,A>, A, .= 0) (<5,0,B>, B, .= 0) (<5,0,C>,     C, .= 0) (<5,0,D>,         D, .= 0) 
          (<6,0,A>, A, .= 0) (<6,0,B>, B, .= 0) (<6,0,C>,     C, .= 0) (<6,0,D>,         D, .= 0) 
          (<7,0,A>, A, .= 0) (<7,0,B>, B, .= 0) (<7,0,C>,     B, .= 0) (<7,0,D>,         A, .= 0) 
* Step 2: SizeboundsProc WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. start(A,B,C,D)  -> stop1(A,B,C,D)      [A >= 0 && B >= 0 && C >= 0 && D = 0]                      (?,1)
          1. start(A,B,C,D)  -> cont1(A,B,C,D)      [D >= 1 && A >= 0 && B >= 0 && C >= 0 && D >= 0 && A >= D] (?,1)
          2. cont1(A,B,C,D)  -> stop2(A,B,1,-1 + D) [D >= 1 && B >= 0 && A >= D && C = 0]                      (?,1)
          3. cont1(A,B,C,D)  -> a(A,B,-1 + C,D)     [C >= 1 && D >= 1 && C >= 0 && B >= 0 && A >= D]           (?,1)
          4. a(A,B,C,D)      -> b(A,B,E,-1 + D)     [A >= D && B >= 0 && C >= 0 && D >= 1]                     (?,1)
          5. b(A,B,C,D)      -> start(A,B,C,D)      [C >= 0 && D >= 0 && B >= 0 && A >= 1 + D]                 (?,1)
          6. b(A,B,C,D)      -> stop3(A,B,C,D)      [0 >= 1 + C && D >= 0 && B >= 0 && A >= 1 + D]             (?,1)
          7. start0(A,B,C,D) -> start(A,B,B,A)      [A >= 0 && B >= 0]                                         (1,1)
        Signature:
          {(a,4);(b,4);(cont1,4);(start,4);(start0,4);(stop1,4);(stop2,4);(stop3,4)}
        Flow Graph:
          [0->{},1->{2,3},2->{},3->{4},4->{5,6},5->{0,1},6->{},7->{0,1}]
        Sizebounds:
          (<0,0,A>, ?) (<0,0,B>, ?) (<0,0,C>, ?) (<0,0,D>, ?) 
          (<1,0,A>, ?) (<1,0,B>, ?) (<1,0,C>, ?) (<1,0,D>, ?) 
          (<2,0,A>, ?) (<2,0,B>, ?) (<2,0,C>, ?) (<2,0,D>, ?) 
          (<3,0,A>, ?) (<3,0,B>, ?) (<3,0,C>, ?) (<3,0,D>, ?) 
          (<4,0,A>, ?) (<4,0,B>, ?) (<4,0,C>, ?) (<4,0,D>, ?) 
          (<5,0,A>, ?) (<5,0,B>, ?) (<5,0,C>, ?) (<5,0,D>, ?) 
          (<6,0,A>, ?) (<6,0,B>, ?) (<6,0,C>, ?) (<6,0,D>, ?) 
          (<7,0,A>, ?) (<7,0,B>, ?) (<7,0,C>, ?) (<7,0,D>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, ?) (<0,0,D>,     A) 
          (<1,0,A>, A) (<1,0,B>, B) (<1,0,C>, ?) (<1,0,D>,     A) 
          (<2,0,A>, A) (<2,0,B>, B) (<2,0,C>, 1) (<2,0,D>, 1 + A) 
          (<3,0,A>, A) (<3,0,B>, B) (<3,0,C>, ?) (<3,0,D>,     A) 
          (<4,0,A>, A) (<4,0,B>, B) (<4,0,C>, ?) (<4,0,D>,     A) 
          (<5,0,A>, A) (<5,0,B>, B) (<5,0,C>, ?) (<5,0,D>,     A) 
          (<6,0,A>, A) (<6,0,B>, B) (<6,0,C>, ?) (<6,0,D>,     A) 
          (<7,0,A>, A) (<7,0,B>, B) (<7,0,C>, B) (<7,0,D>,     A) 
* Step 3: LeafRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. start(A,B,C,D)  -> stop1(A,B,C,D)      [A >= 0 && B >= 0 && C >= 0 && D = 0]                      (?,1)
          1. start(A,B,C,D)  -> cont1(A,B,C,D)      [D >= 1 && A >= 0 && B >= 0 && C >= 0 && D >= 0 && A >= D] (?,1)
          2. cont1(A,B,C,D)  -> stop2(A,B,1,-1 + D) [D >= 1 && B >= 0 && A >= D && C = 0]                      (?,1)
          3. cont1(A,B,C,D)  -> a(A,B,-1 + C,D)     [C >= 1 && D >= 1 && C >= 0 && B >= 0 && A >= D]           (?,1)
          4. a(A,B,C,D)      -> b(A,B,E,-1 + D)     [A >= D && B >= 0 && C >= 0 && D >= 1]                     (?,1)
          5. b(A,B,C,D)      -> start(A,B,C,D)      [C >= 0 && D >= 0 && B >= 0 && A >= 1 + D]                 (?,1)
          6. b(A,B,C,D)      -> stop3(A,B,C,D)      [0 >= 1 + C && D >= 0 && B >= 0 && A >= 1 + D]             (?,1)
          7. start0(A,B,C,D) -> start(A,B,B,A)      [A >= 0 && B >= 0]                                         (1,1)
        Signature:
          {(a,4);(b,4);(cont1,4);(start,4);(start0,4);(stop1,4);(stop2,4);(stop3,4)}
        Flow Graph:
          [0->{},1->{2,3},2->{},3->{4},4->{5,6},5->{0,1},6->{},7->{0,1}]
        Sizebounds:
          (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, ?) (<0,0,D>,     A) 
          (<1,0,A>, A) (<1,0,B>, B) (<1,0,C>, ?) (<1,0,D>,     A) 
          (<2,0,A>, A) (<2,0,B>, B) (<2,0,C>, 1) (<2,0,D>, 1 + A) 
          (<3,0,A>, A) (<3,0,B>, B) (<3,0,C>, ?) (<3,0,D>,     A) 
          (<4,0,A>, A) (<4,0,B>, B) (<4,0,C>, ?) (<4,0,D>,     A) 
          (<5,0,A>, A) (<5,0,B>, B) (<5,0,C>, ?) (<5,0,D>,     A) 
          (<6,0,A>, A) (<6,0,B>, B) (<6,0,C>, ?) (<6,0,D>,     A) 
          (<7,0,A>, A) (<7,0,B>, B) (<7,0,C>, B) (<7,0,D>,     A) 
    + Applied Processor:
        LeafRules
    + Details:
        The following transitions are estimated by its predecessors and are removed [0,2,6]
* Step 4: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          1. start(A,B,C,D)  -> cont1(A,B,C,D)  [D >= 1 && A >= 0 && B >= 0 && C >= 0 && D >= 0 && A >= D] (?,1)
          3. cont1(A,B,C,D)  -> a(A,B,-1 + C,D) [C >= 1 && D >= 1 && C >= 0 && B >= 0 && A >= D]           (?,1)
          4. a(A,B,C,D)      -> b(A,B,E,-1 + D) [A >= D && B >= 0 && C >= 0 && D >= 1]                     (?,1)
          5. b(A,B,C,D)      -> start(A,B,C,D)  [C >= 0 && D >= 0 && B >= 0 && A >= 1 + D]                 (?,1)
          7. start0(A,B,C,D) -> start(A,B,B,A)  [A >= 0 && B >= 0]                                         (1,1)
        Signature:
          {(a,4);(b,4);(cont1,4);(start,4);(start0,4);(stop1,4);(stop2,4);(stop3,4)}
        Flow Graph:
          [1->{3},3->{4},4->{5},5->{1},7->{1}]
        Sizebounds:
          (<1,0,A>, A) (<1,0,B>, B) (<1,0,C>, ?) (<1,0,D>, A) 
          (<3,0,A>, A) (<3,0,B>, B) (<3,0,C>, ?) (<3,0,D>, A) 
          (<4,0,A>, A) (<4,0,B>, B) (<4,0,C>, ?) (<4,0,D>, A) 
          (<5,0,A>, A) (<5,0,B>, B) (<5,0,C>, ?) (<5,0,D>, A) 
          (<7,0,A>, A) (<7,0,B>, B) (<7,0,C>, B) (<7,0,D>, A) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
               p(a) = x4    
               p(b) = 1 + x4
           p(cont1) = x4    
           p(start) = x4    
          p(start0) = x1    
        
        The following rules are strictly oriented:
        [C >= 0 && D >= 0 && B >= 0 && A >= 1 + D] ==>               
                                        b(A,B,C,D)   = 1 + D         
                                                     > D             
                                                     = start(A,B,C,D)
        
        
        The following rules are weakly oriented:
        [D >= 1 && A >= 0 && B >= 0 && C >= 0 && D >= 0 && A >= D] ==>                
                                                    start(A,B,C,D)   = D              
                                                                    >= D              
                                                                     = cont1(A,B,C,D) 
        
                  [C >= 1 && D >= 1 && C >= 0 && B >= 0 && A >= D] ==>                
                                                    cont1(A,B,C,D)   = D              
                                                                    >= D              
                                                                     = a(A,B,-1 + C,D)
        
                            [A >= D && B >= 0 && C >= 0 && D >= 1] ==>                
                                                        a(A,B,C,D)   = D              
                                                                    >= D              
                                                                     = b(A,B,E,-1 + D)
        
                                                [A >= 0 && B >= 0] ==>                
                                                   start0(A,B,C,D)   = A              
                                                                    >= A              
                                                                     = start(A,B,B,A) 
        
        
* Step 5: KnowledgePropagation WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          1. start(A,B,C,D)  -> cont1(A,B,C,D)  [D >= 1 && A >= 0 && B >= 0 && C >= 0 && D >= 0 && A >= D] (?,1)
          3. cont1(A,B,C,D)  -> a(A,B,-1 + C,D) [C >= 1 && D >= 1 && C >= 0 && B >= 0 && A >= D]           (?,1)
          4. a(A,B,C,D)      -> b(A,B,E,-1 + D) [A >= D && B >= 0 && C >= 0 && D >= 1]                     (?,1)
          5. b(A,B,C,D)      -> start(A,B,C,D)  [C >= 0 && D >= 0 && B >= 0 && A >= 1 + D]                 (A,1)
          7. start0(A,B,C,D) -> start(A,B,B,A)  [A >= 0 && B >= 0]                                         (1,1)
        Signature:
          {(a,4);(b,4);(cont1,4);(start,4);(start0,4);(stop1,4);(stop2,4);(stop3,4)}
        Flow Graph:
          [1->{3},3->{4},4->{5},5->{1},7->{1}]
        Sizebounds:
          (<1,0,A>, A) (<1,0,B>, B) (<1,0,C>, ?) (<1,0,D>, A) 
          (<3,0,A>, A) (<3,0,B>, B) (<3,0,C>, ?) (<3,0,D>, A) 
          (<4,0,A>, A) (<4,0,B>, B) (<4,0,C>, ?) (<4,0,D>, A) 
          (<5,0,A>, A) (<5,0,B>, B) (<5,0,C>, ?) (<5,0,D>, A) 
          (<7,0,A>, A) (<7,0,B>, B) (<7,0,C>, B) (<7,0,D>, A) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        We propagate bounds from predecessors.
* Step 6: LocalSizeboundsProc WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          1. start(A,B,C,D)  -> cont1(A,B,C,D)  [D >= 1 && A >= 0 && B >= 0 && C >= 0 && D >= 0 && A >= D] (1 + A,1)
          3. cont1(A,B,C,D)  -> a(A,B,-1 + C,D) [C >= 1 && D >= 1 && C >= 0 && B >= 0 && A >= D]           (1 + A,1)
          4. a(A,B,C,D)      -> b(A,B,E,-1 + D) [A >= D && B >= 0 && C >= 0 && D >= 1]                     (1 + A,1)
          5. b(A,B,C,D)      -> start(A,B,C,D)  [C >= 0 && D >= 0 && B >= 0 && A >= 1 + D]                 (A,1)    
          7. start0(A,B,C,D) -> start(A,B,B,A)  [A >= 0 && B >= 0]                                         (1,1)    
        Signature:
          {(a,4);(b,4);(cont1,4);(start,4);(start0,4);(stop1,4);(stop2,4);(stop3,4)}
        Flow Graph:
          [1->{3},3->{4},4->{5},5->{1},7->{1}]
        Sizebounds:
          (<1,0,A>, A) (<1,0,B>, B) (<1,0,C>, ?) (<1,0,D>, A) 
          (<3,0,A>, A) (<3,0,B>, B) (<3,0,C>, ?) (<3,0,D>, A) 
          (<4,0,A>, A) (<4,0,B>, B) (<4,0,C>, ?) (<4,0,D>, A) 
          (<5,0,A>, A) (<5,0,B>, B) (<5,0,C>, ?) (<5,0,D>, A) 
          (<7,0,A>, A) (<7,0,B>, B) (<7,0,C>, B) (<7,0,D>, A) 
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        The problem is already solved.

WORST_CASE(?,O(n^1))