WORST_CASE(?,O(1))
* Step 1: LocalSizeboundsProc WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0. evalndloopstart(A)    -> evalndloopentryin(A)  True                                 (1,1)
          1. evalndloopentryin(A)  -> evalndloopbbin(0)     True                                 (?,1)
          2. evalndloopbbin(A)     -> evalndloopbbin(B)     [2 + A >= B && B >= 1 + A && 9 >= B] (?,1)
          3. evalndloopbbin(A)     -> evalndloopreturnin(A) [B >= 3 + A]                         (?,1)
          4. evalndloopbbin(A)     -> evalndloopreturnin(A) [A >= B]                             (?,1)
          5. evalndloopbbin(A)     -> evalndloopreturnin(A) [B >= 10]                            (?,1)
          6. evalndloopreturnin(A) -> evalndloopstop(A)     True                                 (?,1)
        Signature:
          {(evalndloopbbin,1);(evalndloopentryin,1);(evalndloopreturnin,1);(evalndloopstart,1);(evalndloopstop,1)}
        Flow Graph:
          [0->{1},1->{2,3,4,5},2->{2,3,4,5},3->{6},4->{6},5->{6},6->{}]
        
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (<0,0,A>,     A, .= 0) 
          (<1,0,A>,     0, .= 0) 
          (<2,0,A>, 9 + A, .+ 9) 
          (<3,0,A>,     A, .= 0) 
          (<4,0,A>,     A, .= 0) 
          (<5,0,A>,     A, .= 0) 
          (<6,0,A>,     A, .= 0) 
* Step 2: SizeboundsProc WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0. evalndloopstart(A)    -> evalndloopentryin(A)  True                                 (1,1)
          1. evalndloopentryin(A)  -> evalndloopbbin(0)     True                                 (?,1)
          2. evalndloopbbin(A)     -> evalndloopbbin(B)     [2 + A >= B && B >= 1 + A && 9 >= B] (?,1)
          3. evalndloopbbin(A)     -> evalndloopreturnin(A) [B >= 3 + A]                         (?,1)
          4. evalndloopbbin(A)     -> evalndloopreturnin(A) [A >= B]                             (?,1)
          5. evalndloopbbin(A)     -> evalndloopreturnin(A) [B >= 10]                            (?,1)
          6. evalndloopreturnin(A) -> evalndloopstop(A)     True                                 (?,1)
        Signature:
          {(evalndloopbbin,1);(evalndloopentryin,1);(evalndloopreturnin,1);(evalndloopstart,1);(evalndloopstop,1)}
        Flow Graph:
          [0->{1},1->{2,3,4,5},2->{2,3,4,5},3->{6},4->{6},5->{6},6->{}]
        Sizebounds:
          (<0,0,A>, ?) 
          (<1,0,A>, ?) 
          (<2,0,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>, 0) 
          (<2,0,A>, 1) 
          (<3,0,A>, 1) 
          (<4,0,A>, 1) 
          (<5,0,A>, 1) 
          (<6,0,A>, 1) 
* Step 3: LeafRules WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0. evalndloopstart(A)    -> evalndloopentryin(A)  True                                 (1,1)
          1. evalndloopentryin(A)  -> evalndloopbbin(0)     True                                 (?,1)
          2. evalndloopbbin(A)     -> evalndloopbbin(B)     [2 + A >= B && B >= 1 + A && 9 >= B] (?,1)
          3. evalndloopbbin(A)     -> evalndloopreturnin(A) [B >= 3 + A]                         (?,1)
          4. evalndloopbbin(A)     -> evalndloopreturnin(A) [A >= B]                             (?,1)
          5. evalndloopbbin(A)     -> evalndloopreturnin(A) [B >= 10]                            (?,1)
          6. evalndloopreturnin(A) -> evalndloopstop(A)     True                                 (?,1)
        Signature:
          {(evalndloopbbin,1);(evalndloopentryin,1);(evalndloopreturnin,1);(evalndloopstart,1);(evalndloopstop,1)}
        Flow Graph:
          [0->{1},1->{2,3,4,5},2->{2,3,4,5},3->{6},4->{6},5->{6},6->{}]
        Sizebounds:
          (<0,0,A>, A) 
          (<1,0,A>, 0) 
          (<2,0,A>, 1) 
          (<3,0,A>, 1) 
          (<4,0,A>, 1) 
          (<5,0,A>, 1) 
          (<6,0,A>, 1) 
    + Applied Processor:
        LeafRules
    + Details:
        The following transitions are estimated by its predecessors and are removed [3,4,5,6]
* Step 4: PolyRank WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0. evalndloopstart(A)   -> evalndloopentryin(A) True                                 (1,1)
          1. evalndloopentryin(A) -> evalndloopbbin(0)    True                                 (?,1)
          2. evalndloopbbin(A)    -> evalndloopbbin(B)    [2 + A >= B && B >= 1 + A && 9 >= B] (?,1)
        Signature:
          {(evalndloopbbin,1);(evalndloopentryin,1);(evalndloopreturnin,1);(evalndloopstart,1);(evalndloopstop,1)}
        Flow Graph:
          [0->{1},1->{2},2->{2}]
        Sizebounds:
          (<0,0,A>, A) 
          (<1,0,A>, 0) 
          (<2,0,A>, 1) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
             p(evalndloopbbin) = 9 + -1*x1
          p(evalndloopentryin) = 9        
            p(evalndloopstart) = 9        
        
        The following rules are strictly oriented:
        [2 + A >= B && B >= 1 + A && 9 >= B] ==>                  
                           evalndloopbbin(A)   = 9 + -1*A         
                                               > 9 + -1*B         
                                               = evalndloopbbin(B)
        
        
        The following rules are weakly oriented:
                          True ==>                     
            evalndloopstart(A)   = 9                   
                                >= 9                   
                                 = evalndloopentryin(A)
        
                          True ==>                     
          evalndloopentryin(A)   = 9                   
                                >= 9                   
                                 = evalndloopbbin(0)   
        
        
* Step 5: KnowledgePropagation WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0. evalndloopstart(A)   -> evalndloopentryin(A) True                                 (1,1)
          1. evalndloopentryin(A) -> evalndloopbbin(0)    True                                 (?,1)
          2. evalndloopbbin(A)    -> evalndloopbbin(B)    [2 + A >= B && B >= 1 + A && 9 >= B] (9,1)
        Signature:
          {(evalndloopbbin,1);(evalndloopentryin,1);(evalndloopreturnin,1);(evalndloopstart,1);(evalndloopstop,1)}
        Flow Graph:
          [0->{1},1->{2},2->{2}]
        Sizebounds:
          (<0,0,A>, A) 
          (<1,0,A>, 0) 
          (<2,0,A>, 1) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        We propagate bounds from predecessors.
* Step 6: LocalSizeboundsProc WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0. evalndloopstart(A)   -> evalndloopentryin(A) True                                 (1,1)
          1. evalndloopentryin(A) -> evalndloopbbin(0)    True                                 (1,1)
          2. evalndloopbbin(A)    -> evalndloopbbin(B)    [2 + A >= B && B >= 1 + A && 9 >= B] (9,1)
        Signature:
          {(evalndloopbbin,1);(evalndloopentryin,1);(evalndloopreturnin,1);(evalndloopstart,1);(evalndloopstop,1)}
        Flow Graph:
          [0->{1},1->{2},2->{2}]
        Sizebounds:
          (<0,0,A>, A) 
          (<1,0,A>, 0) 
          (<2,0,A>, 1) 
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        The problem is already solved.

WORST_CASE(?,O(1))