YES(?,O(n^1))
* Step 1: UnsatPaths WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. start(A,B) -> eval(A,B)     True                   (1,1)
          1. eval(A,B)  -> eval(1 + A,B) [B >= 1 + A && B >= A] (?,1)
          2. eval(A,B)  -> eval(A,1 + B) [A >= 1 + B]           (?,1)
        Signature:
          {(eval,2);(start,2)}
        Flow Graph:
          [0->{1,2},1->{1,2},2->{1,2}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(1,2),(2,1)]
* Step 2: FromIts WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. start(A,B) -> eval(A,B)     True                   (1,1)
          1. eval(A,B)  -> eval(1 + A,B) [B >= 1 + A && B >= A] (?,1)
          2. eval(A,B)  -> eval(A,1 + B) [A >= 1 + B]           (?,1)
        Signature:
          {(eval,2);(start,2)}
        Flow Graph:
          [0->{1,2},1->{1},2->{2}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 3: AddSinks WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          start(A,B) -> eval(A,B)      True
          eval(A,B)  -> eval(1 + A,B)  [B >= 1 + A && B >= A]
          eval(A,B)  -> eval(A,1 + B)  [A >= 1 + B]
        Signature:
          {(eval,2);(start,2)}
        Rule Graph:
          [0->{1,2},1->{1},2->{2}]
    + Applied Processor:
        AddSinks
    + Details:
        ()
* Step 4: Unfold WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          start(A,B) -> eval(A,B)       True
          eval(A,B)  -> eval(1 + A,B)   [B >= 1 + A && B >= A]
          eval(A,B)  -> eval(A,1 + B)   [A >= 1 + B]
          eval(A,B)  -> exitus616(A,B)  True
          eval(A,B)  -> exitus616(A,B)  True
        Signature:
          {(eval,2);(exitus616,2);(start,2)}
        Rule Graph:
          [0->{1,2},1->{1,4},2->{2,3}]
    + Applied Processor:
        Unfold
    + Details:
        ()
* Step 5: Decompose WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          start.0(A,B) -> eval.1(A,B)       True
          start.0(A,B) -> eval.2(A,B)       True
          eval.1(A,B)  -> eval.1(1 + A,B)   [B >= 1 + A && B >= A]
          eval.1(A,B)  -> eval.4(1 + A,B)   [B >= 1 + A && B >= A]
          eval.2(A,B)  -> eval.2(A,1 + B)   [A >= 1 + B]
          eval.2(A,B)  -> eval.3(A,1 + B)   [A >= 1 + B]
          eval.3(A,B)  -> exitus616.5(A,B)  True
          eval.4(A,B)  -> exitus616.5(A,B)  True
        Signature:
          {(eval.1,2);(eval.2,2);(eval.3,2);(eval.4,2);(exitus616.5,2);(start.0,2)}
        Rule Graph:
          [0->{2,3},1->{4,5},2->{2,3},3->{7},4->{4,5},5->{6},6->{},7->{}]
    + Applied Processor:
        Decompose Greedy
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5,6,7]
          |
          +- p:[4] c: [4]
          |
          `- p:[2] c: [2]
* Step 6: AbstractSize WORST_CASE(?,O(n^1))
    + Considered Problem:
        (Rules:
          start.0(A,B) -> eval.1(A,B)       True
          start.0(A,B) -> eval.2(A,B)       True
          eval.1(A,B)  -> eval.1(1 + A,B)   [B >= 1 + A && B >= A]
          eval.1(A,B)  -> eval.4(1 + A,B)   [B >= 1 + A && B >= A]
          eval.2(A,B)  -> eval.2(A,1 + B)   [A >= 1 + B]
          eval.2(A,B)  -> eval.3(A,1 + B)   [A >= 1 + B]
          eval.3(A,B)  -> exitus616.5(A,B)  True
          eval.4(A,B)  -> exitus616.5(A,B)  True
        Signature:
          {(eval.1,2);(eval.2,2);(eval.3,2);(eval.4,2);(exitus616.5,2);(start.0,2)}
        Rule Graph:
          [0->{2,3},1->{4,5},2->{2,3},3->{7},4->{4,5},5->{6},6->{},7->{}]
        ,We construct a looptree:
          P: [0,1,2,3,4,5,6,7]
          |
          +- p:[4] c: [4]
          |
          `- p:[2] c: [2])
    + Applied Processor:
        AbstractSize Minimize
    + Details:
        ()
