YES(?,POLY) * Step 1: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalrealheapsortstart(A,B,C,D) -> evalrealheapsortentryin(A,B,C,D) True (1,1) 1. evalrealheapsortentryin(A,B,C,D) -> evalrealheapsortreturnin(A,B,C,D) [2 >= A] (?,1) 2. evalrealheapsortentryin(A,B,C,D) -> evalrealheapsortbb6in(A,1,C,D) [A >= 3] (?,1) 3. evalrealheapsortreturnin(A,B,C,D) -> evalrealheapsortstop(A,B,C,D) True (?,1) 4. evalrealheapsortbb6in(A,B,C,D) -> evalrealheapsortbb3in(A,B,B,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && A >= 1 + B] (?,1) 5. evalrealheapsortbb3in(A,B,C,D) -> evalrealheapsortbb4in(A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] 6. evalrealheapsortbb3in(A,B,C,D) -> evalrealheapsortbb5in(A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && 0 >= C] 7. evalrealheapsortbb4in(A,B,C,D) -> evalrealheapsortbb5in(A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] 8. evalrealheapsortbb4in(A,B,C,D) -> evalrealheapsortbb2in(A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] 9. evalrealheapsortbb5in(A,B,C,D) -> evalrealheapsortbb6in(A,1 + B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] (?,1) 10. evalrealheapsortbb6in(A,B,C,D) -> evalrealheapsortbb7in(A,B,C,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && B >= A] (?,1) 11. evalrealheapsortbb2in(A,B,C,D) -> evalrealheapsortbb3in(A,B,-1 + E,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && F >= 0 && 1 + C >= 2*F && 2*F >= C && G >= 0 && 1 + C >= 2*G && 2*G >= C && E >= 0 && 1 + C >= 2*E && 2*E >= C] 12. evalrealheapsortbb7in(A,B,C,D) -> evalrealheapsortbb18in(A,0,C,D) [-3 + B >= 0 && -6 + A + B >= 0 && -1*A + B >= 0 && -3 + A >= 0] (?,1) 13. evalrealheapsortbb18in(A,B,C,D) -> evalrealheapsortreturnin(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 1 + B >= A] (?,1) 14. evalrealheapsortbb18in(A,B,C,D) -> evalrealheapsortbb8in(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 2 + B] (?,1) 15. evalrealheapsortbb8in(A,B,C,D) -> evalrealheapsortbb16in(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] (?,1) 16. evalrealheapsortbb16in(A,B,C,D) -> evalrealheapsortbb17in(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 2 + B + 2*C >= A] (?,1) 17. evalrealheapsortbb16in(A,B,C,D) -> evalrealheapsortbb9in(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 3 + B + 2*C] (?,1) 18. evalrealheapsortbb17in(A,B,C,D) -> evalrealheapsortbb18in(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] (?,1) 19. evalrealheapsortbb9in(A,B,C,D) -> evalrealheapsortbb10in(A,B,C,D) [-3 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 4 + B + 2*C] 20. evalrealheapsortbb9in(A,B,C,D) -> evalrealheapsortbb11in(A,B,C,D) [-3 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A = 3 + B + 2*C] 21. evalrealheapsortbb10in(A,B,C,D) -> evalrealheapsortbb12in(A,B,C,D) [-4 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] 22. evalrealheapsortbb10in(A,B,C,D) -> evalrealheapsortbb11in(A,B,C,D) [-4 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] 23. evalrealheapsortbb11in(A,B,C,D) -> evalrealheapsortbb13in(A,B,C,1 + 2*C) [-3 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] 24. evalrealheapsortbb13in(A,B,C,D) -> evalrealheapsortbb16in(A,B,A,D) [-1 + D >= 0 (?,1) && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] 25. evalrealheapsortbb13in(A,B,C,D) -> evalrealheapsortbb14in(A,B,C,D) [-1 + D >= 0 (?,1) && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] 26. evalrealheapsortbb12in(A,B,C,D) -> evalrealheapsortbb13in(A,B,C,2 + 2*C) [-4 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] 27. evalrealheapsortbb14in(A,B,C,D) -> evalrealheapsortbb16in(A,B,D,D) [-1 + D >= 0 (?,1) && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] Signature: {(evalrealheapsortbb10in,4) ;(evalrealheapsortbb11in,4) ;(evalrealheapsortbb12in,4) ;(evalrealheapsortbb13in,4) ;(evalrealheapsortbb14in,4) ;(evalrealheapsortbb16in,4) ;(evalrealheapsortbb17in,4) ;(evalrealheapsortbb18in,4) ;(evalrealheapsortbb2in,4) ;(evalrealheapsortbb3in,4) ;(evalrealheapsortbb4in,4) ;(evalrealheapsortbb5in,4) ;(evalrealheapsortbb6in,4) ;(evalrealheapsortbb7in,4) ;(evalrealheapsortbb8in,4) ;(evalrealheapsortbb9in,4) ;(evalrealheapsortentryin,4) ;(evalrealheapsortreturnin,4) ;(evalrealheapsortstart,4) ;(evalrealheapsortstop,4)} Flow Graph: [0->{1,2},1->{3},2->{4,10},3->{},4->{5,6},5->{7,8},6->{9},7->{9},8->{11},9->{4,10},10->{12},11->{5,6} ,12->{13,14},13->{3},14->{15},15->{16,17},16->{18},17->{19,20},18->{13,14},19->{21,22},20->{23},21->{26} ,22->{23},23->{24,25},24->{16,17},25->{27},26->{24,25},27->{16,17}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,10),(4,6),(12,13),(24,17)] * Step 2: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalrealheapsortstart(A,B,C,D) -> evalrealheapsortentryin(A,B,C,D) True (1,1) 1. evalrealheapsortentryin(A,B,C,D) -> evalrealheapsortreturnin(A,B,C,D) [2 >= A] (?,1) 2. evalrealheapsortentryin(A,B,C,D) -> evalrealheapsortbb6in(A,1,C,D) [A >= 3] (?,1) 3. evalrealheapsortreturnin(A,B,C,D) -> evalrealheapsortstop(A,B,C,D) True (?,1) 4. evalrealheapsortbb6in(A,B,C,D) -> evalrealheapsortbb3in(A,B,B,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && A >= 1 + B] (?,1) 5. evalrealheapsortbb3in(A,B,C,D) -> evalrealheapsortbb4in(A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] 6. evalrealheapsortbb3in(A,B,C,D) -> evalrealheapsortbb5in(A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && 0 >= C] 7. evalrealheapsortbb4in(A,B,C,D) -> evalrealheapsortbb5in(A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] 8. evalrealheapsortbb4in(A,B,C,D) -> evalrealheapsortbb2in(A,B,C,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] 9. evalrealheapsortbb5in(A,B,C,D) -> evalrealheapsortbb6in(A,1 + B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] (?,1) 10. evalrealheapsortbb6in(A,B,C,D) -> evalrealheapsortbb7in(A,B,C,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && B >= A] (?,1) 11. evalrealheapsortbb2in(A,B,C,D) -> evalrealheapsortbb3in(A,B,-1 + E,D) [B + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && F >= 0 && 1 + C >= 2*F && 2*F >= C && G >= 0 && 1 + C >= 2*G && 2*G >= C && E >= 0 && 1 + C >= 2*E && 2*E >= C] 12. evalrealheapsortbb7in(A,B,C,D) -> evalrealheapsortbb18in(A,0,C,D) [-3 + B >= 0 && -6 + A + B >= 0 && -1*A + B >= 0 && -3 + A >= 0] (?,1) 13. evalrealheapsortbb18in(A,B,C,D) -> evalrealheapsortreturnin(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 1 + B >= A] (?,1) 14. evalrealheapsortbb18in(A,B,C,D) -> evalrealheapsortbb8in(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 2 + B] (?,1) 15. evalrealheapsortbb8in(A,B,C,D) -> evalrealheapsortbb16in(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] (?,1) 16. evalrealheapsortbb16in(A,B,C,D) -> evalrealheapsortbb17in(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 2 + B + 2*C >= A] (?,1) 17. evalrealheapsortbb16in(A,B,C,D) -> evalrealheapsortbb9in(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 3 + B + 2*C] (?,1) 18. evalrealheapsortbb17in(A,B,C,D) -> evalrealheapsortbb18in(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] (?,1) 19. evalrealheapsortbb9in(A,B,C,D) -> evalrealheapsortbb10in(A,B,C,D) [-3 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 4 + B + 2*C] 20. evalrealheapsortbb9in(A,B,C,D) -> evalrealheapsortbb11in(A,B,C,D) [-3 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A = 3 + B + 2*C] 21. evalrealheapsortbb10in(A,B,C,D) -> evalrealheapsortbb12in(A,B,C,D) [-4 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] 22. evalrealheapsortbb10in(A,B,C,D) -> evalrealheapsortbb11in(A,B,C,D) [-4 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] 23. evalrealheapsortbb11in(A,B,C,D) -> evalrealheapsortbb13in(A,B,C,1 + 2*C) [-3 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] 24. evalrealheapsortbb13in(A,B,C,D) -> evalrealheapsortbb16in(A,B,A,D) [-1 + D >= 0 (?,1) && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] 25. evalrealheapsortbb13in(A,B,C,D) -> evalrealheapsortbb14in(A,B,C,D) [-1 + D >= 0 (?,1) && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] 26. evalrealheapsortbb12in(A,B,C,D) -> evalrealheapsortbb13in(A,B,C,2 + 2*C) [-4 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] 27. evalrealheapsortbb14in(A,B,C,D) -> evalrealheapsortbb16in(A,B,D,D) [-1 + D >= 0 (?,1) && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] Signature: {(evalrealheapsortbb10in,4) ;(evalrealheapsortbb11in,4) ;(evalrealheapsortbb12in,4) ;(evalrealheapsortbb13in,4) ;(evalrealheapsortbb14in,4) ;(evalrealheapsortbb16in,4) ;(evalrealheapsortbb17in,4) ;(evalrealheapsortbb18in,4) ;(evalrealheapsortbb2in,4) ;(evalrealheapsortbb3in,4) ;(evalrealheapsortbb4in,4) ;(evalrealheapsortbb5in,4) ;(evalrealheapsortbb6in,4) ;(evalrealheapsortbb7in,4) ;(evalrealheapsortbb8in,4) ;(evalrealheapsortbb9in,4) ;(evalrealheapsortentryin,4) ;(evalrealheapsortreturnin,4) ;(evalrealheapsortstart,4) ;(evalrealheapsortstop,4)} Flow Graph: [0->{1,2},1->{3},2->{4},3->{},4->{5},5->{7,8},6->{9},7->{9},8->{11},9->{4,10},10->{12},11->{5,6},12->{14} ,13->{3},14->{15},15->{16,17},16->{18},17->{19,20},18->{13,14},19->{21,22},20->{23},21->{26},22->{23} ,23->{24,25},24->{16},25->{27},26->{24,25},27->{16,17}] + Applied Processor: FromIts + Details: () * Step 3: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: evalrealheapsortstart(A,B,C,D) -> evalrealheapsortentryin(A,B,C,D) True evalrealheapsortentryin(A,B,C,D) -> evalrealheapsortreturnin(A,B,C,D) [2 >= A] evalrealheapsortentryin(A,B,C,D) -> evalrealheapsortbb6in(A,1,C,D) [A >= 3] evalrealheapsortreturnin(A,B,C,D) -> evalrealheapsortstop(A,B,C,D) True evalrealheapsortbb6in(A,B,C,D) -> evalrealheapsortbb3in(A,B,B,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && A >= 1 + B] evalrealheapsortbb3in(A,B,C,D) -> evalrealheapsortbb4in(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] evalrealheapsortbb3in(A,B,C,D) -> evalrealheapsortbb5in(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && 0 >= C] evalrealheapsortbb4in(A,B,C,D) -> evalrealheapsortbb5in(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb4in(A,B,C,D) -> evalrealheapsortbb2in(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb5in(A,B,C,D) -> evalrealheapsortbb6in(A,1 + B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb6in(A,B,C,D) -> evalrealheapsortbb7in(A,B,C,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && B >= A] evalrealheapsortbb2in(A,B,C,D) -> evalrealheapsortbb3in(A,B,-1 + E,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && F >= 0 && 1 + C >= 2*F && 2*F >= C && G >= 0 && 1 + C >= 2*G && 2*G >= C && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb7in(A,B,C,D) -> evalrealheapsortbb18in(A,0,C,D) [-3 + B >= 0 && -6 + A + B >= 0 && -1*A + B >= 0 && -3 + A >= 0] evalrealheapsortbb18in(A,B,C,D) -> evalrealheapsortreturnin(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 1 + B >= A] evalrealheapsortbb18in(A,B,C,D) -> evalrealheapsortbb8in(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 2 + B] evalrealheapsortbb8in(A,B,C,D) -> evalrealheapsortbb16in(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb16in(A,B,C,D) -> evalrealheapsortbb17in(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 2 + B + 2*C >= A] evalrealheapsortbb16in(A,B,C,D) -> evalrealheapsortbb9in(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 3 + B + 2*C] evalrealheapsortbb17in(A,B,C,D) -> evalrealheapsortbb18in(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb9in(A,B,C,D) -> evalrealheapsortbb10in(A,B,C,D) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 4 + B + 2*C] evalrealheapsortbb9in(A,B,C,D) -> evalrealheapsortbb11in(A,B,C,D) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A = 3 + B + 2*C] evalrealheapsortbb10in(A,B,C,D) -> evalrealheapsortbb12in(A,B,C,D) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb10in(A,B,C,D) -> evalrealheapsortbb11in(A,B,C,D) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb11in(A,B,C,D) -> evalrealheapsortbb13in(A,B,C,1 + 2*C) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb13in(A,B,C,D) -> evalrealheapsortbb16in(A,B,A,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb13in(A,B,C,D) -> evalrealheapsortbb14in(A,B,C,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb12in(A,B,C,D) -> evalrealheapsortbb13in(A,B,C,2 + 2*C) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb14in(A,B,C,D) -> evalrealheapsortbb16in(A,B,D,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] Signature: {(evalrealheapsortbb10in,4) ;(evalrealheapsortbb11in,4) ;(evalrealheapsortbb12in,4) ;(evalrealheapsortbb13in,4) ;(evalrealheapsortbb14in,4) ;(evalrealheapsortbb16in,4) ;(evalrealheapsortbb17in,4) ;(evalrealheapsortbb18in,4) ;(evalrealheapsortbb2in,4) ;(evalrealheapsortbb3in,4) ;(evalrealheapsortbb4in,4) ;(evalrealheapsortbb5in,4) ;(evalrealheapsortbb6in,4) ;(evalrealheapsortbb7in,4) ;(evalrealheapsortbb8in,4) ;(evalrealheapsortbb9in,4) ;(evalrealheapsortentryin,4) ;(evalrealheapsortreturnin,4) ;(evalrealheapsortstart,4) ;(evalrealheapsortstop,4)} Rule Graph: [0->{1,2},1->{3},2->{4},3->{},4->{5},5->{7,8},6->{9},7->{9},8->{11},9->{4,10},10->{12},11->{5,6},12->{14} ,13->{3},14->{15},15->{16,17},16->{18},17->{19,20},18->{13,14},19->{21,22},20->{23},21->{26},22->{23} ,23->{24,25},24->{16},25->{27},26->{24,25},27->{16,17}] + Applied Processor: AddSinks + Details: () * Step 4: Unfold WORST_CASE(?,POLY) + Considered Problem: Rules: evalrealheapsortstart(A,B,C,D) -> evalrealheapsortentryin(A,B,C,D) True evalrealheapsortentryin(A,B,C,D) -> evalrealheapsortreturnin(A,B,C,D) [2 >= A] evalrealheapsortentryin(A,B,C,D) -> evalrealheapsortbb6in(A,1,C,D) [A >= 3] evalrealheapsortreturnin(A,B,C,D) -> evalrealheapsortstop(A,B,C,D) True evalrealheapsortbb6in(A,B,C,D) -> evalrealheapsortbb3in(A,B,B,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && A >= 1 + B] evalrealheapsortbb3in(A,B,C,D) -> evalrealheapsortbb4in(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] evalrealheapsortbb3in(A,B,C,D) -> evalrealheapsortbb5in(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && 0 >= C] evalrealheapsortbb4in(A,B,C,D) -> evalrealheapsortbb5in(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb4in(A,B,C,D) -> evalrealheapsortbb2in(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb5in(A,B,C,D) -> evalrealheapsortbb6in(A,1 + B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb6in(A,B,C,D) -> evalrealheapsortbb7in(A,B,C,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && B >= A] evalrealheapsortbb2in(A,B,C,D) -> evalrealheapsortbb3in(A,B,-1 + E,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && F >= 0 && 1 + C >= 2*F && 2*F >= C && G >= 0 && 1 + C >= 2*G && 2*G >= C && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb7in(A,B,C,D) -> evalrealheapsortbb18in(A,0,C,D) [-3 + B >= 0 && -6 + A + B >= 0 && -1*A + B >= 0 && -3 + A >= 0] evalrealheapsortbb18in(A,B,C,D) -> evalrealheapsortreturnin(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 1 + B >= A] evalrealheapsortbb18in(A,B,C,D) -> evalrealheapsortbb8in(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 2 + B] evalrealheapsortbb8in(A,B,C,D) -> evalrealheapsortbb16in(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb16in(A,B,C,D) -> evalrealheapsortbb17in(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 2 + B + 2*C >= A] evalrealheapsortbb16in(A,B,C,D) -> evalrealheapsortbb9in(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 3 + B + 2*C] evalrealheapsortbb17in(A,B,C,D) -> evalrealheapsortbb18in(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb9in(A,B,C,D) -> evalrealheapsortbb10in(A,B,C,D) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 4 + B + 2*C] evalrealheapsortbb9in(A,B,C,D) -> evalrealheapsortbb11in(A,B,C,D) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A = 3 + B + 2*C] evalrealheapsortbb10in(A,B,C,D) -> evalrealheapsortbb12in(A,B,C,D) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb10in(A,B,C,D) -> evalrealheapsortbb11in(A,B,C,D) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb11in(A,B,C,D) -> evalrealheapsortbb13in(A,B,C,1 + 2*C) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb13in(A,B,C,D) -> evalrealheapsortbb16in(A,B,A,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb13in(A,B,C,D) -> evalrealheapsortbb14in(A,B,C,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb12in(A,B,C,D) -> evalrealheapsortbb13in(A,B,C,2 + 2*C) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb14in(A,B,C,D) -> evalrealheapsortbb16in(A,B,D,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortstop(A,B,C,D) -> exitus616(A,B,C,D) True evalrealheapsortstop(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(evalrealheapsortbb10in,4) ;(evalrealheapsortbb11in,4) ;(evalrealheapsortbb12in,4) ;(evalrealheapsortbb13in,4) ;(evalrealheapsortbb14in,4) ;(evalrealheapsortbb16in,4) ;(evalrealheapsortbb17in,4) ;(evalrealheapsortbb18in,4) ;(evalrealheapsortbb2in,4) ;(evalrealheapsortbb3in,4) ;(evalrealheapsortbb4in,4) ;(evalrealheapsortbb5in,4) ;(evalrealheapsortbb6in,4) ;(evalrealheapsortbb7in,4) ;(evalrealheapsortbb8in,4) ;(evalrealheapsortbb9in,4) ;(evalrealheapsortentryin,4) ;(evalrealheapsortreturnin,4) ;(evalrealheapsortstart,4) ;(evalrealheapsortstop,4) ;(exitus616,4)} Rule Graph: [0->{1,2},1->{3},2->{4},3->{28,29},4->{5},5->{7,8},6->{9},7->{9},8->{11},9->{4,10},10->{12},11->{5,6} ,12->{14},13->{3},14->{15},15->{16,17},16->{18},17->{19,20},18->{13,14},19->{21,22},20->{23},21->{26} ,22->{23},23->{24,25},24->{16},25->{27},26->{24,25},27->{16,17}] + Applied Processor: Unfold + Details: () * Step 5: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: evalrealheapsortstart.0(A,B,C,D) -> evalrealheapsortentryin.1(A,B,C,D) True evalrealheapsortstart.0(A,B,C,D) -> evalrealheapsortentryin.2(A,B,C,D) True evalrealheapsortentryin.1(A,B,C,D) -> evalrealheapsortreturnin.3(A,B,C,D) [2 >= A] evalrealheapsortentryin.2(A,B,C,D) -> evalrealheapsortbb6in.4(A,1,C,D) [A >= 3] evalrealheapsortreturnin.3(A,B,C,D) -> evalrealheapsortstop.28(A,B,C,D) True evalrealheapsortreturnin.3(A,B,C,D) -> evalrealheapsortstop.29(A,B,C,D) True evalrealheapsortbb6in.4(A,B,C,D) -> evalrealheapsortbb3in.5(A,B,B,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && A >= 1 + B] evalrealheapsortbb3in.5(A,B,C,D) -> evalrealheapsortbb4in.7(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] evalrealheapsortbb3in.5(A,B,C,D) -> evalrealheapsortbb4in.8(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] evalrealheapsortbb3in.6(A,B,C,D) -> evalrealheapsortbb5in.9(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && 0 >= C] evalrealheapsortbb4in.7(A,B,C,D) -> evalrealheapsortbb5in.9(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb4in.8(A,B,C,D) -> evalrealheapsortbb2in.11(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb5in.9(A,B,C,D) -> evalrealheapsortbb6in.4(A,1 + B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb5in.9(A,B,C,D) -> evalrealheapsortbb6in.10(A,1 + B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb6in.10(A,B,C,D) -> evalrealheapsortbb7in.12(A,B,C,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && B >= A] evalrealheapsortbb2in.11(A,B,C,D) -> evalrealheapsortbb3in.5(A,B,-1 + E,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && F >= 0 && 1 + C >= 2*F && 2*F >= C && G >= 0 && 1 + C >= 2*G && 2*G >= C && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb2in.11(A,B,C,D) -> evalrealheapsortbb3in.6(A,B,-1 + E,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && F >= 0 && 1 + C >= 2*F && 2*F >= C && G >= 0 && 1 + C >= 2*G && 2*G >= C && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb7in.12(A,B,C,D) -> evalrealheapsortbb18in.14(A,0,C,D) [-3 + B >= 0 && -6 + A + B >= 0 && -1*A + B >= 0 && -3 + A >= 0] evalrealheapsortbb18in.13(A,B,C,D) -> evalrealheapsortreturnin.3(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 1 + B >= A] evalrealheapsortbb18in.14(A,B,C,D) -> evalrealheapsortbb8in.15(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 2 + B] evalrealheapsortbb8in.15(A,B,C,D) -> evalrealheapsortbb16in.16(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb8in.15(A,B,C,D) -> evalrealheapsortbb16in.17(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb16in.16(A,B,C,D) -> evalrealheapsortbb17in.18(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 2 + B + 2*C >= A] evalrealheapsortbb16in.17(A,B,C,D) -> evalrealheapsortbb9in.19(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 3 + B + 2*C] evalrealheapsortbb16in.17(A,B,C,D) -> evalrealheapsortbb9in.20(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 3 + B + 2*C] evalrealheapsortbb17in.18(A,B,C,D) -> evalrealheapsortbb18in.13(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb17in.18(A,B,C,D) -> evalrealheapsortbb18in.14(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb9in.19(A,B,C,D) -> evalrealheapsortbb10in.21(A,B,C,D) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 4 + B + 2*C] evalrealheapsortbb9in.19(A,B,C,D) -> evalrealheapsortbb10in.22(A,B,C,D) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 4 + B + 2*C] evalrealheapsortbb9in.20(A,B,C,D) -> evalrealheapsortbb11in.23(A,B,C,D) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A = 3 + B + 2*C] evalrealheapsortbb10in.21(A,B,C,D) -> evalrealheapsortbb12in.26(A,B,C,D) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb10in.22(A,B,C,D) -> evalrealheapsortbb11in.23(A,B,C,D) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb11in.23(A,B,C,D) -> evalrealheapsortbb13in.24(A,B,C,1 + 2*C) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb11in.23(A,B,C,D) -> evalrealheapsortbb13in.25(A,B,C,1 + 2*C) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb13in.24(A,B,C,D) -> evalrealheapsortbb16in.16(A,B,A,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb13in.25(A,B,C,D) -> evalrealheapsortbb14in.27(A,B,C,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb12in.26(A,B,C,D) -> evalrealheapsortbb13in.24(A,B,C,2 + 2*C) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb12in.26(A,B,C,D) -> evalrealheapsortbb13in.25(A,B,C,2 + 2*C) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb14in.27(A,B,C,D) -> evalrealheapsortbb16in.16(A,B,D,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb14in.27(A,B,C,D) -> evalrealheapsortbb16in.17(A,B,D,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortstop.28(A,B,C,D) -> exitus616.30(A,B,C,D) True evalrealheapsortstop.29(A,B,C,D) -> exitus616.30(A,B,C,D) True Signature: {(evalrealheapsortbb10in.21,4) ;(evalrealheapsortbb10in.22,4) ;(evalrealheapsortbb11in.23,4) ;(evalrealheapsortbb12in.26,4) ;(evalrealheapsortbb13in.24,4) ;(evalrealheapsortbb13in.25,4) ;(evalrealheapsortbb14in.27,4) ;(evalrealheapsortbb16in.16,4) ;(evalrealheapsortbb16in.17,4) ;(evalrealheapsortbb17in.18,4) ;(evalrealheapsortbb18in.13,4) ;(evalrealheapsortbb18in.14,4) ;(evalrealheapsortbb2in.11,4) ;(evalrealheapsortbb3in.5,4) ;(evalrealheapsortbb3in.6,4) ;(evalrealheapsortbb4in.7,4) ;(evalrealheapsortbb4in.8,4) ;(evalrealheapsortbb5in.9,4) ;(evalrealheapsortbb6in.10,4) ;(evalrealheapsortbb6in.4,4) ;(evalrealheapsortbb7in.12,4) ;(evalrealheapsortbb8in.15,4) ;(evalrealheapsortbb9in.19,4) ;(evalrealheapsortbb9in.20,4) ;(evalrealheapsortentryin.1,4) ;(evalrealheapsortentryin.2,4) ;(evalrealheapsortreturnin.3,4) ;(evalrealheapsortstart.0,4) ;(evalrealheapsortstop.28,4) ;(evalrealheapsortstop.29,4) ;(exitus616.30,4)} Rule Graph: [0->{2},1->{3},2->{4,5},3->{6},4->{40},5->{41},6->{7,8},7->{10},8->{11},9->{12,13},10->{12,13},11->{15,16} ,12->{6},13->{14},14->{17},15->{7,8},16->{9},17->{19},18->{4,5},19->{20,21},20->{22},21->{23,24},22->{25,26} ,23->{27,28},24->{29},25->{18},26->{19},27->{30},28->{31},29->{32,33},30->{36,37},31->{32,33},32->{34} ,33->{35},34->{22},35->{38,39},36->{34},37->{35},38->{22},39->{23,24},40->{},41->{}] + 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,31,32,33,34,35,36,37,38,39,40,41] | +- p:[6,12,9,16,11,8,15,10,7] c: [6,7,9,10,12,16] | | | `- p:[8,15,11] c: [8,11,15] | `- p:[19,26,22,20,34,32,29,24,21,39,35,33,31,28,23,37,30,27,36,38] c: [19,20,21,22,26,32,34,36,38] | `- p:[23,39,35,33,29,24,31,28,37,30,27] c: [23,24,27,28,29,30,31,33,35,37,39] * Step 6: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: evalrealheapsortstart.0(A,B,C,D) -> evalrealheapsortentryin.1(A,B,C,D) True evalrealheapsortstart.0(A,B,C,D) -> evalrealheapsortentryin.2(A,B,C,D) True evalrealheapsortentryin.1(A,B,C,D) -> evalrealheapsortreturnin.3(A,B,C,D) [2 >= A] evalrealheapsortentryin.2(A,B,C,D) -> evalrealheapsortbb6in.4(A,1,C,D) [A >= 3] evalrealheapsortreturnin.3(A,B,C,D) -> evalrealheapsortstop.28(A,B,C,D) True evalrealheapsortreturnin.3(A,B,C,D) -> evalrealheapsortstop.29(A,B,C,D) True evalrealheapsortbb6in.4(A,B,C,D) -> evalrealheapsortbb3in.5(A,B,B,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && A >= 1 + B] evalrealheapsortbb3in.5(A,B,C,D) -> evalrealheapsortbb4in.7(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] evalrealheapsortbb3in.5(A,B,C,D) -> evalrealheapsortbb4in.8(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 1] evalrealheapsortbb3in.6(A,B,C,D) -> evalrealheapsortbb5in.9(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && 0 >= C] evalrealheapsortbb4in.7(A,B,C,D) -> evalrealheapsortbb5in.9(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb4in.8(A,B,C,D) -> evalrealheapsortbb2in.11(A,B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb5in.9(A,B,C,D) -> evalrealheapsortbb6in.4(A,1 + B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb5in.9(A,B,C,D) -> evalrealheapsortbb6in.10(A,1 + B,C,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb6in.10(A,B,C,D) -> evalrealheapsortbb7in.12(A,B,C,D) [-1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && B >= A] evalrealheapsortbb2in.11(A,B,C,D) -> evalrealheapsortbb3in.5(A,B,-1 + E,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && F >= 0 && 1 + C >= 2*F && 2*F >= C && G >= 0 && 1 + C >= 2*G && 2*G >= C && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb2in.11(A,B,C,D) -> evalrealheapsortbb3in.6(A,B,-1 + E,D) [B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -4 + A + C >= 0 && -1 + A + -1*B >= 0 && -1 + B >= 0 && -4 + A + B >= 0 && -3 + A >= 0 && C >= 0 && F >= 0 && 1 + C >= 2*F && 2*F >= C && G >= 0 && 1 + C >= 2*G && 2*G >= C && E >= 0 && 1 + C >= 2*E && 2*E >= C] evalrealheapsortbb7in.12(A,B,C,D) -> evalrealheapsortbb18in.14(A,0,C,D) [-3 + B >= 0 && -6 + A + B >= 0 && -1*A + B >= 0 && -3 + A >= 0] evalrealheapsortbb18in.13(A,B,C,D) -> evalrealheapsortreturnin.3(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 1 + B >= A] evalrealheapsortbb18in.14(A,B,C,D) -> evalrealheapsortbb8in.15(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 2 + B] evalrealheapsortbb8in.15(A,B,C,D) -> evalrealheapsortbb16in.16(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb8in.15(A,B,C,D) -> evalrealheapsortbb16in.17(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb16in.16(A,B,C,D) -> evalrealheapsortbb17in.18(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 2 + B + 2*C >= A] evalrealheapsortbb16in.17(A,B,C,D) -> evalrealheapsortbb9in.19(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 3 + B + 2*C] evalrealheapsortbb16in.17(A,B,C,D) -> evalrealheapsortbb9in.20(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 3 + B + 2*C] evalrealheapsortbb17in.18(A,B,C,D) -> evalrealheapsortbb18in.13(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb17in.18(A,B,C,D) -> evalrealheapsortbb18in.14(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb9in.19(A,B,C,D) -> evalrealheapsortbb10in.21(A,B,C,D) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 4 + B + 2*C] evalrealheapsortbb9in.19(A,B,C,D) -> evalrealheapsortbb10in.22(A,B,C,D) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 4 + B + 2*C] evalrealheapsortbb9in.20(A,B,C,D) -> evalrealheapsortbb11in.23(A,B,C,D) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A = 3 + B + 2*C] evalrealheapsortbb10in.21(A,B,C,D) -> evalrealheapsortbb12in.26(A,B,C,D) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb10in.22(A,B,C,D) -> evalrealheapsortbb11in.23(A,B,C,D) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb11in.23(A,B,C,D) -> evalrealheapsortbb13in.24(A,B,C,1 + 2*C) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb11in.23(A,B,C,D) -> evalrealheapsortbb13in.25(A,B,C,1 + 2*C) [-3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb13in.24(A,B,C,D) -> evalrealheapsortbb16in.16(A,B,A,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb13in.25(A,B,C,D) -> evalrealheapsortbb14in.27(A,B,C,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb12in.26(A,B,C,D) -> evalrealheapsortbb13in.24(A,B,C,2 + 2*C) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb12in.26(A,B,C,D) -> evalrealheapsortbb13in.25(A,B,C,2 + 2*C) [-4 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] evalrealheapsortbb14in.27(A,B,C,D) -> evalrealheapsortbb16in.16(A,B,D,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortbb14in.27(A,B,C,D) -> evalrealheapsortbb16in.17(A,B,D,D) [-1 + D >= 0 && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortstop.28(A,B,C,D) -> exitus616.30(A,B,C,D) True evalrealheapsortstop.29(A,B,C,D) -> exitus616.30(A,B,C,D) True Signature: {(evalrealheapsortbb10in.21,4) ;(evalrealheapsortbb10in.22,4) ;(evalrealheapsortbb11in.23,4) ;(evalrealheapsortbb12in.26,4) ;(evalrealheapsortbb13in.24,4) ;(evalrealheapsortbb13in.25,4) ;(evalrealheapsortbb14in.27,4) ;(evalrealheapsortbb16in.16,4) ;(evalrealheapsortbb16in.17,4) ;(evalrealheapsortbb17in.18,4) ;(evalrealheapsortbb18in.13,4) ;(evalrealheapsortbb18in.14,4) ;(evalrealheapsortbb2in.11,4) ;(evalrealheapsortbb3in.5,4) ;(evalrealheapsortbb3in.6,4) ;(evalrealheapsortbb4in.7,4) ;(evalrealheapsortbb4in.8,4) ;(evalrealheapsortbb5in.9,4) ;(evalrealheapsortbb6in.10,4) ;(evalrealheapsortbb6in.4,4) ;(evalrealheapsortbb7in.12,4) ;(evalrealheapsortbb8in.15,4) ;(evalrealheapsortbb9in.19,4) ;(evalrealheapsortbb9in.20,4) ;(evalrealheapsortentryin.1,4) ;(evalrealheapsortentryin.2,4) ;(evalrealheapsortreturnin.3,4) ;(evalrealheapsortstart.0,4) ;(evalrealheapsortstop.28,4) ;(evalrealheapsortstop.29,4) ;(exitus616.30,4)} Rule Graph: [0->{2},1->{3},2->{4,5},3->{6},4->{40},5->{41},6->{7,8},7->{10},8->{11},9->{12,13},10->{12,13},11->{15,16} ,12->{6},13->{14},14->{17},15->{7,8},16->{9},17->{19},18->{4,5},19->{20,21},20->{22},21->{23,24},22->{25,26} ,23->{27,28},24->{29},25->{18},26->{19},27->{30},28->{31},29->{32,33},30->{36,37},31->{32,33},32->{34} ,33->{35},34->{22},35->{38,39},36->{34},37->{35},38->{22},39->{23,24},40->{},41->{}] ,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,31,32,33,34,35,36,37,38,39,40,41] | +- p:[6,12,9,16,11,8,15,10,7] c: [6,7,9,10,12,16] | | | `- p:[8,15,11] c: [8,11,15] | `- p:[19,26,22,20,34,32,29,24,21,39,35,33,31,28,23,37,30,27,36,38] c: [19,20,21,22,26,32,34,36,38] | `- p:[23,39,35,33,29,24,31,28,37,30,27] c: [23,24,27,28,29,30,31,33,35,37,39]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,0.0,0.0.0,0.1,0.1.0] evalrealheapsortstart.0 ~> evalrealheapsortentryin.1 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstart.0 ~> evalrealheapsortentryin.2 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortentryin.1 ~> evalrealheapsortreturnin.3 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortentryin.2 ~> evalrealheapsortbb6in.4 [A <= A, B <= K, C <= C, D <= D] evalrealheapsortreturnin.3 ~> evalrealheapsortstop.28 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortreturnin.3 ~> evalrealheapsortstop.29 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb6in.4 ~> evalrealheapsortbb3in.5 [A <= A, B <= B, C <= B, D <= D] evalrealheapsortbb3in.5 ~> evalrealheapsortbb4in.7 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb3in.5 ~> evalrealheapsortbb4in.8 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb3in.6 ~> evalrealheapsortbb5in.9 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb4in.7 ~> evalrealheapsortbb5in.9 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb4in.8 ~> evalrealheapsortbb2in.11 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb5in.9 ~> evalrealheapsortbb6in.4 [A <= A, B <= A, C <= C, D <= D] evalrealheapsortbb5in.9 ~> evalrealheapsortbb6in.10 [A <= A, B <= A, C <= C, D <= D] evalrealheapsortbb6in.10 ~> evalrealheapsortbb7in.12 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb2in.11 ~> evalrealheapsortbb3in.5 [A <= A, B <= B, C <= A, D <= D] evalrealheapsortbb2in.11 ~> evalrealheapsortbb3in.6 [A <= A, B <= B, C <= A, D <= D] evalrealheapsortbb7in.12 ~> evalrealheapsortbb18in.14 [A <= A, B <= 0*K, C <= C, D <= D] evalrealheapsortbb18in.13 ~> evalrealheapsortreturnin.3 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb18in.14 ~> evalrealheapsortbb8in.15 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb8in.15 ~> evalrealheapsortbb16in.16 [A <= A, B <= B, C <= 0*K, D <= D] evalrealheapsortbb8in.15 ~> evalrealheapsortbb16in.17 [A <= A, B <= B, C <= 0*K, D <= D] evalrealheapsortbb16in.16 ~> evalrealheapsortbb17in.18 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.19 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.20 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb17in.18 ~> evalrealheapsortbb18in.13 [A <= A, B <= A + B, C <= C, D <= D] evalrealheapsortbb17in.18 ~> evalrealheapsortbb18in.14 [A <= A, B <= A + B, C <= C, D <= D] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.21 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.22 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb9in.20 ~> evalrealheapsortbb11in.23 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb10in.21 ~> evalrealheapsortbb12in.26 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb10in.22 ~> evalrealheapsortbb11in.23 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb11in.23 ~> evalrealheapsortbb13in.24 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortbb11in.23 ~> evalrealheapsortbb13in.25 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortbb13in.24 ~> evalrealheapsortbb16in.16 [A <= A, B <= B, C <= A, D <= D] evalrealheapsortbb13in.25 ~> evalrealheapsortbb14in.27 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb12in.26 ~> evalrealheapsortbb13in.24 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortbb12in.26 ~> evalrealheapsortbb13in.25 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortbb14in.27 ~> evalrealheapsortbb16in.16 [A <= A, B <= B, C <= D, D <= D] evalrealheapsortbb14in.27 ~> evalrealheapsortbb16in.17 [A <= A, B <= B, C <= D, D <= D] evalrealheapsortstop.28 ~> exitus616.30 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstop.29 ~> exitus616.30 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= K + A + B] evalrealheapsortbb6in.4 ~> evalrealheapsortbb3in.5 [A <= A, B <= B, C <= B, D <= D] evalrealheapsortbb5in.9 ~> evalrealheapsortbb6in.4 [A <= A, B <= A, C <= C, D <= D] evalrealheapsortbb3in.6 ~> evalrealheapsortbb5in.9 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb2in.11 ~> evalrealheapsortbb3in.6 [A <= A, B <= B, C <= A, D <= D] evalrealheapsortbb4in.8 ~> evalrealheapsortbb2in.11 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb3in.5 ~> evalrealheapsortbb4in.8 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb2in.11 ~> evalrealheapsortbb3in.5 [A <= A, B <= B, C <= A, D <= D] evalrealheapsortbb4in.7 ~> evalrealheapsortbb5in.9 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb3in.5 ~> evalrealheapsortbb4in.7 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0.0 <= K + 4*C] evalrealheapsortbb3in.5 ~> evalrealheapsortbb4in.8 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb2in.11 ~> evalrealheapsortbb3in.5 [A <= A, B <= B, C <= A, D <= D] evalrealheapsortbb4in.8 ~> evalrealheapsortbb2in.11 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.1 <= K + A + B] evalrealheapsortbb18in.14 ~> evalrealheapsortbb8in.15 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb17in.18 ~> evalrealheapsortbb18in.14 [A <= A, B <= A + B, C <= C, D <= D] evalrealheapsortbb16in.16 ~> evalrealheapsortbb17in.18 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb8in.15 ~> evalrealheapsortbb16in.16 [A <= A, B <= B, C <= 0*K, D <= D] evalrealheapsortbb13in.24 ~> evalrealheapsortbb16in.16 [A <= A, B <= B, C <= A, D <= D] evalrealheapsortbb11in.23 ~> evalrealheapsortbb13in.24 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortbb9in.20 ~> evalrealheapsortbb11in.23 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.20 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb8in.15 ~> evalrealheapsortbb16in.17 [A <= A, B <= B, C <= 0*K, D <= D] evalrealheapsortbb14in.27 ~> evalrealheapsortbb16in.17 [A <= A, B <= B, C <= D, D <= D] evalrealheapsortbb13in.25 ~> evalrealheapsortbb14in.27 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb11in.23 ~> evalrealheapsortbb13in.25 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortbb10in.22 ~> evalrealheapsortbb11in.23 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.22 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.19 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb12in.26 ~> evalrealheapsortbb13in.25 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortbb10in.21 ~> evalrealheapsortbb12in.26 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.21 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb12in.26 ~> evalrealheapsortbb13in.24 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortbb14in.27 ~> evalrealheapsortbb16in.16 [A <= A, B <= B, C <= D, D <= D] + Loop: [0.1.0 <= 3*K + A + C] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.19 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb14in.27 ~> evalrealheapsortbb16in.17 [A <= A, B <= B, C <= D, D <= D] evalrealheapsortbb13in.25 ~> evalrealheapsortbb14in.27 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb11in.23 ~> evalrealheapsortbb13in.25 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortbb9in.20 ~> evalrealheapsortbb11in.23 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.20 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb10in.22 ~> evalrealheapsortbb11in.23 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.22 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb12in.26 ~> evalrealheapsortbb13in.25 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortbb10in.21 ~> evalrealheapsortbb12in.26 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.21 [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,0.1,0.1.0] evalrealheapsortstart.0 ~> evalrealheapsortentryin.1 [] evalrealheapsortstart.0 ~> evalrealheapsortentryin.2 [] evalrealheapsortentryin.1 ~> evalrealheapsortreturnin.3 [] evalrealheapsortentryin.2 ~> evalrealheapsortbb6in.4 [K ~=> B] evalrealheapsortreturnin.3 ~> evalrealheapsortstop.28 [] evalrealheapsortreturnin.3 ~> evalrealheapsortstop.29 [] evalrealheapsortbb6in.4 ~> evalrealheapsortbb3in.5 [B ~=> C] evalrealheapsortbb3in.5 ~> evalrealheapsortbb4in.7 [] evalrealheapsortbb3in.5 ~> evalrealheapsortbb4in.8 [] evalrealheapsortbb3in.6 ~> evalrealheapsortbb5in.9 [] evalrealheapsortbb4in.7 ~> evalrealheapsortbb5in.9 [] evalrealheapsortbb4in.8 ~> evalrealheapsortbb2in.11 [] evalrealheapsortbb5in.9 ~> evalrealheapsortbb6in.4 [A ~=> B] evalrealheapsortbb5in.9 ~> evalrealheapsortbb6in.10 [A ~=> B] evalrealheapsortbb6in.10 ~> evalrealheapsortbb7in.12 [] evalrealheapsortbb2in.11 ~> evalrealheapsortbb3in.5 [A ~=> C] evalrealheapsortbb2in.11 ~> evalrealheapsortbb3in.6 [A ~=> C] evalrealheapsortbb7in.12 ~> evalrealheapsortbb18in.14 [K ~=> B] evalrealheapsortbb18in.13 ~> evalrealheapsortreturnin.3 [] evalrealheapsortbb18in.14 ~> evalrealheapsortbb8in.15 [] evalrealheapsortbb8in.15 ~> evalrealheapsortbb16in.16 [K ~=> C] evalrealheapsortbb8in.15 ~> evalrealheapsortbb16in.17 [K ~=> C] evalrealheapsortbb16in.16 ~> evalrealheapsortbb17in.18 [] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.19 [] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.20 [] evalrealheapsortbb17in.18 ~> evalrealheapsortbb18in.13 [A ~+> B,B ~+> B] evalrealheapsortbb17in.18 ~> evalrealheapsortbb18in.14 [A ~+> B,B ~+> B] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.21 [] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.22 [] evalrealheapsortbb9in.20 ~> evalrealheapsortbb11in.23 [] evalrealheapsortbb10in.21 ~> evalrealheapsortbb12in.26 [] evalrealheapsortbb10in.22 ~> evalrealheapsortbb11in.23 [] evalrealheapsortbb11in.23 ~> evalrealheapsortbb13in.24 [A ~+> D,C ~+> D] evalrealheapsortbb11in.23 ~> evalrealheapsortbb13in.25 [A ~+> D,C ~+> D] evalrealheapsortbb13in.24 ~> evalrealheapsortbb16in.16 [A ~=> C] evalrealheapsortbb13in.25 ~> evalrealheapsortbb14in.27 [] evalrealheapsortbb12in.26 ~> evalrealheapsortbb13in.24 [A ~+> D,C ~+> D] evalrealheapsortbb12in.26 ~> evalrealheapsortbb13in.25 [A ~+> D,C ~+> D] evalrealheapsortbb14in.27 ~> evalrealheapsortbb16in.16 [D ~=> C] evalrealheapsortbb14in.27 ~> evalrealheapsortbb16in.17 [D ~=> C] evalrealheapsortstop.28 ~> exitus616.30 [] evalrealheapsortstop.29 ~> exitus616.30 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] evalrealheapsortbb6in.4 ~> evalrealheapsortbb3in.5 [B ~=> C] evalrealheapsortbb5in.9 ~> evalrealheapsortbb6in.4 [A ~=> B] evalrealheapsortbb3in.6 ~> evalrealheapsortbb5in.9 [] evalrealheapsortbb2in.11 ~> evalrealheapsortbb3in.6 [A ~=> C] evalrealheapsortbb4in.8 ~> evalrealheapsortbb2in.11 [] evalrealheapsortbb3in.5 ~> evalrealheapsortbb4in.8 [] evalrealheapsortbb2in.11 ~> evalrealheapsortbb3in.5 [A ~=> C] evalrealheapsortbb4in.7 ~> evalrealheapsortbb5in.9 [] evalrealheapsortbb3in.5 ~> evalrealheapsortbb4in.7 [] + Loop: [K ~+> 0.0.0,C ~*> 0.0.0] evalrealheapsortbb3in.5 ~> evalrealheapsortbb4in.8 [] evalrealheapsortbb2in.11 ~> evalrealheapsortbb3in.5 [A ~=> C] evalrealheapsortbb4in.8 ~> evalrealheapsortbb2in.11 [] + Loop: [A ~+> 0.1,B ~+> 0.1,K ~+> 0.1] evalrealheapsortbb18in.14 ~> evalrealheapsortbb8in.15 [] evalrealheapsortbb17in.18 ~> evalrealheapsortbb18in.14 [A ~+> B,B ~+> B] evalrealheapsortbb16in.16 ~> evalrealheapsortbb17in.18 [] evalrealheapsortbb8in.15 ~> evalrealheapsortbb16in.16 [K ~=> C] evalrealheapsortbb13in.24 ~> evalrealheapsortbb16in.16 [A ~=> C] evalrealheapsortbb11in.23 ~> evalrealheapsortbb13in.24 [A ~+> D,C ~+> D] evalrealheapsortbb9in.20 ~> evalrealheapsortbb11in.23 [] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.20 [] evalrealheapsortbb8in.15 ~> evalrealheapsortbb16in.17 [K ~=> C] evalrealheapsortbb14in.27 ~> evalrealheapsortbb16in.17 [D ~=> C] evalrealheapsortbb13in.25 ~> evalrealheapsortbb14in.27 [] evalrealheapsortbb11in.23 ~> evalrealheapsortbb13in.25 [A ~+> D,C ~+> D] evalrealheapsortbb10in.22 ~> evalrealheapsortbb11in.23 [] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.22 [] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.19 [] evalrealheapsortbb12in.26 ~> evalrealheapsortbb13in.25 [A ~+> D,C ~+> D] evalrealheapsortbb10in.21 ~> evalrealheapsortbb12in.26 [] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.21 [] evalrealheapsortbb12in.26 ~> evalrealheapsortbb13in.24 [A ~+> D,C ~+> D] evalrealheapsortbb14in.27 ~> evalrealheapsortbb16in.16 [D ~=> C] + Loop: [A ~+> 0.1.0,C ~+> 0.1.0,K ~*> 0.1.0] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.19 [] evalrealheapsortbb14in.27 ~> evalrealheapsortbb16in.17 [D ~=> C] evalrealheapsortbb13in.25 ~> evalrealheapsortbb14in.27 [] evalrealheapsortbb11in.23 ~> evalrealheapsortbb13in.25 [A ~+> D,C ~+> D] evalrealheapsortbb9in.20 ~> evalrealheapsortbb11in.23 [] evalrealheapsortbb16in.17 ~> evalrealheapsortbb9in.20 [] evalrealheapsortbb10in.22 ~> evalrealheapsortbb11in.23 [] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.22 [] evalrealheapsortbb12in.26 ~> evalrealheapsortbb13in.25 [A ~+> D,C ~+> D] evalrealheapsortbb10in.21 ~> evalrealheapsortbb12in.26 [] evalrealheapsortbb9in.19 ~> evalrealheapsortbb10in.21 [] + Applied Processor: Lare + Details: evalrealheapsortstart.0 ~> exitus616.30 [A ~=> C ,D ~=> C ,K ~=> C ,A ~+> B ,A ~+> C ,A ~+> D ,A ~+> 0.0 ,A ~+> 0.1 ,A ~+> 0.1.0 ,A ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> C ,K ~+> D ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> tick ,A ~*> B ,A ~*> C ,A ~*> D ,A ~*> 0.0.0 ,A ~*> tick ,K ~*> B ,K ~*> C ,K ~*> D ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> tick] + evalrealheapsortbb5in.9> [A ~=> B ,A ~=> C ,B ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> 0.0.0 ,B ~*> tick ,K ~*> tick] + evalrealheapsortbb3in.5> [A ~=> C ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,C ~*> 0.0.0 ,C ~*> tick] evalrealheapsortbb2in.11> [A ~=> C ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick ,C ~*> 0.0.0 ,C ~*> tick] + evalrealheapsortbb17in.18> [A ~=> C ,D ~=> C ,K ~=> C ,A ~+> B ,A ~+> C ,A ~+> D ,A ~+> 0.1 ,A ~+> 0.1.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.1 ,B ~+> tick ,tick ~+> tick ,K ~+> C ,K ~+> D ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> tick ,A ~*> B ,A ~*> C ,A ~*> D ,A ~*> tick ,B ~*> B ,B ~*> tick ,K ~*> B ,K ~*> C ,K ~*> D ,K ~*> 0.1.0 ,K ~*> tick] + evalrealheapsortbb12in.26> [A ~+> C ,A ~+> D ,A ~+> 0.1.0 ,A ~+> tick ,C ~+> C ,C ~+> D ,C ~+> 0.1.0 ,C ~+> tick ,tick ~+> tick ,A ~*> C ,A ~*> D ,C ~*> C ,C ~*> D ,K ~*> C ,K ~*> D ,K ~*> 0.1.0 ,K ~*> tick] evalrealheapsortbb14in.27> [A ~+> C ,A ~+> D ,A ~+> 0.1.0 ,A ~+> tick ,C ~+> C ,C ~+> D ,C ~+> 0.1.0 ,C ~+> tick ,tick ~+> tick ,A ~*> C ,A ~*> D ,C ~*> C ,C ~*> D ,K ~*> C ,K ~*> D ,K ~*> 0.1.0 ,K ~*> tick] evalrealheapsortbb11in.23> [A ~+> C ,A ~+> D ,A ~+> 0.1.0 ,A ~+> tick ,C ~+> C ,C ~+> D ,C ~+> 0.1.0 ,C ~+> tick ,tick ~+> tick ,A ~*> C ,A ~*> D ,C ~*> C ,C ~*> D ,K ~*> C ,K ~*> D ,K ~*> 0.1.0 ,K ~*> tick] YES(?,POLY)