YES(?,POLY) * Step 1: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalrealshellsortstart(A,B,C,D,E) -> evalrealshellsortentryin(A,B,C,D,E) True (1,1) 1. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,0,C,D,E) [A = 0] (?,1) 2. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [A >= 1 && F >= 0 && A >= 2*F && 1 + 2*F >= A] (?,1) 3. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [0 >= 1 + A && 0 >= F && 2*F >= A && 1 + A >= 2*F] (?,1) 4. evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,0,D,E) [B >= 1] (?,1) 5. evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortreturnin(A,B,C,D,E) [0 >= B] (?,1) 6. evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb1in(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && A >= 1 + C] (?,1) 7. evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb7in(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && C >= A] (?,1) 8. evalrealshellsortbb1in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,F,C) [-1 + A + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 9. evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + E] 10. evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb4in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= B] 11. evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb2in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && F >= 1 + D] 12. evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && D >= F] 13. evalrealshellsortbb2in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,D,-1*B + E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] 14. evalrealshellsortbb5in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,1 + C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 15. evalrealshellsortbb7in(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1*A + C >= 0 && -1 + B >= 0 && B >= 1 && F >= 0 && B >= 2*F && 1 + 2*F >= B] (?,1) 16. evalrealshellsortreturnin(A,B,C,D,E) -> evalrealshellsortstop(A,B,C,D,E) [-1*B >= 0] (?,1) Signature: {(evalrealshellsortbb1in,5) ;(evalrealshellsortbb2in,5) ;(evalrealshellsortbb3in,5) ;(evalrealshellsortbb4in,5) ;(evalrealshellsortbb5in,5) ;(evalrealshellsortbb6in,5) ;(evalrealshellsortbb7in,5) ;(evalrealshellsortbb8in,5) ;(evalrealshellsortentryin,5) ;(evalrealshellsortreturnin,5) ;(evalrealshellsortstart,5) ;(evalrealshellsortstop,5)} Flow Graph: [0->{1,2,3},1->{4,5},2->{4,5},3->{4,5},4->{6,7},5->{16},6->{8},7->{15},8->{9,10},9->{14},10->{11,12} ,11->{13},12->{14},13->{9,10},14->{6,7},15->{4,5},16->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,4),(3,4)] * Step 2: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalrealshellsortstart(A,B,C,D,E) -> evalrealshellsortentryin(A,B,C,D,E) True (1,1) 1. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,0,C,D,E) [A = 0] (?,1) 2. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [A >= 1 && F >= 0 && A >= 2*F && 1 + 2*F >= A] (?,1) 3. evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [0 >= 1 + A && 0 >= F && 2*F >= A && 1 + A >= 2*F] (?,1) 4. evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,0,D,E) [B >= 1] (?,1) 5. evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortreturnin(A,B,C,D,E) [0 >= B] (?,1) 6. evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb1in(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && A >= 1 + C] (?,1) 7. evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb7in(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && C >= A] (?,1) 8. evalrealshellsortbb1in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,F,C) [-1 + A + -1*C >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 9. evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + E] 10. evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb4in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= B] 11. evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb2in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && F >= 1 + D] 12. evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && D >= F] 13. evalrealshellsortbb2in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,D,-1*B + E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] 14. evalrealshellsortbb5in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,1 + C,D,E) [C + -1*E >= 0 (?,1) && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] 15. evalrealshellsortbb7in(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1*A + C >= 0 && -1 + B >= 0 && B >= 1 && F >= 0 && B >= 2*F && 1 + 2*F >= B] (?,1) 16. evalrealshellsortreturnin(A,B,C,D,E) -> evalrealshellsortstop(A,B,C,D,E) [-1*B >= 0] (?,1) Signature: {(evalrealshellsortbb1in,5) ;(evalrealshellsortbb2in,5) ;(evalrealshellsortbb3in,5) ;(evalrealshellsortbb4in,5) ;(evalrealshellsortbb5in,5) ;(evalrealshellsortbb6in,5) ;(evalrealshellsortbb7in,5) ;(evalrealshellsortbb8in,5) ;(evalrealshellsortentryin,5) ;(evalrealshellsortreturnin,5) ;(evalrealshellsortstart,5) ;(evalrealshellsortstop,5)} Flow Graph: [0->{1,2,3},1->{5},2->{4,5},3->{5},4->{6,7},5->{16},6->{8},7->{15},8->{9,10},9->{14},10->{11,12},11->{13} ,12->{14},13->{9,10},14->{6,7},15->{4,5},16->{}] + Applied Processor: FromIts + Details: () * Step 3: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: evalrealshellsortstart(A,B,C,D,E) -> evalrealshellsortentryin(A,B,C,D,E) True evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,0,C,D,E) [A = 0] evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [A >= 1 && F >= 0 && A >= 2*F && 1 + 2*F >= A] evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [0 >= 1 + A && 0 >= F && 2*F >= A && 1 + A >= 2*F] evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,0,D,E) [B >= 1] evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortreturnin(A,B,C,D,E) [0 >= B] evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb1in(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && A >= 1 + C] evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb7in(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && C >= A] evalrealshellsortbb1in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,F,C) [-1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + E] evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb4in(A,B,C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= B] evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb2in(A,B,C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && F >= 1 + D] evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && D >= F] evalrealshellsortbb2in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,D,-1*B + E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] evalrealshellsortbb5in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,1 + C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] evalrealshellsortbb7in(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1*A + C >= 0 && -1 + B >= 0 && B >= 1 && F >= 0 && B >= 2*F && 1 + 2*F >= B] evalrealshellsortreturnin(A,B,C,D,E) -> evalrealshellsortstop(A,B,C,D,E) [-1*B >= 0] Signature: {(evalrealshellsortbb1in,5) ;(evalrealshellsortbb2in,5) ;(evalrealshellsortbb3in,5) ;(evalrealshellsortbb4in,5) ;(evalrealshellsortbb5in,5) ;(evalrealshellsortbb6in,5) ;(evalrealshellsortbb7in,5) ;(evalrealshellsortbb8in,5) ;(evalrealshellsortentryin,5) ;(evalrealshellsortreturnin,5) ;(evalrealshellsortstart,5) ;(evalrealshellsortstop,5)} Rule Graph: [0->{1,2,3},1->{5},2->{4,5},3->{5},4->{6,7},5->{16},6->{8},7->{15},8->{9,10},9->{14},10->{11,12},11->{13} ,12->{14},13->{9,10},14->{6,7},15->{4,5},16->{}] + Applied Processor: AddSinks + Details: () * Step 4: Unfold WORST_CASE(?,POLY) + Considered Problem: Rules: evalrealshellsortstart(A,B,C,D,E) -> evalrealshellsortentryin(A,B,C,D,E) True evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,0,C,D,E) [A = 0] evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [A >= 1 && F >= 0 && A >= 2*F && 1 + 2*F >= A] evalrealshellsortentryin(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [0 >= 1 + A && 0 >= F && 2*F >= A && 1 + A >= 2*F] evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,0,D,E) [B >= 1] evalrealshellsortbb8in(A,B,C,D,E) -> evalrealshellsortreturnin(A,B,C,D,E) [0 >= B] evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb1in(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && A >= 1 + C] evalrealshellsortbb6in(A,B,C,D,E) -> evalrealshellsortbb7in(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && C >= A] evalrealshellsortbb1in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,F,C) [-1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + E] evalrealshellsortbb3in(A,B,C,D,E) -> evalrealshellsortbb4in(A,B,C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= B] evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb2in(A,B,C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && F >= 1 + D] evalrealshellsortbb4in(A,B,C,D,E) -> evalrealshellsortbb5in(A,B,C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && D >= F] evalrealshellsortbb2in(A,B,C,D,E) -> evalrealshellsortbb3in(A,B,C,D,-1*B + E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] evalrealshellsortbb5in(A,B,C,D,E) -> evalrealshellsortbb6in(A,B,1 + C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] evalrealshellsortbb7in(A,B,C,D,E) -> evalrealshellsortbb8in(A,F,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1*A + C >= 0 && -1 + B >= 0 && B >= 1 && F >= 0 && B >= 2*F && 1 + 2*F >= B] evalrealshellsortreturnin(A,B,C,D,E) -> evalrealshellsortstop(A,B,C,D,E) [-1*B >= 0] evalrealshellsortstop(A,B,C,D,E) -> exitus616(A,B,C,D,E) True evalrealshellsortstop(A,B,C,D,E) -> exitus616(A,B,C,D,E) True evalrealshellsortstop(A,B,C,D,E) -> exitus616(A,B,C,D,E) True Signature: {(evalrealshellsortbb1in,5) ;(evalrealshellsortbb2in,5) ;(evalrealshellsortbb3in,5) ;(evalrealshellsortbb4in,5) ;(evalrealshellsortbb5in,5) ;(evalrealshellsortbb6in,5) ;(evalrealshellsortbb7in,5) ;(evalrealshellsortbb8in,5) ;(evalrealshellsortentryin,5) ;(evalrealshellsortreturnin,5) ;(evalrealshellsortstart,5) ;(evalrealshellsortstop,5) ;(exitus616,5)} Rule Graph: [0->{1,2,3},1->{5},2->{4,5},3->{5},4->{6,7},5->{16},6->{8},7->{15},8->{9,10},9->{14},10->{11,12},11->{13} ,12->{14},13->{9,10},14->{6,7},15->{4,5},16->{17,18,19}] + Applied Processor: Unfold + Details: () * Step 5: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: evalrealshellsortstart.0(A,B,C,D,E) -> evalrealshellsortentryin.1(A,B,C,D,E) True evalrealshellsortstart.0(A,B,C,D,E) -> evalrealshellsortentryin.2(A,B,C,D,E) True evalrealshellsortstart.0(A,B,C,D,E) -> evalrealshellsortentryin.3(A,B,C,D,E) True evalrealshellsortentryin.1(A,B,C,D,E) -> evalrealshellsortbb8in.5(A,0,C,D,E) [A = 0] evalrealshellsortentryin.2(A,B,C,D,E) -> evalrealshellsortbb8in.4(A,F,C,D,E) [A >= 1 && F >= 0 && A >= 2*F && 1 + 2*F >= A] evalrealshellsortentryin.2(A,B,C,D,E) -> evalrealshellsortbb8in.5(A,F,C,D,E) [A >= 1 && F >= 0 && A >= 2*F && 1 + 2*F >= A] evalrealshellsortentryin.3(A,B,C,D,E) -> evalrealshellsortbb8in.5(A,F,C,D,E) [0 >= 1 + A && 0 >= F && 2*F >= A && 1 + A >= 2*F] evalrealshellsortbb8in.4(A,B,C,D,E) -> evalrealshellsortbb6in.6(A,B,0,D,E) [B >= 1] evalrealshellsortbb8in.4(A,B,C,D,E) -> evalrealshellsortbb6in.7(A,B,0,D,E) [B >= 1] evalrealshellsortbb8in.5(A,B,C,D,E) -> evalrealshellsortreturnin.16(A,B,C,D,E) [0 >= B] evalrealshellsortbb6in.6(A,B,C,D,E) -> evalrealshellsortbb1in.8(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && A >= 1 + C] evalrealshellsortbb6in.7(A,B,C,D,E) -> evalrealshellsortbb7in.15(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && C >= A] evalrealshellsortbb1in.8(A,B,C,D,E) -> evalrealshellsortbb3in.9(A,B,C,F,C) [-1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] evalrealshellsortbb1in.8(A,B,C,D,E) -> evalrealshellsortbb3in.10(A,B,C,F,C) [-1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] evalrealshellsortbb3in.9(A,B,C,D,E) -> evalrealshellsortbb5in.14(A,B,C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + E] evalrealshellsortbb3in.10(A,B,C,D,E) -> evalrealshellsortbb4in.11(A,B,C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= B] evalrealshellsortbb3in.10(A,B,C,D,E) -> evalrealshellsortbb4in.12(A,B,C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= B] evalrealshellsortbb4in.11(A,B,C,D,E) -> evalrealshellsortbb2in.13(A,B,C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && F >= 1 + D] evalrealshellsortbb4in.12(A,B,C,D,E) -> evalrealshellsortbb5in.14(A,B,C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && D >= F] evalrealshellsortbb2in.13(A,B,C,D,E) -> evalrealshellsortbb3in.9(A,B,C,D,-1*B + E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] evalrealshellsortbb2in.13(A,B,C,D,E) -> evalrealshellsortbb3in.10(A,B,C,D,-1*B + E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] evalrealshellsortbb5in.14(A,B,C,D,E) -> evalrealshellsortbb6in.6(A,B,1 + C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] evalrealshellsortbb5in.14(A,B,C,D,E) -> evalrealshellsortbb6in.7(A,B,1 + C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] evalrealshellsortbb7in.15(A,B,C,D,E) -> evalrealshellsortbb8in.4(A,F,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1*A + C >= 0 && -1 + B >= 0 && B >= 1 && F >= 0 && B >= 2*F && 1 + 2*F >= B] evalrealshellsortbb7in.15(A,B,C,D,E) -> evalrealshellsortbb8in.5(A,F,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1*A + C >= 0 && -1 + B >= 0 && B >= 1 && F >= 0 && B >= 2*F && 1 + 2*F >= B] evalrealshellsortreturnin.16(A,B,C,D,E) -> evalrealshellsortstop.17(A,B,C,D,E) [-1*B >= 0] evalrealshellsortreturnin.16(A,B,C,D,E) -> evalrealshellsortstop.18(A,B,C,D,E) [-1*B >= 0] evalrealshellsortreturnin.16(A,B,C,D,E) -> evalrealshellsortstop.19(A,B,C,D,E) [-1*B >= 0] evalrealshellsortstop.17(A,B,C,D,E) -> exitus616.20(A,B,C,D,E) True evalrealshellsortstop.18(A,B,C,D,E) -> exitus616.20(A,B,C,D,E) True evalrealshellsortstop.19(A,B,C,D,E) -> exitus616.20(A,B,C,D,E) True Signature: {(evalrealshellsortbb1in.8,5) ;(evalrealshellsortbb2in.13,5) ;(evalrealshellsortbb3in.10,5) ;(evalrealshellsortbb3in.9,5) ;(evalrealshellsortbb4in.11,5) ;(evalrealshellsortbb4in.12,5) ;(evalrealshellsortbb5in.14,5) ;(evalrealshellsortbb6in.6,5) ;(evalrealshellsortbb6in.7,5) ;(evalrealshellsortbb7in.15,5) ;(evalrealshellsortbb8in.4,5) ;(evalrealshellsortbb8in.5,5) ;(evalrealshellsortentryin.1,5) ;(evalrealshellsortentryin.2,5) ;(evalrealshellsortentryin.3,5) ;(evalrealshellsortreturnin.16,5) ;(evalrealshellsortstart.0,5) ;(evalrealshellsortstop.17,5) ;(evalrealshellsortstop.18,5) ;(evalrealshellsortstop.19,5) ;(exitus616.20,5)} Rule Graph: [0->{3},1->{4,5},2->{6},3->{9},4->{7,8},5->{9},6->{9},7->{10},8->{11},9->{25,26,27},10->{12,13},11->{23 ,24},12->{14},13->{15,16},14->{21,22},15->{17},16->{18},17->{19,20},18->{21,22},19->{14},20->{15,16} ,21->{10},22->{11},23->{7,8},24->{9},25->{28},26->{29},27->{30},28->{},29->{},30->{}] + 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,24,25,26,27,28,29,30] | `- p:[7,23,11,8,22,14,12,10,21,18,16,13,20,17,15,19] c: [7,8,11,22,23] | `- p:[10,21,14,12,19,17,15,13,20,18,16] c: [10,12,13,14,16,18,19,21] | `- p:[15,20,17] c: [15,17,20] * Step 6: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: evalrealshellsortstart.0(A,B,C,D,E) -> evalrealshellsortentryin.1(A,B,C,D,E) True evalrealshellsortstart.0(A,B,C,D,E) -> evalrealshellsortentryin.2(A,B,C,D,E) True evalrealshellsortstart.0(A,B,C,D,E) -> evalrealshellsortentryin.3(A,B,C,D,E) True evalrealshellsortentryin.1(A,B,C,D,E) -> evalrealshellsortbb8in.5(A,0,C,D,E) [A = 0] evalrealshellsortentryin.2(A,B,C,D,E) -> evalrealshellsortbb8in.4(A,F,C,D,E) [A >= 1 && F >= 0 && A >= 2*F && 1 + 2*F >= A] evalrealshellsortentryin.2(A,B,C,D,E) -> evalrealshellsortbb8in.5(A,F,C,D,E) [A >= 1 && F >= 0 && A >= 2*F && 1 + 2*F >= A] evalrealshellsortentryin.3(A,B,C,D,E) -> evalrealshellsortbb8in.5(A,F,C,D,E) [0 >= 1 + A && 0 >= F && 2*F >= A && 1 + A >= 2*F] evalrealshellsortbb8in.4(A,B,C,D,E) -> evalrealshellsortbb6in.6(A,B,0,D,E) [B >= 1] evalrealshellsortbb8in.4(A,B,C,D,E) -> evalrealshellsortbb6in.7(A,B,0,D,E) [B >= 1] evalrealshellsortbb8in.5(A,B,C,D,E) -> evalrealshellsortreturnin.16(A,B,C,D,E) [0 >= B] evalrealshellsortbb6in.6(A,B,C,D,E) -> evalrealshellsortbb1in.8(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && A >= 1 + C] evalrealshellsortbb6in.7(A,B,C,D,E) -> evalrealshellsortbb7in.15(A,B,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1 + B >= 0 && C >= A] evalrealshellsortbb1in.8(A,B,C,D,E) -> evalrealshellsortbb3in.9(A,B,C,F,C) [-1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] evalrealshellsortbb1in.8(A,B,C,D,E) -> evalrealshellsortbb3in.10(A,B,C,F,C) [-1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] evalrealshellsortbb3in.9(A,B,C,D,E) -> evalrealshellsortbb5in.14(A,B,C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + E] evalrealshellsortbb3in.10(A,B,C,D,E) -> evalrealshellsortbb4in.11(A,B,C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= B] evalrealshellsortbb3in.10(A,B,C,D,E) -> evalrealshellsortbb4in.12(A,B,C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= B] evalrealshellsortbb4in.11(A,B,C,D,E) -> evalrealshellsortbb2in.13(A,B,C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && F >= 1 + D] evalrealshellsortbb4in.12(A,B,C,D,E) -> evalrealshellsortbb5in.14(A,B,C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0 && D >= F] evalrealshellsortbb2in.13(A,B,C,D,E) -> evalrealshellsortbb3in.9(A,B,C,D,-1*B + E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] evalrealshellsortbb2in.13(A,B,C,D,E) -> evalrealshellsortbb3in.10(A,B,C,D,-1*B + E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1*B + E >= 0 && -3 + A + E >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -3 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] evalrealshellsortbb5in.14(A,B,C,D,E) -> evalrealshellsortbb6in.6(A,B,1 + C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] evalrealshellsortbb5in.14(A,B,C,D,E) -> evalrealshellsortbb6in.7(A,B,1 + C,D,E) [C + -1*E >= 0 && -1 + A + -1*E >= 0 && C + E >= 0 && -1 + B + E >= 0 && -1 + A + E >= 0 && -1 + A + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] evalrealshellsortbb7in.15(A,B,C,D,E) -> evalrealshellsortbb8in.4(A,F,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1*A + C >= 0 && -1 + B >= 0 && B >= 1 && F >= 0 && B >= 2*F && 1 + 2*F >= B] evalrealshellsortbb7in.15(A,B,C,D,E) -> evalrealshellsortbb8in.5(A,F,C,D,E) [C >= 0 && -1 + B + C >= 0 && -1*A + C >= 0 && -1 + B >= 0 && B >= 1 && F >= 0 && B >= 2*F && 1 + 2*F >= B] evalrealshellsortreturnin.16(A,B,C,D,E) -> evalrealshellsortstop.17(A,B,C,D,E) [-1*B >= 0] evalrealshellsortreturnin.16(A,B,C,D,E) -> evalrealshellsortstop.18(A,B,C,D,E) [-1*B >= 0] evalrealshellsortreturnin.16(A,B,C,D,E) -> evalrealshellsortstop.19(A,B,C,D,E) [-1*B >= 0] evalrealshellsortstop.17(A,B,C,D,E) -> exitus616.20(A,B,C,D,E) True evalrealshellsortstop.18(A,B,C,D,E) -> exitus616.20(A,B,C,D,E) True evalrealshellsortstop.19(A,B,C,D,E) -> exitus616.20(A,B,C,D,E) True Signature: {(evalrealshellsortbb1in.8,5) ;(evalrealshellsortbb2in.13,5) ;(evalrealshellsortbb3in.10,5) ;(evalrealshellsortbb3in.9,5) ;(evalrealshellsortbb4in.11,5) ;(evalrealshellsortbb4in.12,5) ;(evalrealshellsortbb5in.14,5) ;(evalrealshellsortbb6in.6,5) ;(evalrealshellsortbb6in.7,5) ;(evalrealshellsortbb7in.15,5) ;(evalrealshellsortbb8in.4,5) ;(evalrealshellsortbb8in.5,5) ;(evalrealshellsortentryin.1,5) ;(evalrealshellsortentryin.2,5) ;(evalrealshellsortentryin.3,5) ;(evalrealshellsortreturnin.16,5) ;(evalrealshellsortstart.0,5) ;(evalrealshellsortstop.17,5) ;(evalrealshellsortstop.18,5) ;(evalrealshellsortstop.19,5) ;(exitus616.20,5)} Rule Graph: [0->{3},1->{4,5},2->{6},3->{9},4->{7,8},5->{9},6->{9},7->{10},8->{11},9->{25,26,27},10->{12,13},11->{23 ,24},12->{14},13->{15,16},14->{21,22},15->{17},16->{18},17->{19,20},18->{21,22},19->{14},20->{15,16} ,21->{10},22->{11},23->{7,8},24->{9},25->{28},26->{29},27->{30},28->{},29->{},30->{}] ,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,24,25,26,27,28,29,30] | `- p:[7,23,11,8,22,14,12,10,21,18,16,13,20,17,15,19] c: [7,8,11,22,23] | `- p:[10,21,14,12,19,17,15,13,20,18,16] c: [10,12,13,14,16,18,19,21] | `- p:[15,20,17] c: [15,17,20]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,E,0.0,0.0.0,0.0.0.0] evalrealshellsortstart.0 ~> evalrealshellsortentryin.1 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortstart.0 ~> evalrealshellsortentryin.2 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortstart.0 ~> evalrealshellsortentryin.3 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortentryin.1 ~> evalrealshellsortbb8in.5 [A <= A, B <= 0*K, C <= C, D <= D, E <= E] evalrealshellsortentryin.2 ~> evalrealshellsortbb8in.4 [A <= A, B <= A, C <= C, D <= D, E <= E] evalrealshellsortentryin.2 ~> evalrealshellsortbb8in.5 [A <= A, B <= A, C <= C, D <= D, E <= E] evalrealshellsortentryin.3 ~> evalrealshellsortbb8in.5 [A <= A, B <= A, C <= C, D <= D, E <= E] evalrealshellsortbb8in.4 ~> evalrealshellsortbb6in.6 [A <= A, B <= B, C <= 0*K, D <= D, E <= E] evalrealshellsortbb8in.4 ~> evalrealshellsortbb6in.7 [A <= A, B <= B, C <= 0*K, D <= D, E <= E] evalrealshellsortbb8in.5 ~> evalrealshellsortreturnin.16 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb6in.6 ~> evalrealshellsortbb1in.8 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb6in.7 ~> evalrealshellsortbb7in.15 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb1in.8 ~> evalrealshellsortbb3in.9 [A <= A, B <= B, C <= C, D <= unknown, E <= C] evalrealshellsortbb1in.8 ~> evalrealshellsortbb3in.10 [A <= A, B <= B, C <= C, D <= unknown, E <= C] evalrealshellsortbb3in.9 ~> evalrealshellsortbb5in.14 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb3in.10 ~> evalrealshellsortbb4in.11 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb3in.10 ~> evalrealshellsortbb4in.12 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb4in.11 ~> evalrealshellsortbb2in.13 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb4in.12 ~> evalrealshellsortbb5in.14 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb2in.13 ~> evalrealshellsortbb3in.9 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb2in.13 ~> evalrealshellsortbb3in.10 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb5in.14 ~> evalrealshellsortbb6in.6 [A <= A, B <= B, C <= A, D <= D, E <= E] evalrealshellsortbb5in.14 ~> evalrealshellsortbb6in.7 [A <= A, B <= B, C <= A, D <= D, E <= E] evalrealshellsortbb7in.15 ~> evalrealshellsortbb8in.4 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb7in.15 ~> evalrealshellsortbb8in.5 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortreturnin.16 ~> evalrealshellsortstop.17 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortreturnin.16 ~> evalrealshellsortstop.18 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortreturnin.16 ~> evalrealshellsortstop.19 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortstop.17 ~> exitus616.20 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortstop.18 ~> exitus616.20 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortstop.19 ~> exitus616.20 [A <= A, B <= B, C <= C, D <= D, E <= E] + Loop: [0.0 <= 2*K + 2*B] evalrealshellsortbb8in.4 ~> evalrealshellsortbb6in.6 [A <= A, B <= B, C <= 0*K, D <= D, E <= E] evalrealshellsortbb7in.15 ~> evalrealshellsortbb8in.4 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb6in.7 ~> evalrealshellsortbb7in.15 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb8in.4 ~> evalrealshellsortbb6in.7 [A <= A, B <= B, C <= 0*K, D <= D, E <= E] evalrealshellsortbb5in.14 ~> evalrealshellsortbb6in.7 [A <= A, B <= B, C <= A, D <= D, E <= E] evalrealshellsortbb3in.9 ~> evalrealshellsortbb5in.14 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb1in.8 ~> evalrealshellsortbb3in.9 [A <= A, B <= B, C <= C, D <= unknown, E <= C] evalrealshellsortbb6in.6 ~> evalrealshellsortbb1in.8 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb5in.14 ~> evalrealshellsortbb6in.6 [A <= A, B <= B, C <= A, D <= D, E <= E] evalrealshellsortbb4in.12 ~> evalrealshellsortbb5in.14 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb3in.10 ~> evalrealshellsortbb4in.12 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb1in.8 ~> evalrealshellsortbb3in.10 [A <= A, B <= B, C <= C, D <= unknown, E <= C] evalrealshellsortbb2in.13 ~> evalrealshellsortbb3in.10 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb4in.11 ~> evalrealshellsortbb2in.13 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb3in.10 ~> evalrealshellsortbb4in.11 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb2in.13 ~> evalrealshellsortbb3in.9 [A <= A, B <= B, C <= C, D <= D, E <= E] + Loop: [0.0.0 <= A + C] evalrealshellsortbb6in.6 ~> evalrealshellsortbb1in.8 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb5in.14 ~> evalrealshellsortbb6in.6 [A <= A, B <= B, C <= A, D <= D, E <= E] evalrealshellsortbb3in.9 ~> evalrealshellsortbb5in.14 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb1in.8 ~> evalrealshellsortbb3in.9 [A <= A, B <= B, C <= C, D <= unknown, E <= C] evalrealshellsortbb2in.13 ~> evalrealshellsortbb3in.9 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb4in.11 ~> evalrealshellsortbb2in.13 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb3in.10 ~> evalrealshellsortbb4in.11 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb1in.8 ~> evalrealshellsortbb3in.10 [A <= A, B <= B, C <= C, D <= unknown, E <= C] evalrealshellsortbb2in.13 ~> evalrealshellsortbb3in.10 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb4in.12 ~> evalrealshellsortbb5in.14 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb3in.10 ~> evalrealshellsortbb4in.12 [A <= A, B <= B, C <= C, D <= D, E <= E] + Loop: [0.0.0.0 <= K + E] evalrealshellsortbb3in.10 ~> evalrealshellsortbb4in.11 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb2in.13 ~> evalrealshellsortbb3in.10 [A <= A, B <= B, C <= C, D <= D, E <= E] evalrealshellsortbb4in.11 ~> evalrealshellsortbb2in.13 [A <= A, B <= B, C <= C, D <= D, E <= E] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,0.0,0.0.0,0.0.0.0] evalrealshellsortstart.0 ~> evalrealshellsortentryin.1 [] evalrealshellsortstart.0 ~> evalrealshellsortentryin.2 [] evalrealshellsortstart.0 ~> evalrealshellsortentryin.3 [] evalrealshellsortentryin.1 ~> evalrealshellsortbb8in.5 [K ~=> B] evalrealshellsortentryin.2 ~> evalrealshellsortbb8in.4 [A ~=> B] evalrealshellsortentryin.2 ~> evalrealshellsortbb8in.5 [A ~=> B] evalrealshellsortentryin.3 ~> evalrealshellsortbb8in.5 [A ~=> B] evalrealshellsortbb8in.4 ~> evalrealshellsortbb6in.6 [K ~=> C] evalrealshellsortbb8in.4 ~> evalrealshellsortbb6in.7 [K ~=> C] evalrealshellsortbb8in.5 ~> evalrealshellsortreturnin.16 [] evalrealshellsortbb6in.6 ~> evalrealshellsortbb1in.8 [] evalrealshellsortbb6in.7 ~> evalrealshellsortbb7in.15 [] evalrealshellsortbb1in.8 ~> evalrealshellsortbb3in.9 [C ~=> E,huge ~=> D] evalrealshellsortbb1in.8 ~> evalrealshellsortbb3in.10 [C ~=> E,huge ~=> D] evalrealshellsortbb3in.9 ~> evalrealshellsortbb5in.14 [] evalrealshellsortbb3in.10 ~> evalrealshellsortbb4in.11 [] evalrealshellsortbb3in.10 ~> evalrealshellsortbb4in.12 [] evalrealshellsortbb4in.11 ~> evalrealshellsortbb2in.13 [] evalrealshellsortbb4in.12 ~> evalrealshellsortbb5in.14 [] evalrealshellsortbb2in.13 ~> evalrealshellsortbb3in.9 [] evalrealshellsortbb2in.13 ~> evalrealshellsortbb3in.10 [] evalrealshellsortbb5in.14 ~> evalrealshellsortbb6in.6 [A ~=> C] evalrealshellsortbb5in.14 ~> evalrealshellsortbb6in.7 [A ~=> C] evalrealshellsortbb7in.15 ~> evalrealshellsortbb8in.4 [] evalrealshellsortbb7in.15 ~> evalrealshellsortbb8in.5 [] evalrealshellsortreturnin.16 ~> evalrealshellsortstop.17 [] evalrealshellsortreturnin.16 ~> evalrealshellsortstop.18 [] evalrealshellsortreturnin.16 ~> evalrealshellsortstop.19 [] evalrealshellsortstop.17 ~> exitus616.20 [] evalrealshellsortstop.18 ~> exitus616.20 [] evalrealshellsortstop.19 ~> exitus616.20 [] + Loop: [B ~*> 0.0,K ~*> 0.0] evalrealshellsortbb8in.4 ~> evalrealshellsortbb6in.6 [K ~=> C] evalrealshellsortbb7in.15 ~> evalrealshellsortbb8in.4 [] evalrealshellsortbb6in.7 ~> evalrealshellsortbb7in.15 [] evalrealshellsortbb8in.4 ~> evalrealshellsortbb6in.7 [K ~=> C] evalrealshellsortbb5in.14 ~> evalrealshellsortbb6in.7 [A ~=> C] evalrealshellsortbb3in.9 ~> evalrealshellsortbb5in.14 [] evalrealshellsortbb1in.8 ~> evalrealshellsortbb3in.9 [C ~=> E,huge ~=> D] evalrealshellsortbb6in.6 ~> evalrealshellsortbb1in.8 [] evalrealshellsortbb5in.14 ~> evalrealshellsortbb6in.6 [A ~=> C] evalrealshellsortbb4in.12 ~> evalrealshellsortbb5in.14 [] evalrealshellsortbb3in.10 ~> evalrealshellsortbb4in.12 [] evalrealshellsortbb1in.8 ~> evalrealshellsortbb3in.10 [C ~=> E,huge ~=> D] evalrealshellsortbb2in.13 ~> evalrealshellsortbb3in.10 [] evalrealshellsortbb4in.11 ~> evalrealshellsortbb2in.13 [] evalrealshellsortbb3in.10 ~> evalrealshellsortbb4in.11 [] evalrealshellsortbb2in.13 ~> evalrealshellsortbb3in.9 [] + Loop: [A ~+> 0.0.0,C ~+> 0.0.0] evalrealshellsortbb6in.6 ~> evalrealshellsortbb1in.8 [] evalrealshellsortbb5in.14 ~> evalrealshellsortbb6in.6 [A ~=> C] evalrealshellsortbb3in.9 ~> evalrealshellsortbb5in.14 [] evalrealshellsortbb1in.8 ~> evalrealshellsortbb3in.9 [C ~=> E,huge ~=> D] evalrealshellsortbb2in.13 ~> evalrealshellsortbb3in.9 [] evalrealshellsortbb4in.11 ~> evalrealshellsortbb2in.13 [] evalrealshellsortbb3in.10 ~> evalrealshellsortbb4in.11 [] evalrealshellsortbb1in.8 ~> evalrealshellsortbb3in.10 [C ~=> E,huge ~=> D] evalrealshellsortbb2in.13 ~> evalrealshellsortbb3in.10 [] evalrealshellsortbb4in.12 ~> evalrealshellsortbb5in.14 [] evalrealshellsortbb3in.10 ~> evalrealshellsortbb4in.12 [] + Loop: [E ~+> 0.0.0.0,K ~+> 0.0.0.0] evalrealshellsortbb3in.10 ~> evalrealshellsortbb4in.11 [] evalrealshellsortbb2in.13 ~> evalrealshellsortbb3in.10 [] evalrealshellsortbb4in.11 ~> evalrealshellsortbb2in.13 [] + Applied Processor: Lare + Details: evalrealshellsortstart.0 ~> exitus616.20 [A ~=> B ,A ~=> C ,A ~=> E ,K ~=> B ,K ~=> C ,K ~=> E ,huge ~=> D ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> tick ,A ~*> 0.0 ,A ~*> tick ,K ~*> 0.0 ,K ~*> 0.0.0.0 ,K ~*> tick] + evalrealshellsortbb7in.15> [A ~=> C ,A ~=> E ,K ~=> C ,K ~=> E ,huge ~=> D ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> tick ,A ~*> tick ,B ~*> 0.0 ,B ~*> tick ,K ~*> 0.0 ,K ~*> 0.0.0.0 ,K ~*> tick] + evalrealshellsortbb5in.14> [A ~=> C ,A ~=> E ,C ~=> E ,huge ~=> D ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> tick ,C ~+> 0.0.0 ,C ~+> 0.0.0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0 ,K ~+> tick ,A ~*> tick ,C ~*> tick ,K ~*> tick] + evalrealshellsortbb3in.10> [E ~+> 0.0.0.0 ,E ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0 ,K ~+> tick] evalrealshellsortbb2in.13> [E ~+> 0.0.0.0 ,E ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0 ,K ~+> tick] YES(?,POLY)