* Step 7: AbstractFlow WORST_CASE(?,O(n^1))
    + Considered Problem:
        Program:
          Domain: [A,B,0.0,0.1]
           start.0  ~>  eval.1        [A <= A, B <= B]
           start.0  ~>  eval.2        [A <= A, B <= B]
           eval.1   ~>  eval.1        [A <= A + B, B <= B]
           eval.1   ~>  eval.4        [A <= A + B, B <= B]
           eval.2   ~>  eval.2        [A <= A, B <= A + B]
           eval.2   ~>  eval.3        [A <= A, B <= A + B]
           eval.3   ~>  exitus616.5   [A <= A, B <= B]
           eval.4   ~>  exitus616.5   [A <= A, B <= B]
          + Loop: [0.0 <= K + A + B]
               eval.2  ~>  eval.2   [A <= A, B <= A + B]
          + Loop: [0.1 <= A + B]
               eval.1  ~>  eval.1   [A <= A + B, B <= B]
    + Applied Processor:
        AbstractFlow
    + Details:
        ()
* Step 8: Lare WORST_CASE(?,O(n^1))
    + Considered Problem:
        Program:
          Domain: [tick,huge,K,A,B,0.0,0.1]
           start.0  ~>  eval.1        []
           start.0  ~>  eval.2        []
           eval.1   ~>  eval.1        [A ~+> A,B ~+> A]
           eval.1   ~>  eval.4        [A ~+> A,B ~+> A]
           eval.2   ~>  eval.2        [A ~+> B,B ~+> B]
           eval.2   ~>  eval.3        [A ~+> B,B ~+> B]
           eval.3   ~>  exitus616.5   []
           eval.4   ~>  exitus616.5   []
          + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0]
               eval.2  ~>  eval.2   [A ~+> B,B ~+> B]
          + Loop: [A ~+> 0.1,B ~+> 0.1]
               eval.1  ~>  eval.1   [A ~+> A,B ~+> A]
    + Applied Processor:
        Lare
    + Details:
         start.0  ~>  exitus616.5   [A ~+> A
                                    ,A ~+> B
                                    ,A ~+> 0.0
                                    ,A ~+> 0.1
                                    ,A ~+> tick
                                    ,B ~+> A
                                    ,B ~+> B
                                    ,B ~+> 0.0
                                    ,B ~+> 0.1
                                    ,B ~+> tick
                                    ,tick ~+> tick
                                    ,K ~+> 0.0
                                    ,K ~+> tick
                                    ,A ~*> A
                                    ,A ~*> B
                                    ,B ~*> A
                                    ,B ~*> B
                                    ,K ~*> B]
        + <eval.2  ~>  eval.2>  [A ~+> B
                                ,A ~+> 0.0
                                ,A ~+> tick
                                ,B ~+> B
                                ,B ~+> 0.0
                                ,B ~+> tick
                                ,tick ~+> tick
                                ,K ~+> 0.0
                                ,K ~+> tick
                                ,A ~*> B
                                ,B ~*> B
                                ,K ~*> B]
        + <eval.1  ~>  eval.1>  [A ~+> A
                                ,A ~+> 0.1
                                ,A ~+> tick
                                ,B ~+> A
                                ,B ~+> 0.1
                                ,B ~+> tick
                                ,tick ~+> tick
                                ,A ~*> A
                                ,B ~*> A]

YES(?,O(n^1))