YES(?,POLY)
* Step 1: FromIts WORST_CASE(?,POLY)
    + Considered Problem:
        Rules:
          0. l0(A,B) -> l1(A,B)          True                  (1,1)
          1. l1(A,B) -> l1(-1 + A,1 + B) [A >= 1]              (?,1)
          2. l1(A,B) -> l2(A,B)          [0 >= A]              (?,1)
          3. l2(A,B) -> l2(A,-1 + B)     [-1*A >= 0 && B >= 1] (?,1)
        Signature:
          {(l0,2);(l1,2);(l2,2)}
        Flow Graph:
          [0->{1,2},1->{1,2},2->{3},3->{3}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 2: AddSinks WORST_CASE(?,POLY)
    + Considered Problem:
        Rules:
          l0(A,B) -> l1(A,B)           True
          l1(A,B) -> l1(-1 + A,1 + B)  [A >= 1]
          l1(A,B) -> l2(A,B)           [0 >= A]
          l2(A,B) -> l2(A,-1 + B)      [-1*A >= 0 && B >= 1]
        Signature:
          {(l0,2);(l1,2);(l2,2)}
        Rule Graph:
          [0->{1,2},1->{1,2},2->{3},3->{3}]
    + Applied Processor:
        AddSinks
    + Details:
        ()
* Step 3: Unfold WORST_CASE(?,POLY)
    + Considered Problem:
        Rules:
          l0(A,B) -> l1(A,B)           True
          l1(A,B) -> l1(-1 + A,1 + B)  [A >= 1]
          l1(A,B) -> l2(A,B)           [0 >= A]
          l2(A,B) -> l2(A,-1 + B)      [-1*A >= 0 && B >= 1]
          l2(A,B) -> exitus616(A,B)    True
        Signature:
          {(exitus616,2);(l0,2);(l1,2);(l2,2)}
        Rule Graph:
          [0->{1,2},1->{1,2},2->{3},3->{3,4}]
    + Applied Processor:
        Unfold
    + Details:
        ()
* Step 4: Decompose WORST_CASE(?,POLY)
    + Considered Problem:
        Rules:
          l0.0(A,B) -> l1.1(A,B)           True
          l0.0(A,B) -> l1.2(A,B)           True
          l1.1(A,B) -> l1.1(-1 + A,1 + B)  [A >= 1]
          l1.1(A,B) -> l1.2(-1 + A,1 + B)  [A >= 1]
          l1.2(A,B) -> l2.3(A,B)           [0 >= A]
          l2.3(A,B) -> l2.3(A,-1 + B)      [-1*A >= 0 && B >= 1]
          l2.3(A,B) -> l2.4(A,-1 + B)      [-1*A >= 0 && B >= 1]
          l2.4(A,B) -> exitus616.5(A,B)    True
        Signature:
          {(exitus616.5,2);(l0.0,2);(l1.1,2);(l1.2,2);(l2.3,2);(l2.4,2)}
        Rule Graph:
          [0->{2,3},1->{4},2->{2,3},3->{4},4->{5,6},5->{5,6},6->{7},7->{}]
    + Applied Processor:
        Decompose Greedy
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5,6,7]
          |
          +- p:[2] c: [2]
          |
          `- p:[5] c: [5]
* Step 5: AbstractSize WORST_CASE(?,POLY)
    + Considered Problem:
        (Rules:
          l0.0(A,B) -> l1.1(A,B)           True
          l0.0(A,B) -> l1.2(A,B)           True
          l1.1(A,B) -> l1.1(-1 + A,1 + B)  [A >= 1]
          l1.1(A,B) -> l1.2(-1 + A,1 + B)  [A >= 1]
          l1.2(A,B) -> l2.3(A,B)           [0 >= A]
          l2.3(A,B) -> l2.3(A,-1 + B)      [-1*A >= 0 && B >= 1]
          l2.3(A,B) -> l2.4(A,-1 + B)      [-1*A >= 0 && B >= 1]
          l2.4(A,B) -> exitus616.5(A,B)    True
        Signature:
          {(exitus616.5,2);(l0.0,2);(l1.1,2);(l1.2,2);(l2.3,2);(l2.4,2)}
        Rule Graph:
          [0->{2,3},1->{4},2->{2,3},3->{4},4->{5,6},5->{5,6},6->{7},7->{}]
        ,We construct a looptree:
          P: [0,1,2,3,4,5,6,7]
          |
          +- p:[2] c: [2]
          |
          `- p:[5] c: [5])
    + Applied Processor:
        AbstractSize Minimize
    + Details:
        ()
* Step 6: AbstractFlow WORST_CASE(?,POLY)
    + Considered Problem:
        Program:
          Domain: [A,B,0.0,0.1]
           l0.0  ~>  l1.1          [A <= A, B <= B]
           l0.0  ~>  l1.2          [A <= A, B <= B]
           l1.1  ~>  l1.1          [A <= A, B <= K + B]
           l1.1  ~>  l1.2          [A <= A, B <= K + B]
           l1.2  ~>  l2.3          [A <= A, B <= B]
           l2.3  ~>  l2.3          [A <= A, B <= B]
           l2.3  ~>  l2.4          [A <= A, B <= B]
           l2.4  ~>  exitus616.5   [A <= A, B <= B]
          + Loop: [0.0 <= K + A]
               l1.1  ~>  l1.1   [A <= A, B <= K + B]
          + Loop: [0.1 <= K + B]
               l2.3  ~>  l2.3   [A <= A, B <= B]
    + Applied Processor:
        AbstractFlow
    + Details:
        ()
* Step 7: Lare WORST_CASE(?,POLY)
    + Considered Problem:
        Program:
          Domain: [tick,huge,K,A,B,0.0,0.1]
           l0.0  ~>  l1.1          []
           l0.0  ~>  l1.2          []
           l1.1  ~>  l1.1          [B ~+> B,K ~+> B]
           l1.1  ~>  l1.2          [B ~+> B,K ~+> B]
           l1.2  ~>  l2.3          []
           l2.3  ~>  l2.3          []
           l2.3  ~>  l2.4          []
           l2.4  ~>  exitus616.5   []
          + Loop: [A ~+> 0.0,K ~+> 0.0]
               l1.1  ~>  l1.1   [B ~+> B,K ~+> B]
          + Loop: [B ~+> 0.1,K ~+> 0.1]
               l2.3  ~>  l2.3   []
    + Applied Processor:
        Lare
    + Details:
         l0.0  ~>  exitus616.5   [A ~+> 0.0
                                 ,A ~+> tick
                                 ,B ~+> B
                                 ,B ~+> 0.1
                                 ,B ~+> tick
                                 ,tick ~+> tick
                                 ,K ~+> B
                                 ,K ~+> 0.0
                                 ,K ~+> 0.1
                                 ,K ~+> tick
                                 ,A ~*> B
                                 ,A ~*> 0.1
                                 ,A ~*> tick
                                 ,K ~*> B
                                 ,K ~*> 0.1
                                 ,K ~*> tick]
        + <l1.1  ~>  l1.1>  [A ~+> 0.0
                            ,A ~+> tick
                            ,B ~+> B
                            ,tick ~+> tick
                            ,K ~+> B
                            ,K ~+> 0.0
                            ,K ~+> tick
                            ,A ~*> B
                            ,K ~*> B]
        + <l2.3  ~>  l2.3>  [B ~+> 0.1,B ~+> tick,tick ~+> tick,K ~+> 0.1,K ~+> tick]

YES(?,POLY)