YES(?,POLY) * Step 1: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalrealbubblestart(A,B,C,D) -> evalrealbubbleentryin(A,B,C,D) True (1,1) 1. evalrealbubbleentryin(A,B,C,D) -> evalrealbubblebb7in(-1 + A,B,C,D) True (?,1) 2. evalrealbubblebb7in(A,B,C,D) -> evalrealbubblebb4in(A,0,0,D) [A >= 1] (?,1) 3. evalrealbubblebb7in(A,B,C,D) -> evalrealbubblereturnin(A,B,C,D) [0 >= A] (?,1) 4. evalrealbubblebb4in(A,B,C,D) -> evalrealbubblebb1in(A,B,C,D) [B + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && A >= 1 + B] 5. evalrealbubblebb4in(A,B,C,D) -> evalrealbubblebb5in(A,B,C,D) [B + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && B >= A] 6. evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb2in(A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && E >= 1 + F] 7. evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && F >= E] 8. evalrealbubblebb2in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,1) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] 9. evalrealbubblebb3in(A,B,C,D) -> evalrealbubblebb4in(A,1 + B,D,D) [1 + C + -1*D >= 0 (?,1) && 1 + B + -1*D >= 0 && A + -1*D >= 0 && D >= 0 && C + D >= 0 && B + D >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] 10. evalrealbubblebb5in(A,B,C,D) -> evalrealbubblereturnin(A,B,C,D) [B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && C = 0] 11. evalrealbubblebb5in(A,B,C,D) -> evalrealbubblebb6in(A,B,C,D) [B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && C >= 1] 12. evalrealbubblebb6in(A,B,C,D) -> evalrealbubblebb7in(-1 + A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0] 13. evalrealbubblereturnin(A,B,C,D) -> evalrealbubblestop(A,B,C,D) True (?,1) Signature: {(evalrealbubblebb1in,4) ;(evalrealbubblebb2in,4) ;(evalrealbubblebb3in,4) ;(evalrealbubblebb4in,4) ;(evalrealbubblebb5in,4) ;(evalrealbubblebb6in,4) ;(evalrealbubblebb7in,4) ;(evalrealbubbleentryin,4) ;(evalrealbubblereturnin,4) ;(evalrealbubblestart,4) ;(evalrealbubblestop,4)} Flow Graph: [0->{1},1->{2,3},2->{4,5},3->{13},4->{6,7},5->{10,11},6->{8},7->{9},8->{9},9->{4,5},10->{13},11->{12} ,12->{2,3},13->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,5)] * Step 2: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalrealbubblestart(A,B,C,D) -> evalrealbubbleentryin(A,B,C,D) True (1,1) 1. evalrealbubbleentryin(A,B,C,D) -> evalrealbubblebb7in(-1 + A,B,C,D) True (?,1) 2. evalrealbubblebb7in(A,B,C,D) -> evalrealbubblebb4in(A,0,0,D) [A >= 1] (?,1) 3. evalrealbubblebb7in(A,B,C,D) -> evalrealbubblereturnin(A,B,C,D) [0 >= A] (?,1) 4. evalrealbubblebb4in(A,B,C,D) -> evalrealbubblebb1in(A,B,C,D) [B + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && A >= 1 + B] 5. evalrealbubblebb4in(A,B,C,D) -> evalrealbubblebb5in(A,B,C,D) [B + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && B >= A] 6. evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb2in(A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && E >= 1 + F] 7. evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,C) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && F >= E] 8. evalrealbubblebb2in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,1) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] 9. evalrealbubblebb3in(A,B,C,D) -> evalrealbubblebb4in(A,1 + B,D,D) [1 + C + -1*D >= 0 (?,1) && 1 + B + -1*D >= 0 && A + -1*D >= 0 && D >= 0 && C + D >= 0 && B + D >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] 10. evalrealbubblebb5in(A,B,C,D) -> evalrealbubblereturnin(A,B,C,D) [B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && C = 0] 11. evalrealbubblebb5in(A,B,C,D) -> evalrealbubblebb6in(A,B,C,D) [B + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && C >= 1] 12. evalrealbubblebb6in(A,B,C,D) -> evalrealbubblebb7in(-1 + A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0] 13. evalrealbubblereturnin(A,B,C,D) -> evalrealbubblestop(A,B,C,D) True (?,1) Signature: {(evalrealbubblebb1in,4) ;(evalrealbubblebb2in,4) ;(evalrealbubblebb3in,4) ;(evalrealbubblebb4in,4) ;(evalrealbubblebb5in,4) ;(evalrealbubblebb6in,4) ;(evalrealbubblebb7in,4) ;(evalrealbubbleentryin,4) ;(evalrealbubblereturnin,4) ;(evalrealbubblestart,4) ;(evalrealbubblestop,4)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{13},4->{6,7},5->{10,11},6->{8},7->{9},8->{9},9->{4,5},10->{13},11->{12},12->{2 ,3},13->{}] + Applied Processor: FromIts + Details: () * Step 3: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: evalrealbubblestart(A,B,C,D) -> evalrealbubbleentryin(A,B,C,D) True evalrealbubbleentryin(A,B,C,D) -> evalrealbubblebb7in(-1 + A,B,C,D) True evalrealbubblebb7in(A,B,C,D) -> evalrealbubblebb4in(A,0,0,D) [A >= 1] evalrealbubblebb7in(A,B,C,D) -> evalrealbubblereturnin(A,B,C,D) [0 >= A] evalrealbubblebb4in(A,B,C,D) -> evalrealbubblebb1in(A,B,C,D) [B + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && A >= 1 + B] evalrealbubblebb4in(A,B,C,D) -> evalrealbubblebb5in(A,B,C,D) [B + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && B >= A] evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb2in(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && E >= 1 + F] evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,C) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && F >= E] evalrealbubblebb2in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,1) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] evalrealbubblebb3in(A,B,C,D) -> evalrealbubblebb4in(A,1 + B,D,D) [1 + C + -1*D >= 0 && 1 + B + -1*D >= 0 && A + -1*D >= 0 && D >= 0 && C + D >= 0 && B + D >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] evalrealbubblebb5in(A,B,C,D) -> evalrealbubblereturnin(A,B,C,D) [B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && C = 0] evalrealbubblebb5in(A,B,C,D) -> evalrealbubblebb6in(A,B,C,D) [B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && C >= 1] evalrealbubblebb6in(A,B,C,D) -> evalrealbubblebb7in(-1 + A,B,C,D) [B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0] evalrealbubblereturnin(A,B,C,D) -> evalrealbubblestop(A,B,C,D) True Signature: {(evalrealbubblebb1in,4) ;(evalrealbubblebb2in,4) ;(evalrealbubblebb3in,4) ;(evalrealbubblebb4in,4) ;(evalrealbubblebb5in,4) ;(evalrealbubblebb6in,4) ;(evalrealbubblebb7in,4) ;(evalrealbubbleentryin,4) ;(evalrealbubblereturnin,4) ;(evalrealbubblestart,4) ;(evalrealbubblestop,4)} Rule Graph: [0->{1},1->{2,3},2->{4},3->{13},4->{6,7},5->{10,11},6->{8},7->{9},8->{9},9->{4,5},10->{13},11->{12},12->{2 ,3},13->{}] + Applied Processor: AddSinks + Details: () * Step 4: Unfold WORST_CASE(?,POLY) + Considered Problem: Rules: evalrealbubblestart(A,B,C,D) -> evalrealbubbleentryin(A,B,C,D) True evalrealbubbleentryin(A,B,C,D) -> evalrealbubblebb7in(-1 + A,B,C,D) True evalrealbubblebb7in(A,B,C,D) -> evalrealbubblebb4in(A,0,0,D) [A >= 1] evalrealbubblebb7in(A,B,C,D) -> evalrealbubblereturnin(A,B,C,D) [0 >= A] evalrealbubblebb4in(A,B,C,D) -> evalrealbubblebb1in(A,B,C,D) [B + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && A >= 1 + B] evalrealbubblebb4in(A,B,C,D) -> evalrealbubblebb5in(A,B,C,D) [B + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && B >= A] evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb2in(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && E >= 1 + F] evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,C) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && F >= E] evalrealbubblebb2in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,1) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] evalrealbubblebb3in(A,B,C,D) -> evalrealbubblebb4in(A,1 + B,D,D) [1 + C + -1*D >= 0 && 1 + B + -1*D >= 0 && A + -1*D >= 0 && D >= 0 && C + D >= 0 && B + D >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] evalrealbubblebb5in(A,B,C,D) -> evalrealbubblereturnin(A,B,C,D) [B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && C = 0] evalrealbubblebb5in(A,B,C,D) -> evalrealbubblebb6in(A,B,C,D) [B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && C >= 1] evalrealbubblebb6in(A,B,C,D) -> evalrealbubblebb7in(-1 + A,B,C,D) [B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0] evalrealbubblereturnin(A,B,C,D) -> evalrealbubblestop(A,B,C,D) True evalrealbubblestop(A,B,C,D) -> exitus616(A,B,C,D) True evalrealbubblestop(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(evalrealbubblebb1in,4) ;(evalrealbubblebb2in,4) ;(evalrealbubblebb3in,4) ;(evalrealbubblebb4in,4) ;(evalrealbubblebb5in,4) ;(evalrealbubblebb6in,4) ;(evalrealbubblebb7in,4) ;(evalrealbubbleentryin,4) ;(evalrealbubblereturnin,4) ;(evalrealbubblestart,4) ;(evalrealbubblestop,4) ;(exitus616,4)} Rule Graph: [0->{1},1->{2,3},2->{4},3->{13},4->{6,7},5->{10,11},6->{8},7->{9},8->{9},9->{4,5},10->{13},11->{12},12->{2 ,3},13->{14,15}] + Applied Processor: Unfold + Details: () * Step 5: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: evalrealbubblestart.0(A,B,C,D) -> evalrealbubbleentryin.1(A,B,C,D) True evalrealbubbleentryin.1(A,B,C,D) -> evalrealbubblebb7in.2(-1 + A,B,C,D) True evalrealbubbleentryin.1(A,B,C,D) -> evalrealbubblebb7in.3(-1 + A,B,C,D) True evalrealbubblebb7in.2(A,B,C,D) -> evalrealbubblebb4in.4(A,0,0,D) [A >= 1] evalrealbubblebb7in.3(A,B,C,D) -> evalrealbubblereturnin.13(A,B,C,D) [0 >= A] evalrealbubblebb4in.4(A,B,C,D) -> evalrealbubblebb1in.6(A,B,C,D) [B + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && A >= 1 + B] evalrealbubblebb4in.4(A,B,C,D) -> evalrealbubblebb1in.7(A,B,C,D) [B + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && A >= 1 + B] evalrealbubblebb4in.5(A,B,C,D) -> evalrealbubblebb5in.10(A,B,C,D) [B + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && B >= A] evalrealbubblebb4in.5(A,B,C,D) -> evalrealbubblebb5in.11(A,B,C,D) [B + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && B >= A] evalrealbubblebb1in.6(A,B,C,D) -> evalrealbubblebb2in.8(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && E >= 1 + F] evalrealbubblebb1in.7(A,B,C,D) -> evalrealbubblebb3in.9(A,B,C,C) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && F >= E] evalrealbubblebb2in.8(A,B,C,D) -> evalrealbubblebb3in.9(A,B,C,1) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] evalrealbubblebb3in.9(A,B,C,D) -> evalrealbubblebb4in.4(A,1 + B,D,D) [1 + C + -1*D >= 0 && 1 + B + -1*D >= 0 && A + -1*D >= 0 && D >= 0 && C + D >= 0 && B + D >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] evalrealbubblebb3in.9(A,B,C,D) -> evalrealbubblebb4in.5(A,1 + B,D,D) [1 + C + -1*D >= 0 && 1 + B + -1*D >= 0 && A + -1*D >= 0 && D >= 0 && C + D >= 0 && B + D >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] evalrealbubblebb5in.10(A,B,C,D) -> evalrealbubblereturnin.13(A,B,C,D) [B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && C = 0] evalrealbubblebb5in.11(A,B,C,D) -> evalrealbubblebb6in.12(A,B,C,D) [B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && C >= 1] evalrealbubblebb6in.12(A,B,C,D) -> evalrealbubblebb7in.2(-1 + A,B,C,D) [B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0] evalrealbubblebb6in.12(A,B,C,D) -> evalrealbubblebb7in.3(-1 + A,B,C,D) [B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0] evalrealbubblereturnin.13(A,B,C,D) -> evalrealbubblestop.14(A,B,C,D) True evalrealbubblereturnin.13(A,B,C,D) -> evalrealbubblestop.15(A,B,C,D) True evalrealbubblestop.14(A,B,C,D) -> exitus616.16(A,B,C,D) True evalrealbubblestop.15(A,B,C,D) -> exitus616.16(A,B,C,D) True Signature: {(evalrealbubblebb1in.6,4) ;(evalrealbubblebb1in.7,4) ;(evalrealbubblebb2in.8,4) ;(evalrealbubblebb3in.9,4) ;(evalrealbubblebb4in.4,4) ;(evalrealbubblebb4in.5,4) ;(evalrealbubblebb5in.10,4) ;(evalrealbubblebb5in.11,4) ;(evalrealbubblebb6in.12,4) ;(evalrealbubblebb7in.2,4) ;(evalrealbubblebb7in.3,4) ;(evalrealbubbleentryin.1,4) ;(evalrealbubblereturnin.13,4) ;(evalrealbubblestart.0,4) ;(evalrealbubblestop.14,4) ;(evalrealbubblestop.15,4) ;(exitus616.16,4)} Rule Graph: [0->{1,2},1->{3},2->{4},3->{5,6},4->{18,19},5->{9},6->{10},7->{14},8->{15},9->{11},10->{12,13},11->{12,13} ,12->{5,6},13->{7,8},14->{18,19},15->{16,17},16->{3},17->{4},18->{20},19->{21},20->{},21->{}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21] | `- p:[3,16,15,8,13,10,6,12,11,9,5] c: [3,8,13,15,16] | `- p:[5,12,10,6,11,9] c: [5,6,9,10,11,12] * Step 6: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: evalrealbubblestart.0(A,B,C,D) -> evalrealbubbleentryin.1(A,B,C,D) True evalrealbubbleentryin.1(A,B,C,D) -> evalrealbubblebb7in.2(-1 + A,B,C,D) True evalrealbubbleentryin.1(A,B,C,D) -> evalrealbubblebb7in.3(-1 + A,B,C,D) True evalrealbubblebb7in.2(A,B,C,D) -> evalrealbubblebb4in.4(A,0,0,D) [A >= 1] evalrealbubblebb7in.3(A,B,C,D) -> evalrealbubblereturnin.13(A,B,C,D) [0 >= A] evalrealbubblebb4in.4(A,B,C,D) -> evalrealbubblebb1in.6(A,B,C,D) [B + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && A >= 1 + B] evalrealbubblebb4in.4(A,B,C,D) -> evalrealbubblebb1in.7(A,B,C,D) [B + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && A >= 1 + B] evalrealbubblebb4in.5(A,B,C,D) -> evalrealbubblebb5in.10(A,B,C,D) [B + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && B >= A] evalrealbubblebb4in.5(A,B,C,D) -> evalrealbubblebb5in.11(A,B,C,D) [B + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && B >= A] evalrealbubblebb1in.6(A,B,C,D) -> evalrealbubblebb2in.8(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && E >= 1 + F] evalrealbubblebb1in.7(A,B,C,D) -> evalrealbubblebb3in.9(A,B,C,C) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0 && F >= E] evalrealbubblebb2in.8(A,B,C,D) -> evalrealbubblebb3in.9(A,B,C,1) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] evalrealbubblebb3in.9(A,B,C,D) -> evalrealbubblebb4in.4(A,1 + B,D,D) [1 + C + -1*D >= 0 && 1 + B + -1*D >= 0 && A + -1*D >= 0 && D >= 0 && C + D >= 0 && B + D >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] evalrealbubblebb3in.9(A,B,C,D) -> evalrealbubblebb4in.5(A,1 + B,D,D) [1 + C + -1*D >= 0 && 1 + B + -1*D >= 0 && A + -1*D >= 0 && D >= 0 && C + D >= 0 && B + D >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -1 + A + C >= 0 && -1 + A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && -1 + A >= 0] evalrealbubblebb5in.10(A,B,C,D) -> evalrealbubblereturnin.13(A,B,C,D) [B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && C = 0] evalrealbubblebb5in.11(A,B,C,D) -> evalrealbubblebb6in.12(A,B,C,D) [B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0 && C >= 1] evalrealbubblebb6in.12(A,B,C,D) -> evalrealbubblebb7in.2(-1 + A,B,C,D) [B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0] evalrealbubblebb6in.12(A,B,C,D) -> evalrealbubblebb7in.3(-1 + A,B,C,D) [B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && -1 + A >= 0] evalrealbubblereturnin.13(A,B,C,D) -> evalrealbubblestop.14(A,B,C,D) True evalrealbubblereturnin.13(A,B,C,D) -> evalrealbubblestop.15(A,B,C,D) True evalrealbubblestop.14(A,B,C,D) -> exitus616.16(A,B,C,D) True evalrealbubblestop.15(A,B,C,D) -> exitus616.16(A,B,C,D) True Signature: {(evalrealbubblebb1in.6,4) ;(evalrealbubblebb1in.7,4) ;(evalrealbubblebb2in.8,4) ;(evalrealbubblebb3in.9,4) ;(evalrealbubblebb4in.4,4) ;(evalrealbubblebb4in.5,4) ;(evalrealbubblebb5in.10,4) ;(evalrealbubblebb5in.11,4) ;(evalrealbubblebb6in.12,4) ;(evalrealbubblebb7in.2,4) ;(evalrealbubblebb7in.3,4) ;(evalrealbubbleentryin.1,4) ;(evalrealbubblereturnin.13,4) ;(evalrealbubblestart.0,4) ;(evalrealbubblestop.14,4) ;(evalrealbubblestop.15,4) ;(exitus616.16,4)} Rule Graph: [0->{1,2},1->{3},2->{4},3->{5,6},4->{18,19},5->{9},6->{10},7->{14},8->{15},9->{11},10->{12,13},11->{12,13} ,12->{5,6},13->{7,8},14->{18,19},15->{16,17},16->{3},17->{4},18->{20},19->{21},20->{},21->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21] | `- p:[3,16,15,8,13,10,6,12,11,9,5] c: [3,8,13,15,16] | `- p:[5,12,10,6,11,9] c: [5,6,9,10,11,12]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,0.0,0.0.0] evalrealbubblestart.0 ~> evalrealbubbleentryin.1 [A <= A, B <= B, C <= C, D <= D] evalrealbubbleentryin.1 ~> evalrealbubblebb7in.2 [A <= K + A, B <= B, C <= C, D <= D] evalrealbubbleentryin.1 ~> evalrealbubblebb7in.3 [A <= K + A, B <= B, C <= C, D <= D] evalrealbubblebb7in.2 ~> evalrealbubblebb4in.4 [A <= A, B <= 0*K, C <= 0*K, D <= D] evalrealbubblebb7in.3 ~> evalrealbubblereturnin.13 [A <= A, B <= B, C <= C, D <= D] evalrealbubblebb4in.4 ~> evalrealbubblebb1in.6 [A <= A, B <= B, C <= C, D <= D] evalrealbubblebb4in.4 ~> evalrealbubblebb1in.7 [A <= A, B <= B, C <= C, D <= D] evalrealbubblebb4in.5 ~> evalrealbubblebb5in.10 [A <= A, B <= B, C <= C, D <= D] evalrealbubblebb4in.5 ~> evalrealbubblebb5in.11 [A <= A, B <= B, C <= C, D <= D] evalrealbubblebb1in.6 ~> evalrealbubblebb2in.8 [A <= A, B <= B, C <= C, D <= D] evalrealbubblebb1in.7 ~> evalrealbubblebb3in.9 [A <= A, B <= B, C <= C, D <= C] evalrealbubblebb2in.8 ~> evalrealbubblebb3in.9 [A <= A, B <= B, C <= C, D <= K] evalrealbubblebb3in.9 ~> evalrealbubblebb4in.4 [A <= A, B <= A, C <= D, D <= D] evalrealbubblebb3in.9 ~> evalrealbubblebb4in.5 [A <= A, B <= A, C <= D, D <= D] evalrealbubblebb5in.10 ~> evalrealbubblereturnin.13 [A <= A, B <= B, C <= C, D <= D] evalrealbubblebb5in.11 ~> evalrealbubblebb6in.12 [A <= A, B <= B, C <= C, D <= D] evalrealbubblebb6in.12 ~> evalrealbubblebb7in.2 [A <= B, B <= B, C <= C, D <= D] evalrealbubblebb6in.12 ~> evalrealbubblebb7in.3 [A <= B, B <= B, C <= C, D <= D] evalrealbubblereturnin.13 ~> evalrealbubblestop.14 [A <= A, B <= B, C <= C, D <= D] evalrealbubblereturnin.13 ~> evalrealbubblestop.15 [A <= A, B <= B, C <= C, D <= D] evalrealbubblestop.14 ~> exitus616.16 [A <= A, B <= B, C <= C, D <= D] evalrealbubblestop.15 ~> exitus616.16 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= A] evalrealbubblebb7in.2 ~> evalrealbubblebb4in.4 [A <= A, B <= 0*K, C <= 0*K, D <= D] evalrealbubblebb6in.12 ~> evalrealbubblebb7in.2 [A <= B, B <= B, C <= C, D <= D] evalrealbubblebb5in.11 ~> evalrealbubblebb6in.12 [A <= A, B <= B, C <= C, D <= D] evalrealbubblebb4in.5 ~> evalrealbubblebb5in.11 [A <= A, B <= B, C <= C, D <= D] evalrealbubblebb3in.9 ~> evalrealbubblebb4in.5 [A <= A, B <= A, C <= D, D <= D] evalrealbubblebb1in.7 ~> evalrealbubblebb3in.9 [A <= A, B <= B, C <= C, D <= C] evalrealbubblebb4in.4 ~> evalrealbubblebb1in.7 [A <= A, B <= B, C <= C, D <= D] evalrealbubblebb3in.9 ~> evalrealbubblebb4in.4 [A <= A, B <= A, C <= D, D <= D] evalrealbubblebb2in.8 ~> evalrealbubblebb3in.9 [A <= A, B <= B, C <= C, D <= K] evalrealbubblebb1in.6 ~> evalrealbubblebb2in.8 [A <= A, B <= B, C <= C, D <= D] evalrealbubblebb4in.4 ~> evalrealbubblebb1in.6 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0.0 <= K + A + B] evalrealbubblebb4in.4 ~> evalrealbubblebb1in.6 [A <= A, B <= B, C <= C, D <= D] evalrealbubblebb3in.9 ~> evalrealbubblebb4in.4 [A <= A, B <= A, C <= D, D <= D] evalrealbubblebb1in.7 ~> evalrealbubblebb3in.9 [A <= A, B <= B, C <= C, D <= C] evalrealbubblebb4in.4 ~> evalrealbubblebb1in.7 [A <= A, B <= B, C <= C, D <= D] evalrealbubblebb2in.8 ~> evalrealbubblebb3in.9 [A <= A, B <= B, C <= C, D <= K] evalrealbubblebb1in.6 ~> evalrealbubblebb2in.8 [A <= A, B <= B, C <= C, D <= D] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,0.0,0.0.0] evalrealbubblestart.0 ~> evalrealbubbleentryin.1 [] evalrealbubbleentryin.1 ~> evalrealbubblebb7in.2 [A ~+> A,K ~+> A] evalrealbubbleentryin.1 ~> evalrealbubblebb7in.3 [A ~+> A,K ~+> A] evalrealbubblebb7in.2 ~> evalrealbubblebb4in.4 [K ~=> B,K ~=> C] evalrealbubblebb7in.3 ~> evalrealbubblereturnin.13 [] evalrealbubblebb4in.4 ~> evalrealbubblebb1in.6 [] evalrealbubblebb4in.4 ~> evalrealbubblebb1in.7 [] evalrealbubblebb4in.5 ~> evalrealbubblebb5in.10 [] evalrealbubblebb4in.5 ~> evalrealbubblebb5in.11 [] evalrealbubblebb1in.6 ~> evalrealbubblebb2in.8 [] evalrealbubblebb1in.7 ~> evalrealbubblebb3in.9 [C ~=> D] evalrealbubblebb2in.8 ~> evalrealbubblebb3in.9 [K ~=> D] evalrealbubblebb3in.9 ~> evalrealbubblebb4in.4 [A ~=> B,D ~=> C] evalrealbubblebb3in.9 ~> evalrealbubblebb4in.5 [A ~=> B,D ~=> C] evalrealbubblebb5in.10 ~> evalrealbubblereturnin.13 [] evalrealbubblebb5in.11 ~> evalrealbubblebb6in.12 [] evalrealbubblebb6in.12 ~> evalrealbubblebb7in.2 [B ~=> A] evalrealbubblebb6in.12 ~> evalrealbubblebb7in.3 [B ~=> A] evalrealbubblereturnin.13 ~> evalrealbubblestop.14 [] evalrealbubblereturnin.13 ~> evalrealbubblestop.15 [] evalrealbubblestop.14 ~> exitus616.16 [] evalrealbubblestop.15 ~> exitus616.16 [] + Loop: [A ~=> 0.0] evalrealbubblebb7in.2 ~> evalrealbubblebb4in.4 [K ~=> B,K ~=> C] evalrealbubblebb6in.12 ~> evalrealbubblebb7in.2 [B ~=> A] evalrealbubblebb5in.11 ~> evalrealbubblebb6in.12 [] evalrealbubblebb4in.5 ~> evalrealbubblebb5in.11 [] evalrealbubblebb3in.9 ~> evalrealbubblebb4in.5 [A ~=> B,D ~=> C] evalrealbubblebb1in.7 ~> evalrealbubblebb3in.9 [C ~=> D] evalrealbubblebb4in.4 ~> evalrealbubblebb1in.7 [] evalrealbubblebb3in.9 ~> evalrealbubblebb4in.4 [A ~=> B,D ~=> C] evalrealbubblebb2in.8 ~> evalrealbubblebb3in.9 [K ~=> D] evalrealbubblebb1in.6 ~> evalrealbubblebb2in.8 [] evalrealbubblebb4in.4 ~> evalrealbubblebb1in.6 [] + Loop: [A ~+> 0.0.0,B ~+> 0.0.0,K ~+> 0.0.0] evalrealbubblebb4in.4 ~> evalrealbubblebb1in.6 [] evalrealbubblebb3in.9 ~> evalrealbubblebb4in.4 [A ~=> B,D ~=> C] evalrealbubblebb1in.7 ~> evalrealbubblebb3in.9 [C ~=> D] evalrealbubblebb4in.4 ~> evalrealbubblebb1in.7 [] evalrealbubblebb2in.8 ~> evalrealbubblebb3in.9 [K ~=> D] evalrealbubblebb1in.6 ~> evalrealbubblebb2in.8 [] + Applied Processor: Lare + Details: evalrealbubblestart.0 ~> exitus616.16 [B ~=> A ,D ~=> C ,K ~=> C ,K ~=> D ,A ~+> A ,A ~+> B ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> tick ,K ~*> 0.0.0 ,K ~*> tick] + evalrealbubblebb6in.12> [A ~=> B ,A ~=> 0.0 ,D ~=> C ,K ~=> C ,K ~=> D ,A ~+> 0.0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> tick ,K ~*> 0.0.0 ,K ~*> tick] evalrealbubblebb4in.5> [A ~=> B ,A ~=> 0.0 ,D ~=> C ,K ~=> C ,K ~=> D ,A ~+> 0.0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> tick ,K ~*> 0.0.0 ,K ~*> tick] + evalrealbubblebb3in.9> [A ~=> B ,C ~=> D ,K ~=> C ,K ~=> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> 0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick] YES(?,POLY)