YES(?,O(1))
* Step 1: FromIts WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0. start(A,B,C,D)  -> lbl41(E,B,C,D) [C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A = B && C = D] (?,1)
          1. lbl41(A,B,C,D)  -> stop(A,B,A,D)  [C + -1*D >= 0 && -1*C + D >= 0 && C = D]                                            (?,1)
          2. start0(A,B,C,D) -> start(B,B,D,D) True                                                                                 (1,1)
        Signature:
          {(lbl41,4);(start,4);(start0,4);(stop,4)}
        Flow Graph:
          [0->{1},1->{},2->{0}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 2: AddSinks WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          start(A,B,C,D)  -> lbl41(E,B,C,D)  [C + -1*D >= 0
                                              && -1*C + D >= 0
                                              && A + -1*B >= 0
                                              && -1*A + B >= 0
                                              && A = B
                                              && C = D]
          lbl41(A,B,C,D)  -> stop(A,B,A,D)   [C + -1*D >= 0 && -1*C + D >= 0 && C = D]
          start0(A,B,C,D) -> start(B,B,D,D)  True
        Signature:
          {(lbl41,4);(start,4);(start0,4);(stop,4)}
        Rule Graph:
          [0->{1},1->{},2->{0}]
    + Applied Processor:
        AddSinks
    + Details:
        ()
* Step 3: Decompose WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          start(A,B,C,D)  -> lbl41(E,B,C,D)      [C + -1*D >= 0
                                                  && -1*C + D >= 0
                                                  && A + -1*B >= 0
                                                  && -1*A + B >= 0
                                                  && A = B
                                                  && C = D]
          lbl41(A,B,C,D)  -> stop(A,B,A,D)       [C + -1*D >= 0 && -1*C + D >= 0 && C = D]
          start0(A,B,C,D) -> start(B,B,D,D)      True
          stop(A,B,C,D)   -> exitus616(A,B,C,D)  True
        Signature:
          {(exitus616,4);(lbl41,4);(start,4);(start0,4);(stop,4)}
        Rule Graph:
          [0->{1},1->{3},2->{0}]
    + Applied Processor:
        Decompose Greedy
    + Details:
        We construct a looptree:
          P: [0,1,2,3]
* Step 4: AbstractSize WORST_CASE(?,O(1))
    + Considered Problem:
        (Rules:
          start(A,B,C,D)  -> lbl41(E,B,C,D)      [C + -1*D >= 0
                                                  && -1*C + D >= 0
                                                  && A + -1*B >= 0
                                                  && -1*A + B >= 0
                                                  && A = B
                                                  && C = D]
          lbl41(A,B,C,D)  -> stop(A,B,A,D)       [C + -1*D >= 0 && -1*C + D >= 0 && C = D]
          start0(A,B,C,D) -> start(B,B,D,D)      True
          stop(A,B,C,D)   -> exitus616(A,B,C,D)  True
        Signature:
          {(exitus616,4);(lbl41,4);(start,4);(start0,4);(stop,4)}
        Rule Graph:
          [0->{1},1->{3},2->{0}]
        ,We construct a looptree:
          P: [0,1,2,3])
    + Applied Processor:
        AbstractSize Minimize
    + Details:
        ()
* Step 5: AbstractFlow WORST_CASE(?,O(1))
    + Considered Problem:
        Program:
          Domain: [A,B,C,D]
           start   ~>  lbl41       [A <= unknown, B <= B, C <= C, D <= D]
           lbl41   ~>  stop        [A <= A, B <= B, C <= A, D <= D]
           start0  ~>  start       [A <= B, B <= B, C <= D, D <= D]
           stop    ~>  exitus616   [A <= A, B <= B, C <= C, D <= D]
    + Applied Processor:
        AbstractFlow
    + Details:
        ()
* Step 6: Lare WORST_CASE(?,O(1))
    + Considered Problem:
        Program:
          Domain: [tick,huge,K,A,B,C,D]
           start   ~>  lbl41       [huge ~=> A]
           lbl41   ~>  stop        [A ~=> C]
           start0  ~>  start       [B ~=> A,D ~=> C]
           stop    ~>  exitus616   []
    + Applied Processor:
        Lare
    + Details:
         start0  ~>  exitus616   [huge ~=> A,huge ~=> C]

YES(?,O(1))