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) [A >= 1 + B] (?,1) 5. evalrealbubblebb4in(A,B,C,D) -> evalrealbubblebb5in(A,B,C,D) [B >= A] (?,1) 6. evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb2in(A,B,C,D) [E >= 1 + F] (?,1) 7. evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,C) [F >= E] (?,1) 8. evalrealbubblebb2in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,1) True (?,1) 9. evalrealbubblebb3in(A,B,C,D) -> evalrealbubblebb4in(A,1 + B,D,D) True (?,1) 10. evalrealbubblebb5in(A,B,C,D) -> evalrealbubblereturnin(A,B,C,D) [C = 0] (?,1) 11. evalrealbubblebb5in(A,B,C,D) -> evalrealbubblebb6in(A,B,C,D) [0 >= 1 + C] (?,1) 12. evalrealbubblebb5in(A,B,C,D) -> evalrealbubblebb6in(A,B,C,D) [C >= 1] (?,1) 13. evalrealbubblebb6in(A,B,C,D) -> evalrealbubblebb7in(-1 + A,B,C,D) True (?,1) 14. 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->{14},4->{6,7},5->{10,11,12},6->{8},7->{9},8->{9},9->{4,5},10->{14},11->{13} ,12->{13},13->{2,3},14->{}] + 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) [A >= 1 + B] (?,1) 5. evalrealbubblebb4in(A,B,C,D) -> evalrealbubblebb5in(A,B,C,D) [B >= A] (?,1) 6. evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb2in(A,B,C,D) [E >= 1 + F] (?,1) 7. evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,C) [F >= E] (?,1) 8. evalrealbubblebb2in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,1) True (?,1) 9. evalrealbubblebb3in(A,B,C,D) -> evalrealbubblebb4in(A,1 + B,D,D) True (?,1) 10. evalrealbubblebb5in(A,B,C,D) -> evalrealbubblereturnin(A,B,C,D) [C = 0] (?,1) 11. evalrealbubblebb5in(A,B,C,D) -> evalrealbubblebb6in(A,B,C,D) [0 >= 1 + C] (?,1) 12. evalrealbubblebb5in(A,B,C,D) -> evalrealbubblebb6in(A,B,C,D) [C >= 1] (?,1) 13. evalrealbubblebb6in(A,B,C,D) -> evalrealbubblebb7in(-1 + A,B,C,D) True (?,1) 14. 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->{14},4->{6,7},5->{10,11,12},6->{8},7->{9},8->{9},9->{4,5},10->{14},11->{13} ,12->{13},13->{2,3},14->{}] + Applied Processor: FromIts + Details: () * Step 3: 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) [A >= 1 + B] evalrealbubblebb4in(A,B,C,D) -> evalrealbubblebb5in(A,B,C,D) [B >= A] evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb2in(A,B,C,D) [E >= 1 + F] evalrealbubblebb1in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,C) [F >= E] evalrealbubblebb2in(A,B,C,D) -> evalrealbubblebb3in(A,B,C,1) True evalrealbubblebb3in(A,B,C,D) -> evalrealbubblebb4in(A,1 + B,D,D) True evalrealbubblebb5in(A,B,C,D) -> evalrealbubblereturnin(A,B,C,D) [C = 0] evalrealbubblebb5in(A,B,C,D) -> evalrealbubblebb6in(A,B,C,D) [0 >= 1 + C] evalrealbubblebb5in(A,B,C,D) -> evalrealbubblebb6in(A,B,C,D) [C >= 1] evalrealbubblebb6in(A,B,C,D) -> evalrealbubblebb7in(-1 + A,B,C,D) True 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->{14},4->{6,7},5->{10,11,12},6->{8},7->{9},8->{9},9->{4,5},10->{14},11->{13} ,12->{13},13->{2,3},14->{}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks 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.14(A,B,C,D) [0 >= A] evalrealbubblebb4in.4(A,B,C,D) -> evalrealbubblebb1in.6(A,B,C,D) [A >= 1 + B] evalrealbubblebb4in.4(A,B,C,D) -> evalrealbubblebb1in.7(A,B,C,D) [A >= 1 + B] evalrealbubblebb4in.5(A,B,C,D) -> evalrealbubblebb5in.10(A,B,C,D) [B >= A] evalrealbubblebb4in.5(A,B,C,D) -> evalrealbubblebb5in.11(A,B,C,D) [B >= A] evalrealbubblebb4in.5(A,B,C,D) -> evalrealbubblebb5in.12(A,B,C,D) [B >= A] evalrealbubblebb1in.6(A,B,C,D) -> evalrealbubblebb2in.8(A,B,C,D) [E >= 1 + F] evalrealbubblebb1in.7(A,B,C,D) -> evalrealbubblebb3in.9(A,B,C,C) [F >= E] evalrealbubblebb2in.8(A,B,C,D) -> evalrealbubblebb3in.9(A,B,C,1) True evalrealbubblebb3in.9(A,B,C,D) -> evalrealbubblebb4in.4(A,1 + B,D,D) True evalrealbubblebb3in.9(A,B,C,D) -> evalrealbubblebb4in.5(A,1 + B,D,D) True evalrealbubblebb5in.10(A,B,C,D) -> evalrealbubblereturnin.14(A,B,C,D) [C = 0] evalrealbubblebb5in.11(A,B,C,D) -> evalrealbubblebb6in.13(A,B,C,D) [0 >= 1 + C] evalrealbubblebb5in.12(A,B,C,D) -> evalrealbubblebb6in.13(A,B,C,D) [C >= 1] evalrealbubblebb6in.13(A,B,C,D) -> evalrealbubblebb7in.2(-1 + A,B,C,D) True evalrealbubblebb6in.13(A,B,C,D) -> evalrealbubblebb7in.3(-1 + A,B,C,D) True evalrealbubblereturnin.14(A,B,C,D) -> evalrealbubblestop.15(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) ;(evalrealbubblebb5in.12,4) ;(evalrealbubblebb6in.13,4) ;(evalrealbubblebb7in.2,4) ;(evalrealbubblebb7in.3,4) ;(evalrealbubbleentryin.1,4) ;(evalrealbubblereturnin.14,4) ;(evalrealbubblestart.0,4) ;(evalrealbubblestop.15,4)} Rule Graph: [0->{1,2},1->{3},2->{4},3->{5,6},4->{20},5->{10},6->{11},7->{15},8->{16},9->{17},10->{12},11->{13,14} ,12->{13,14},13->{5,6},14->{7,8,9},15->{20},16->{18,19},17->{18,19},18->{3},19->{4},20->{}] + Applied Processor: AddSinks + 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.14(A,B,C,D) [0 >= A] evalrealbubblebb4in.4(A,B,C,D) -> evalrealbubblebb1in.6(A,B,C,D) [A >= 1 + B] evalrealbubblebb4in.4(A,B,C,D) -> evalrealbubblebb1in.7(A,B,C,D) [A >= 1 + B] evalrealbubblebb4in.5(A,B,C,D) -> evalrealbubblebb5in.10(A,B,C,D) [B >= A] evalrealbubblebb4in.5(A,B,C,D) -> evalrealbubblebb5in.11(A,B,C,D) [B >= A] evalrealbubblebb4in.5(A,B,C,D) -> evalrealbubblebb5in.12(A,B,C,D) [B >= A] evalrealbubblebb1in.6(A,B,C,D) -> evalrealbubblebb2in.8(A,B,C,D) [E >= 1 + F] evalrealbubblebb1in.7(A,B,C,D) -> evalrealbubblebb3in.9(A,B,C,C) [F >= E] evalrealbubblebb2in.8(A,B,C,D) -> evalrealbubblebb3in.9(A,B,C,1) True evalrealbubblebb3in.9(A,B,C,D) -> evalrealbubblebb4in.4(A,1 + B,D,D) True evalrealbubblebb3in.9(A,B,C,D) -> evalrealbubblebb4in.5(A,1 + B,D,D) True evalrealbubblebb5in.10(A,B,C,D) -> evalrealbubblereturnin.14(A,B,C,D) [C = 0] evalrealbubblebb5in.11(A,B,C,D) -> evalrealbubblebb6in.13(A,B,C,D) [0 >= 1 + C] evalrealbubblebb5in.12(A,B,C,D) -> evalrealbubblebb6in.13(A,B,C,D) [C >= 1] evalrealbubblebb6in.13(A,B,C,D) -> evalrealbubblebb7in.2(-1 + A,B,C,D) True evalrealbubblebb6in.13(A,B,C,D) -> evalrealbubblebb7in.3(-1 + A,B,C,D) True evalrealbubblereturnin.14(A,B,C,D) -> evalrealbubblestop.15(A,B,C,D) True evalrealbubblestop.15(A,B,C,D) -> exitus616(A,B,C,D) True evalrealbubblestop.15(A,B,C,D) -> exitus616(A,B,C,D) True evalrealbubblestop.15(A,B,C,D) -> exitus616(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) ;(evalrealbubblebb5in.12,4) ;(evalrealbubblebb6in.13,4) ;(evalrealbubblebb7in.2,4) ;(evalrealbubblebb7in.3,4) ;(evalrealbubbleentryin.1,4) ;(evalrealbubblereturnin.14,4) ;(evalrealbubblestart.0,4) ;(evalrealbubblestop.15,4) ;(exitus616,4)} Rule Graph: [0->{1,2},1->{3},2->{4},3->{5,6},4->{20},5->{10},6->{11},7->{15},8->{16},9->{17},10->{12},11->{13,14} ,12->{13,14},13->{5,6},14->{7,8,9},15->{20},16->{18,19},17->{18,19},18->{3},19->{4},20->{21,22,23}] + 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,22,23] | `- p:[3,18,16,8,14,11,6,13,12,10,5,17,9] c: [3,8,9,14,16,17,18] | `- p:[5,13,11,6,12,10] c: [5,6,10,11,12,13] * 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.14(A,B,C,D) [0 >= A] evalrealbubblebb4in.4(A,B,C,D) -> evalrealbubblebb1in.6(A,B,C,D) [A >= 1 + B] evalrealbubblebb4in.4(A,B,C,D) -> evalrealbubblebb1in.7(A,B,C,D) [A >= 1 + B] evalrealbubblebb4in.5(A,B,C,D) -> evalrealbubblebb5in.10(A,B,C,D) [B >= A] evalrealbubblebb4in.5(A,B,C,D) -> evalrealbubblebb5in.11(A,B,C,D) [B >= A] evalrealbubblebb4in.5(A,B,C,D) -> evalrealbubblebb5in.12(A,B,C,D) [B >= A] evalrealbubblebb1in.6(A,B,C,D) -> evalrealbubblebb2in.8(A,B,C,D) [E >= 1 + F] evalrealbubblebb1in.7(A,B,C,D) -> evalrealbubblebb3in.9(A,B,C,C) [F >= E] evalrealbubblebb2in.8(A,B,C,D) -> evalrealbubblebb3in.9(A,B,C,1) True evalrealbubblebb3in.9(A,B,C,D) -> evalrealbubblebb4in.4(A,1 + B,D,D) True evalrealbubblebb3in.9(A,B,C,D) -> evalrealbubblebb4in.5(A,1 + B,D,D) True evalrealbubblebb5in.10(A,B,C,D) -> evalrealbubblereturnin.14(A,B,C,D) [C = 0] evalrealbubblebb5in.11(A,B,C,D) -> evalrealbubblebb6in.13(A,B,C,D) [0 >= 1 + C] evalrealbubblebb5in.12(A,B,C,D) -> evalrealbubblebb6in.13(A,B,C,D) [C >= 1] evalrealbubblebb6in.13(A,B,C,D) -> evalrealbubblebb7in.2(-1 + A,B,C,D) True evalrealbubblebb6in.13(A,B,C,D) -> evalrealbubblebb7in.3(-1 + A,B,C,D) True evalrealbubblereturnin.14(A,B,C,D) -> evalrealbubblestop.15(A,B,C,D) True evalrealbubblestop.15(A,B,C,D) -> exitus616(A,B,C,D) True evalrealbubblestop.15(A,B,C,D) -> exitus616(A,B,C,D) True evalrealbubblestop.15(A,B,C,D) -> exitus616(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) ;(evalrealbubblebb5in.12,4) ;(evalrealbubblebb6in.13,4) ;(evalrealbubblebb7in.2,4) ;(evalrealbubblebb7in.3,4) ;(evalrealbubbleentryin.1,4) ;(evalrealbubblereturnin.14,4) ;(evalrealbubblestart.0,4) ;(evalrealbubblestop.15,4) ;(exitus616,4)} Rule Graph: [0->{1,2},1->{3},2->{4},3->{5,6},4->{20},5->{10},6->{11},7->{15},8->{16},9->{17},10->{12},11->{13,14} ,12->{13,14},13->{5,6},14->{7,8,9},15->{20},16->{18,19},17->{18,19},18->{3},19->{4},20->{21,22,23}] ,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,22,23] | `- p:[3,18,16,8,14,11,6,13,12,10,5,17,9] c: [3,8,9,14,16,17,18] | `- p:[5,13,11,6,12,10] c: [5,6,10,11,12,13]) + 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.14 [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] evalrealbubblebb4in.5 ~> evalrealbubblebb5in.12 [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 <= K + B, C <= D, D <= D] evalrealbubblebb3in.9 ~> evalrealbubblebb4in.5 [A <= A, B <= K + B, C <= D, D <= D] evalrealbubblebb5in.10 ~> evalrealbubblereturnin.14 [A <= A, B <= B, C <= C, D <= D] evalrealbubblebb5in.11 ~> evalrealbubblebb6in.13 [A <= A, B <= B, C <= C, D <= D] evalrealbubblebb5in.12 ~> evalrealbubblebb6in.13 [A <= A, B <= B, C <= C, D <= D] evalrealbubblebb6in.13 ~> evalrealbubblebb7in.2 [A <= K + A, B <= B, C <= C, D <= D] evalrealbubblebb6in.13 ~> evalrealbubblebb7in.3 [A <= K + A, B <= B, C <= C, D <= D] evalrealbubblereturnin.14 ~> evalrealbubblestop.15 [A <= A, B <= B, C <= C, D <= D] evalrealbubblestop.15 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] evalrealbubblestop.15 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] evalrealbubblestop.15 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= K + A] evalrealbubblebb7in.2 ~> evalrealbubblebb4in.4 [A <= A, B <= 0*K, C <= 0*K, D <= D] evalrealbubblebb6in.13 ~> evalrealbubblebb7in.2 [A <= K + A, B <= B, C <= C, D <= D] evalrealbubblebb5in.11 ~> evalrealbubblebb6in.13 [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 <= K + B, 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 <= K + B, 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] evalrealbubblebb5in.12 ~> evalrealbubblebb6in.13 [A <= A, B <= B, C <= C, D <= D] evalrealbubblebb4in.5 ~> evalrealbubblebb5in.12 [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 <= K + B, 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.14 [] evalrealbubblebb4in.4 ~> evalrealbubblebb1in.6 [] evalrealbubblebb4in.4 ~> evalrealbubblebb1in.7 [] evalrealbubblebb4in.5 ~> evalrealbubblebb5in.10 [] evalrealbubblebb4in.5 ~> evalrealbubblebb5in.11 [] evalrealbubblebb4in.5 ~> evalrealbubblebb5in.12 [] evalrealbubblebb1in.6 ~> evalrealbubblebb2in.8 [] evalrealbubblebb1in.7 ~> evalrealbubblebb3in.9 [C ~=> D] evalrealbubblebb2in.8 ~> evalrealbubblebb3in.9 [K ~=> D] evalrealbubblebb3in.9 ~> evalrealbubblebb4in.4 [D ~=> C,B ~+> B,K ~+> B] evalrealbubblebb3in.9 ~> evalrealbubblebb4in.5 [D ~=> C,B ~+> B,K ~+> B] evalrealbubblebb5in.10 ~> evalrealbubblereturnin.14 [] evalrealbubblebb5in.11 ~> evalrealbubblebb6in.13 [] evalrealbubblebb5in.12 ~> evalrealbubblebb6in.13 [] evalrealbubblebb6in.13 ~> evalrealbubblebb7in.2 [A ~+> A,K ~+> A] evalrealbubblebb6in.13 ~> evalrealbubblebb7in.3 [A ~+> A,K ~+> A] evalrealbubblereturnin.14 ~> evalrealbubblestop.15 [] evalrealbubblestop.15 ~> exitus616 [] evalrealbubblestop.15 ~> exitus616 [] evalrealbubblestop.15 ~> exitus616 [] + Loop: [A ~+> 0.0,K ~+> 0.0] evalrealbubblebb7in.2 ~> evalrealbubblebb4in.4 [K ~=> B,K ~=> C] evalrealbubblebb6in.13 ~> evalrealbubblebb7in.2 [A ~+> A,K ~+> A] evalrealbubblebb5in.11 ~> evalrealbubblebb6in.13 [] evalrealbubblebb4in.5 ~> evalrealbubblebb5in.11 [] evalrealbubblebb3in.9 ~> evalrealbubblebb4in.5 [D ~=> C,B ~+> B,K ~+> B] evalrealbubblebb1in.7 ~> evalrealbubblebb3in.9 [C ~=> D] evalrealbubblebb4in.4 ~> evalrealbubblebb1in.7 [] evalrealbubblebb3in.9 ~> evalrealbubblebb4in.4 [D ~=> C,B ~+> B,K ~+> B] evalrealbubblebb2in.8 ~> evalrealbubblebb3in.9 [K ~=> D] evalrealbubblebb1in.6 ~> evalrealbubblebb2in.8 [] evalrealbubblebb4in.4 ~> evalrealbubblebb1in.6 [] evalrealbubblebb5in.12 ~> evalrealbubblebb6in.13 [] evalrealbubblebb4in.5 ~> evalrealbubblebb5in.12 [] + Loop: [A ~+> 0.0.0,B ~+> 0.0.0,K ~+> 0.0.0] evalrealbubblebb4in.4 ~> evalrealbubblebb1in.6 [] evalrealbubblebb3in.9 ~> evalrealbubblebb4in.4 [D ~=> C,B ~+> B,K ~+> B] 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 [D ~=> C ,K ~=> C ,K ~=> D ,A ~+> A ,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 ~*> A ,A ~*> B ,A ~*> 0.0.0 ,A ~*> tick ,K ~*> A ,K ~*> B ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick] + evalrealbubblebb6in.13> [D ~=> C ,K ~=> C ,K ~=> D ,A ~+> A ,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 ~*> A ,A ~*> B ,A ~*> 0.0.0 ,A ~*> tick ,K ~*> A ,K ~*> B ,K ~*> 0.0.0 ,K ~*> tick] evalrealbubblebb4in.5> [D ~=> C ,K ~=> C ,K ~=> D ,A ~+> A ,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 ~*> A ,A ~*> B ,A ~*> 0.0.0 ,A ~*> tick ,K ~*> A ,K ~*> B ,K ~*> 0.0.0 ,K ~*> tick] + evalrealbubblebb3in.9> [C ~=> D ,K ~=> C ,K ~=> D ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> B ,B ~*> B ,K ~*> B] YES(?,POLY)