YES(?,POLY) * Step 1: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalrealheapsortstep2start(A,B,C,D) -> evalrealheapsortstep2entryin(A,B,C,D) True (1,1) 1. evalrealheapsortstep2entryin(A,B,C,D) -> evalrealheapsortstep2returnin(A,B,C,D) [2 >= A] (?,1) 2. evalrealheapsortstep2entryin(A,B,C,D) -> evalrealheapsortstep2bbin(A,B,C,D) [A >= 3] (?,1) 3. evalrealheapsortstep2returnin(A,B,C,D) -> evalrealheapsortstep2stop(A,B,C,D) True (?,1) 4. evalrealheapsortstep2bbin(A,B,C,D) -> evalrealheapsortstep2bb11in(A,0,C,D) [-3 + A >= 0] (?,1) 5. evalrealheapsortstep2bb11in(A,B,C,D) -> evalrealheapsortstep2returnin(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 1 + B >= A] (?,1) 6. evalrealheapsortstep2bb11in(A,B,C,D) -> evalrealheapsortstep2bb1in(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 2 + B] (?,1) 7. evalrealheapsortstep2bb1in(A,B,C,D) -> evalrealheapsortstep2bb9in(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] (?,1) 8. evalrealheapsortstep2bb9in(A,B,C,D) -> evalrealheapsortstep2bb10in(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) 9. evalrealheapsortstep2bb9in(A,B,C,D) -> evalrealheapsortstep2bb2in(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) 10. evalrealheapsortstep2bb10in(A,B,C,D) -> evalrealheapsortstep2bb11in(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] (?,1) 11. evalrealheapsortstep2bb2in(A,B,C,D) -> evalrealheapsortstep2bb3in(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] 12. evalrealheapsortstep2bb2in(A,B,C,D) -> evalrealheapsortstep2bb4in(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] 13. evalrealheapsortstep2bb3in(A,B,C,D) -> evalrealheapsortstep2bb5in(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] 14. evalrealheapsortstep2bb3in(A,B,C,D) -> evalrealheapsortstep2bb4in(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] 15. evalrealheapsortstep2bb4in(A,B,C,D) -> evalrealheapsortstep2bb6in(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] 16. evalrealheapsortstep2bb6in(A,B,C,D) -> evalrealheapsortstep2bb9in(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] 17. evalrealheapsortstep2bb6in(A,B,C,D) -> evalrealheapsortstep2bb7in(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] 18. evalrealheapsortstep2bb5in(A,B,C,D) -> evalrealheapsortstep2bb6in(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] 19. evalrealheapsortstep2bb7in(A,B,C,D) -> evalrealheapsortstep2bb9in(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: {(evalrealheapsortstep2bb10in,4) ;(evalrealheapsortstep2bb11in,4) ;(evalrealheapsortstep2bb1in,4) ;(evalrealheapsortstep2bb2in,4) ;(evalrealheapsortstep2bb3in,4) ;(evalrealheapsortstep2bb4in,4) ;(evalrealheapsortstep2bb5in,4) ;(evalrealheapsortstep2bb6in,4) ;(evalrealheapsortstep2bb7in,4) ;(evalrealheapsortstep2bb9in,4) ;(evalrealheapsortstep2bbin,4) ;(evalrealheapsortstep2entryin,4) ;(evalrealheapsortstep2returnin,4) ;(evalrealheapsortstep2start,4) ;(evalrealheapsortstep2stop,4)} Flow Graph: [0->{1,2},1->{3},2->{4},3->{},4->{5,6},5->{3},6->{7},7->{8,9},8->{10},9->{11,12},10->{5,6},11->{13,14} ,12->{15},13->{18},14->{15},15->{16,17},16->{8,9},17->{19},18->{16,17},19->{8,9}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(4,5),(16,9)] * Step 2: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalrealheapsortstep2start(A,B,C,D) -> evalrealheapsortstep2entryin(A,B,C,D) True (1,1) 1. evalrealheapsortstep2entryin(A,B,C,D) -> evalrealheapsortstep2returnin(A,B,C,D) [2 >= A] (?,1) 2. evalrealheapsortstep2entryin(A,B,C,D) -> evalrealheapsortstep2bbin(A,B,C,D) [A >= 3] (?,1) 3. evalrealheapsortstep2returnin(A,B,C,D) -> evalrealheapsortstep2stop(A,B,C,D) True (?,1) 4. evalrealheapsortstep2bbin(A,B,C,D) -> evalrealheapsortstep2bb11in(A,0,C,D) [-3 + A >= 0] (?,1) 5. evalrealheapsortstep2bb11in(A,B,C,D) -> evalrealheapsortstep2returnin(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 1 + B >= A] (?,1) 6. evalrealheapsortstep2bb11in(A,B,C,D) -> evalrealheapsortstep2bb1in(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 2 + B] (?,1) 7. evalrealheapsortstep2bb1in(A,B,C,D) -> evalrealheapsortstep2bb9in(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] (?,1) 8. evalrealheapsortstep2bb9in(A,B,C,D) -> evalrealheapsortstep2bb10in(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) 9. evalrealheapsortstep2bb9in(A,B,C,D) -> evalrealheapsortstep2bb2in(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) 10. evalrealheapsortstep2bb10in(A,B,C,D) -> evalrealheapsortstep2bb11in(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] (?,1) 11. evalrealheapsortstep2bb2in(A,B,C,D) -> evalrealheapsortstep2bb3in(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] 12. evalrealheapsortstep2bb2in(A,B,C,D) -> evalrealheapsortstep2bb4in(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] 13. evalrealheapsortstep2bb3in(A,B,C,D) -> evalrealheapsortstep2bb5in(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] 14. evalrealheapsortstep2bb3in(A,B,C,D) -> evalrealheapsortstep2bb4in(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] 15. evalrealheapsortstep2bb4in(A,B,C,D) -> evalrealheapsortstep2bb6in(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] 16. evalrealheapsortstep2bb6in(A,B,C,D) -> evalrealheapsortstep2bb9in(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] 17. evalrealheapsortstep2bb6in(A,B,C,D) -> evalrealheapsortstep2bb7in(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] 18. evalrealheapsortstep2bb5in(A,B,C,D) -> evalrealheapsortstep2bb6in(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] 19. evalrealheapsortstep2bb7in(A,B,C,D) -> evalrealheapsortstep2bb9in(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: {(evalrealheapsortstep2bb10in,4) ;(evalrealheapsortstep2bb11in,4) ;(evalrealheapsortstep2bb1in,4) ;(evalrealheapsortstep2bb2in,4) ;(evalrealheapsortstep2bb3in,4) ;(evalrealheapsortstep2bb4in,4) ;(evalrealheapsortstep2bb5in,4) ;(evalrealheapsortstep2bb6in,4) ;(evalrealheapsortstep2bb7in,4) ;(evalrealheapsortstep2bb9in,4) ;(evalrealheapsortstep2bbin,4) ;(evalrealheapsortstep2entryin,4) ;(evalrealheapsortstep2returnin,4) ;(evalrealheapsortstep2start,4) ;(evalrealheapsortstep2stop,4)} Flow Graph: [0->{1,2},1->{3},2->{4},3->{},4->{6},5->{3},6->{7},7->{8,9},8->{10},9->{11,12},10->{5,6},11->{13,14} ,12->{15},13->{18},14->{15},15->{16,17},16->{8},17->{19},18->{16,17},19->{8,9}] + Applied Processor: FromIts + Details: () * Step 3: Unfold WORST_CASE(?,POLY) + Considered Problem: Rules: evalrealheapsortstep2start(A,B,C,D) -> evalrealheapsortstep2entryin(A,B,C,D) True evalrealheapsortstep2entryin(A,B,C,D) -> evalrealheapsortstep2returnin(A,B,C,D) [2 >= A] evalrealheapsortstep2entryin(A,B,C,D) -> evalrealheapsortstep2bbin(A,B,C,D) [A >= 3] evalrealheapsortstep2returnin(A,B,C,D) -> evalrealheapsortstep2stop(A,B,C,D) True evalrealheapsortstep2bbin(A,B,C,D) -> evalrealheapsortstep2bb11in(A,0,C,D) [-3 + A >= 0] evalrealheapsortstep2bb11in(A,B,C,D) -> evalrealheapsortstep2returnin(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 1 + B >= A] evalrealheapsortstep2bb11in(A,B,C,D) -> evalrealheapsortstep2bb1in(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 2 + B] evalrealheapsortstep2bb1in(A,B,C,D) -> evalrealheapsortstep2bb9in(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortstep2bb9in(A,B,C,D) -> evalrealheapsortstep2bb10in(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] evalrealheapsortstep2bb9in(A,B,C,D) -> evalrealheapsortstep2bb2in(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] evalrealheapsortstep2bb10in(A,B,C,D) -> evalrealheapsortstep2bb11in(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortstep2bb2in(A,B,C,D) -> evalrealheapsortstep2bb3in(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] evalrealheapsortstep2bb2in(A,B,C,D) -> evalrealheapsortstep2bb4in(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] evalrealheapsortstep2bb3in(A,B,C,D) -> evalrealheapsortstep2bb5in(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] evalrealheapsortstep2bb3in(A,B,C,D) -> evalrealheapsortstep2bb4in(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] evalrealheapsortstep2bb4in(A,B,C,D) -> evalrealheapsortstep2bb6in(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] evalrealheapsortstep2bb6in(A,B,C,D) -> evalrealheapsortstep2bb9in(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] evalrealheapsortstep2bb6in(A,B,C,D) -> evalrealheapsortstep2bb7in(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] evalrealheapsortstep2bb5in(A,B,C,D) -> evalrealheapsortstep2bb6in(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] evalrealheapsortstep2bb7in(A,B,C,D) -> evalrealheapsortstep2bb9in(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: {(evalrealheapsortstep2bb10in,4) ;(evalrealheapsortstep2bb11in,4) ;(evalrealheapsortstep2bb1in,4) ;(evalrealheapsortstep2bb2in,4) ;(evalrealheapsortstep2bb3in,4) ;(evalrealheapsortstep2bb4in,4) ;(evalrealheapsortstep2bb5in,4) ;(evalrealheapsortstep2bb6in,4) ;(evalrealheapsortstep2bb7in,4) ;(evalrealheapsortstep2bb9in,4) ;(evalrealheapsortstep2bbin,4) ;(evalrealheapsortstep2entryin,4) ;(evalrealheapsortstep2returnin,4) ;(evalrealheapsortstep2start,4) ;(evalrealheapsortstep2stop,4)} Rule Graph: [0->{1,2},1->{3},2->{4},3->{},4->{6},5->{3},6->{7},7->{8,9},8->{10},9->{11,12},10->{5,6},11->{13,14} ,12->{15},13->{18},14->{15},15->{16,17},16->{8},17->{19},18->{16,17},19->{8,9}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: evalrealheapsortstep2start.0(A,B,C,D) -> evalrealheapsortstep2entryin.1(A,B,C,D) True evalrealheapsortstep2start.0(A,B,C,D) -> evalrealheapsortstep2entryin.2(A,B,C,D) True evalrealheapsortstep2entryin.1(A,B,C,D) -> evalrealheapsortstep2returnin.3(A,B,C,D) [2 >= A] evalrealheapsortstep2entryin.2(A,B,C,D) -> evalrealheapsortstep2bbin.4(A,B,C,D) [A >= 3] evalrealheapsortstep2returnin.3(A,B,C,D) -> evalrealheapsortstep2stop.20(A,B,C,D) True evalrealheapsortstep2bbin.4(A,B,C,D) -> evalrealheapsortstep2bb11in.6(A,0,C,D) [-3 + A >= 0] evalrealheapsortstep2bb11in.5(A,B,C,D) -> evalrealheapsortstep2returnin.3(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 1 + B >= A] evalrealheapsortstep2bb11in.6(A,B,C,D) -> evalrealheapsortstep2bb1in.7(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 2 + B] evalrealheapsortstep2bb1in.7(A,B,C,D) -> evalrealheapsortstep2bb9in.8(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortstep2bb1in.7(A,B,C,D) -> evalrealheapsortstep2bb9in.9(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortstep2bb9in.8(A,B,C,D) -> evalrealheapsortstep2bb10in.10(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] evalrealheapsortstep2bb9in.9(A,B,C,D) -> evalrealheapsortstep2bb2in.11(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] evalrealheapsortstep2bb9in.9(A,B,C,D) -> evalrealheapsortstep2bb2in.12(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] evalrealheapsortstep2bb10in.10(A,B,C,D) -> evalrealheapsortstep2bb11in.5(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortstep2bb10in.10(A,B,C,D) -> evalrealheapsortstep2bb11in.6(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortstep2bb2in.11(A,B,C,D) -> evalrealheapsortstep2bb3in.13(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] evalrealheapsortstep2bb2in.11(A,B,C,D) -> evalrealheapsortstep2bb3in.14(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] evalrealheapsortstep2bb2in.12(A,B,C,D) -> evalrealheapsortstep2bb4in.15(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] evalrealheapsortstep2bb3in.13(A,B,C,D) -> evalrealheapsortstep2bb5in.18(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] evalrealheapsortstep2bb3in.14(A,B,C,D) -> evalrealheapsortstep2bb4in.15(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] evalrealheapsortstep2bb4in.15(A,B,C,D) -> evalrealheapsortstep2bb6in.16(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] evalrealheapsortstep2bb4in.15(A,B,C,D) -> evalrealheapsortstep2bb6in.17(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] evalrealheapsortstep2bb6in.16(A,B,C,D) -> evalrealheapsortstep2bb9in.8(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] evalrealheapsortstep2bb6in.17(A,B,C,D) -> evalrealheapsortstep2bb7in.19(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] evalrealheapsortstep2bb5in.18(A,B,C,D) -> evalrealheapsortstep2bb6in.16(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] evalrealheapsortstep2bb5in.18(A,B,C,D) -> evalrealheapsortstep2bb6in.17(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] evalrealheapsortstep2bb7in.19(A,B,C,D) -> evalrealheapsortstep2bb9in.8(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] evalrealheapsortstep2bb7in.19(A,B,C,D) -> evalrealheapsortstep2bb9in.9(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: {(evalrealheapsortstep2bb10in.10,4) ;(evalrealheapsortstep2bb11in.5,4) ;(evalrealheapsortstep2bb11in.6,4) ;(evalrealheapsortstep2bb1in.7,4) ;(evalrealheapsortstep2bb2in.11,4) ;(evalrealheapsortstep2bb2in.12,4) ;(evalrealheapsortstep2bb3in.13,4) ;(evalrealheapsortstep2bb3in.14,4) ;(evalrealheapsortstep2bb4in.15,4) ;(evalrealheapsortstep2bb5in.18,4) ;(evalrealheapsortstep2bb6in.16,4) ;(evalrealheapsortstep2bb6in.17,4) ;(evalrealheapsortstep2bb7in.19,4) ;(evalrealheapsortstep2bb9in.8,4) ;(evalrealheapsortstep2bb9in.9,4) ;(evalrealheapsortstep2bbin.4,4) ;(evalrealheapsortstep2entryin.1,4) ;(evalrealheapsortstep2entryin.2,4) ;(evalrealheapsortstep2returnin.3,4) ;(evalrealheapsortstep2start.0,4) ;(evalrealheapsortstep2stop.20,4)} Rule Graph: [0->{2},1->{3},2->{4},3->{5},4->{},5->{7},6->{4},7->{8,9},8->{10},9->{11,12},10->{13,14},11->{15,16} ,12->{17},13->{6},14->{7},15->{18},16->{19},17->{20,21},18->{24,25},19->{20,21},20->{22},21->{23},22->{10} ,23->{26,27},24->{22},25->{23},26->{10},27->{11,12}] + Applied Processor: AddSinks + Details: () * Step 5: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: evalrealheapsortstep2start.0(A,B,C,D) -> evalrealheapsortstep2entryin.1(A,B,C,D) True evalrealheapsortstep2start.0(A,B,C,D) -> evalrealheapsortstep2entryin.2(A,B,C,D) True evalrealheapsortstep2entryin.1(A,B,C,D) -> evalrealheapsortstep2returnin.3(A,B,C,D) [2 >= A] evalrealheapsortstep2entryin.2(A,B,C,D) -> evalrealheapsortstep2bbin.4(A,B,C,D) [A >= 3] evalrealheapsortstep2returnin.3(A,B,C,D) -> evalrealheapsortstep2stop.20(A,B,C,D) True evalrealheapsortstep2bbin.4(A,B,C,D) -> evalrealheapsortstep2bb11in.6(A,0,C,D) [-3 + A >= 0] evalrealheapsortstep2bb11in.5(A,B,C,D) -> evalrealheapsortstep2returnin.3(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 1 + B >= A] evalrealheapsortstep2bb11in.6(A,B,C,D) -> evalrealheapsortstep2bb1in.7(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 2 + B] evalrealheapsortstep2bb1in.7(A,B,C,D) -> evalrealheapsortstep2bb9in.8(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortstep2bb1in.7(A,B,C,D) -> evalrealheapsortstep2bb9in.9(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortstep2bb9in.8(A,B,C,D) -> evalrealheapsortstep2bb10in.10(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] evalrealheapsortstep2bb9in.9(A,B,C,D) -> evalrealheapsortstep2bb2in.11(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] evalrealheapsortstep2bb9in.9(A,B,C,D) -> evalrealheapsortstep2bb2in.12(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] evalrealheapsortstep2bb10in.10(A,B,C,D) -> evalrealheapsortstep2bb11in.5(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortstep2bb10in.10(A,B,C,D) -> evalrealheapsortstep2bb11in.6(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortstep2bb2in.11(A,B,C,D) -> evalrealheapsortstep2bb3in.13(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] evalrealheapsortstep2bb2in.11(A,B,C,D) -> evalrealheapsortstep2bb3in.14(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] evalrealheapsortstep2bb2in.12(A,B,C,D) -> evalrealheapsortstep2bb4in.15(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] evalrealheapsortstep2bb3in.13(A,B,C,D) -> evalrealheapsortstep2bb5in.18(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] evalrealheapsortstep2bb3in.14(A,B,C,D) -> evalrealheapsortstep2bb4in.15(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] evalrealheapsortstep2bb4in.15(A,B,C,D) -> evalrealheapsortstep2bb6in.16(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] evalrealheapsortstep2bb4in.15(A,B,C,D) -> evalrealheapsortstep2bb6in.17(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] evalrealheapsortstep2bb6in.16(A,B,C,D) -> evalrealheapsortstep2bb9in.8(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] evalrealheapsortstep2bb6in.17(A,B,C,D) -> evalrealheapsortstep2bb7in.19(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] evalrealheapsortstep2bb5in.18(A,B,C,D) -> evalrealheapsortstep2bb6in.16(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] evalrealheapsortstep2bb5in.18(A,B,C,D) -> evalrealheapsortstep2bb6in.17(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] evalrealheapsortstep2bb7in.19(A,B,C,D) -> evalrealheapsortstep2bb9in.8(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] evalrealheapsortstep2bb7in.19(A,B,C,D) -> evalrealheapsortstep2bb9in.9(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] evalrealheapsortstep2stop.20(A,B,C,D) -> exitus616(A,B,C,D) True evalrealheapsortstep2stop.20(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(evalrealheapsortstep2bb10in.10,4) ;(evalrealheapsortstep2bb11in.5,4) ;(evalrealheapsortstep2bb11in.6,4) ;(evalrealheapsortstep2bb1in.7,4) ;(evalrealheapsortstep2bb2in.11,4) ;(evalrealheapsortstep2bb2in.12,4) ;(evalrealheapsortstep2bb3in.13,4) ;(evalrealheapsortstep2bb3in.14,4) ;(evalrealheapsortstep2bb4in.15,4) ;(evalrealheapsortstep2bb5in.18,4) ;(evalrealheapsortstep2bb6in.16,4) ;(evalrealheapsortstep2bb6in.17,4) ;(evalrealheapsortstep2bb7in.19,4) ;(evalrealheapsortstep2bb9in.8,4) ;(evalrealheapsortstep2bb9in.9,4) ;(evalrealheapsortstep2bbin.4,4) ;(evalrealheapsortstep2entryin.1,4) ;(evalrealheapsortstep2entryin.2,4) ;(evalrealheapsortstep2returnin.3,4) ;(evalrealheapsortstep2start.0,4) ;(evalrealheapsortstep2stop.20,4) ;(exitus616,4)} Rule Graph: [0->{2},1->{3},2->{4},3->{5},4->{28,29},5->{7},6->{4},7->{8,9},8->{10},9->{11,12},10->{13,14},11->{15,16} ,12->{17},13->{6},14->{7},15->{18},16->{19},17->{20,21},18->{24,25},19->{20,21},20->{22},21->{23},22->{10} ,23->{26,27},24->{22},25->{23},26->{10},27->{11,12}] + 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] | `- p:[7,14,10,8,22,20,17,12,9,27,23,21,19,16,11,25,18,15,24,26] c: [7,8,9,10,14,20,22,24,26] | `- p:[11,27,23,21,17,12,19,16,25,18,15] c: [11,12,15,16,17,18,19,21,23,25,27] * Step 6: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: evalrealheapsortstep2start.0(A,B,C,D) -> evalrealheapsortstep2entryin.1(A,B,C,D) True evalrealheapsortstep2start.0(A,B,C,D) -> evalrealheapsortstep2entryin.2(A,B,C,D) True evalrealheapsortstep2entryin.1(A,B,C,D) -> evalrealheapsortstep2returnin.3(A,B,C,D) [2 >= A] evalrealheapsortstep2entryin.2(A,B,C,D) -> evalrealheapsortstep2bbin.4(A,B,C,D) [A >= 3] evalrealheapsortstep2returnin.3(A,B,C,D) -> evalrealheapsortstep2stop.20(A,B,C,D) True evalrealheapsortstep2bbin.4(A,B,C,D) -> evalrealheapsortstep2bb11in.6(A,0,C,D) [-3 + A >= 0] evalrealheapsortstep2bb11in.5(A,B,C,D) -> evalrealheapsortstep2returnin.3(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 1 + B >= A] evalrealheapsortstep2bb11in.6(A,B,C,D) -> evalrealheapsortstep2bb1in.7(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 2 + B] evalrealheapsortstep2bb1in.7(A,B,C,D) -> evalrealheapsortstep2bb9in.8(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortstep2bb1in.7(A,B,C,D) -> evalrealheapsortstep2bb9in.9(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortstep2bb9in.8(A,B,C,D) -> evalrealheapsortstep2bb10in.10(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] evalrealheapsortstep2bb9in.9(A,B,C,D) -> evalrealheapsortstep2bb2in.11(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] evalrealheapsortstep2bb9in.9(A,B,C,D) -> evalrealheapsortstep2bb2in.12(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] evalrealheapsortstep2bb10in.10(A,B,C,D) -> evalrealheapsortstep2bb11in.5(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortstep2bb10in.10(A,B,C,D) -> evalrealheapsortstep2bb11in.6(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] evalrealheapsortstep2bb2in.11(A,B,C,D) -> evalrealheapsortstep2bb3in.13(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] evalrealheapsortstep2bb2in.11(A,B,C,D) -> evalrealheapsortstep2bb3in.14(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] evalrealheapsortstep2bb2in.12(A,B,C,D) -> evalrealheapsortstep2bb4in.15(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] evalrealheapsortstep2bb3in.13(A,B,C,D) -> evalrealheapsortstep2bb5in.18(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] evalrealheapsortstep2bb3in.14(A,B,C,D) -> evalrealheapsortstep2bb4in.15(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] evalrealheapsortstep2bb4in.15(A,B,C,D) -> evalrealheapsortstep2bb6in.16(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] evalrealheapsortstep2bb4in.15(A,B,C,D) -> evalrealheapsortstep2bb6in.17(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] evalrealheapsortstep2bb6in.16(A,B,C,D) -> evalrealheapsortstep2bb9in.8(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] evalrealheapsortstep2bb6in.17(A,B,C,D) -> evalrealheapsortstep2bb7in.19(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] evalrealheapsortstep2bb5in.18(A,B,C,D) -> evalrealheapsortstep2bb6in.16(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] evalrealheapsortstep2bb5in.18(A,B,C,D) -> evalrealheapsortstep2bb6in.17(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] evalrealheapsortstep2bb7in.19(A,B,C,D) -> evalrealheapsortstep2bb9in.8(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] evalrealheapsortstep2bb7in.19(A,B,C,D) -> evalrealheapsortstep2bb9in.9(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] evalrealheapsortstep2stop.20(A,B,C,D) -> exitus616(A,B,C,D) True evalrealheapsortstep2stop.20(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(evalrealheapsortstep2bb10in.10,4) ;(evalrealheapsortstep2bb11in.5,4) ;(evalrealheapsortstep2bb11in.6,4) ;(evalrealheapsortstep2bb1in.7,4) ;(evalrealheapsortstep2bb2in.11,4) ;(evalrealheapsortstep2bb2in.12,4) ;(evalrealheapsortstep2bb3in.13,4) ;(evalrealheapsortstep2bb3in.14,4) ;(evalrealheapsortstep2bb4in.15,4) ;(evalrealheapsortstep2bb5in.18,4) ;(evalrealheapsortstep2bb6in.16,4) ;(evalrealheapsortstep2bb6in.17,4) ;(evalrealheapsortstep2bb7in.19,4) ;(evalrealheapsortstep2bb9in.8,4) ;(evalrealheapsortstep2bb9in.9,4) ;(evalrealheapsortstep2bbin.4,4) ;(evalrealheapsortstep2entryin.1,4) ;(evalrealheapsortstep2entryin.2,4) ;(evalrealheapsortstep2returnin.3,4) ;(evalrealheapsortstep2start.0,4) ;(evalrealheapsortstep2stop.20,4) ;(exitus616,4)} Rule Graph: [0->{2},1->{3},2->{4},3->{5},4->{28,29},5->{7},6->{4},7->{8,9},8->{10},9->{11,12},10->{13,14},11->{15,16} ,12->{17},13->{6},14->{7},15->{18},16->{19},17->{20,21},18->{24,25},19->{20,21},20->{22},21->{23},22->{10} ,23->{26,27},24->{22},25->{23},26->{10},27->{11,12}] ,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] | `- p:[7,14,10,8,22,20,17,12,9,27,23,21,19,16,11,25,18,15,24,26] c: [7,8,9,10,14,20,22,24,26] | `- p:[11,27,23,21,17,12,19,16,25,18,15] c: [11,12,15,16,17,18,19,21,23,25,27]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,0.0,0.0.0] evalrealheapsortstep2start.0 ~> evalrealheapsortstep2entryin.1 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2start.0 ~> evalrealheapsortstep2entryin.2 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2entryin.1 ~> evalrealheapsortstep2returnin.3 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2entryin.2 ~> evalrealheapsortstep2bbin.4 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2returnin.3 ~> evalrealheapsortstep2stop.20 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bbin.4 ~> evalrealheapsortstep2bb11in.6 [A <= A, B <= 0*K, C <= C, D <= D] evalrealheapsortstep2bb11in.5 ~> evalrealheapsortstep2returnin.3 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb11in.6 ~> evalrealheapsortstep2bb1in.7 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb1in.7 ~> evalrealheapsortstep2bb9in.8 [A <= A, B <= B, C <= 0*K, D <= D] evalrealheapsortstep2bb1in.7 ~> evalrealheapsortstep2bb9in.9 [A <= A, B <= B, C <= 0*K, D <= D] evalrealheapsortstep2bb9in.8 ~> evalrealheapsortstep2bb10in.10 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb9in.9 ~> evalrealheapsortstep2bb2in.11 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb9in.9 ~> evalrealheapsortstep2bb2in.12 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb10in.10 ~> evalrealheapsortstep2bb11in.5 [A <= A, B <= A + B, C <= C, D <= D] evalrealheapsortstep2bb10in.10 ~> evalrealheapsortstep2bb11in.6 [A <= A, B <= A + B, C <= C, D <= D] evalrealheapsortstep2bb2in.11 ~> evalrealheapsortstep2bb3in.13 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb2in.11 ~> evalrealheapsortstep2bb3in.14 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb2in.12 ~> evalrealheapsortstep2bb4in.15 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb3in.13 ~> evalrealheapsortstep2bb5in.18 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb3in.14 ~> evalrealheapsortstep2bb4in.15 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb4in.15 ~> evalrealheapsortstep2bb6in.16 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortstep2bb4in.15 ~> evalrealheapsortstep2bb6in.17 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortstep2bb6in.16 ~> evalrealheapsortstep2bb9in.8 [A <= A, B <= B, C <= A, D <= D] evalrealheapsortstep2bb6in.17 ~> evalrealheapsortstep2bb7in.19 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb5in.18 ~> evalrealheapsortstep2bb6in.16 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortstep2bb5in.18 ~> evalrealheapsortstep2bb6in.17 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortstep2bb7in.19 ~> evalrealheapsortstep2bb9in.8 [A <= A, B <= B, C <= D, D <= D] evalrealheapsortstep2bb7in.19 ~> evalrealheapsortstep2bb9in.9 [A <= A, B <= B, C <= D, D <= D] evalrealheapsortstep2stop.20 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2stop.20 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= K + A + B] evalrealheapsortstep2bb11in.6 ~> evalrealheapsortstep2bb1in.7 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb10in.10 ~> evalrealheapsortstep2bb11in.6 [A <= A, B <= A + B, C <= C, D <= D] evalrealheapsortstep2bb9in.8 ~> evalrealheapsortstep2bb10in.10 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb1in.7 ~> evalrealheapsortstep2bb9in.8 [A <= A, B <= B, C <= 0*K, D <= D] evalrealheapsortstep2bb6in.16 ~> evalrealheapsortstep2bb9in.8 [A <= A, B <= B, C <= A, D <= D] evalrealheapsortstep2bb4in.15 ~> evalrealheapsortstep2bb6in.16 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortstep2bb2in.12 ~> evalrealheapsortstep2bb4in.15 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb9in.9 ~> evalrealheapsortstep2bb2in.12 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb1in.7 ~> evalrealheapsortstep2bb9in.9 [A <= A, B <= B, C <= 0*K, D <= D] evalrealheapsortstep2bb7in.19 ~> evalrealheapsortstep2bb9in.9 [A <= A, B <= B, C <= D, D <= D] evalrealheapsortstep2bb6in.17 ~> evalrealheapsortstep2bb7in.19 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb4in.15 ~> evalrealheapsortstep2bb6in.17 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortstep2bb3in.14 ~> evalrealheapsortstep2bb4in.15 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb2in.11 ~> evalrealheapsortstep2bb3in.14 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb9in.9 ~> evalrealheapsortstep2bb2in.11 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb5in.18 ~> evalrealheapsortstep2bb6in.17 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortstep2bb3in.13 ~> evalrealheapsortstep2bb5in.18 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb2in.11 ~> evalrealheapsortstep2bb3in.13 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb5in.18 ~> evalrealheapsortstep2bb6in.16 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortstep2bb7in.19 ~> evalrealheapsortstep2bb9in.8 [A <= A, B <= B, C <= D, D <= D] + Loop: [0.0.0 <= 3*K + A + C] evalrealheapsortstep2bb9in.9 ~> evalrealheapsortstep2bb2in.11 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb7in.19 ~> evalrealheapsortstep2bb9in.9 [A <= A, B <= B, C <= D, D <= D] evalrealheapsortstep2bb6in.17 ~> evalrealheapsortstep2bb7in.19 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb4in.15 ~> evalrealheapsortstep2bb6in.17 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortstep2bb2in.12 ~> evalrealheapsortstep2bb4in.15 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb9in.9 ~> evalrealheapsortstep2bb2in.12 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb3in.14 ~> evalrealheapsortstep2bb4in.15 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb2in.11 ~> evalrealheapsortstep2bb3in.14 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb5in.18 ~> evalrealheapsortstep2bb6in.17 [A <= A, B <= B, C <= C, D <= A + C] evalrealheapsortstep2bb3in.13 ~> evalrealheapsortstep2bb5in.18 [A <= A, B <= B, C <= C, D <= D] evalrealheapsortstep2bb2in.11 ~> evalrealheapsortstep2bb3in.13 [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] evalrealheapsortstep2start.0 ~> evalrealheapsortstep2entryin.1 [] evalrealheapsortstep2start.0 ~> evalrealheapsortstep2entryin.2 [] evalrealheapsortstep2entryin.1 ~> evalrealheapsortstep2returnin.3 [] evalrealheapsortstep2entryin.2 ~> evalrealheapsortstep2bbin.4 [] evalrealheapsortstep2returnin.3 ~> evalrealheapsortstep2stop.20 [] evalrealheapsortstep2bbin.4 ~> evalrealheapsortstep2bb11in.6 [K ~=> B] evalrealheapsortstep2bb11in.5 ~> evalrealheapsortstep2returnin.3 [] evalrealheapsortstep2bb11in.6 ~> evalrealheapsortstep2bb1in.7 [] evalrealheapsortstep2bb1in.7 ~> evalrealheapsortstep2bb9in.8 [K ~=> C] evalrealheapsortstep2bb1in.7 ~> evalrealheapsortstep2bb9in.9 [K ~=> C] evalrealheapsortstep2bb9in.8 ~> evalrealheapsortstep2bb10in.10 [] evalrealheapsortstep2bb9in.9 ~> evalrealheapsortstep2bb2in.11 [] evalrealheapsortstep2bb9in.9 ~> evalrealheapsortstep2bb2in.12 [] evalrealheapsortstep2bb10in.10 ~> evalrealheapsortstep2bb11in.5 [A ~+> B,B ~+> B] evalrealheapsortstep2bb10in.10 ~> evalrealheapsortstep2bb11in.6 [A ~+> B,B ~+> B] evalrealheapsortstep2bb2in.11 ~> evalrealheapsortstep2bb3in.13 [] evalrealheapsortstep2bb2in.11 ~> evalrealheapsortstep2bb3in.14 [] evalrealheapsortstep2bb2in.12 ~> evalrealheapsortstep2bb4in.15 [] evalrealheapsortstep2bb3in.13 ~> evalrealheapsortstep2bb5in.18 [] evalrealheapsortstep2bb3in.14 ~> evalrealheapsortstep2bb4in.15 [] evalrealheapsortstep2bb4in.15 ~> evalrealheapsortstep2bb6in.16 [A ~+> D,C ~+> D] evalrealheapsortstep2bb4in.15 ~> evalrealheapsortstep2bb6in.17 [A ~+> D,C ~+> D] evalrealheapsortstep2bb6in.16 ~> evalrealheapsortstep2bb9in.8 [A ~=> C] evalrealheapsortstep2bb6in.17 ~> evalrealheapsortstep2bb7in.19 [] evalrealheapsortstep2bb5in.18 ~> evalrealheapsortstep2bb6in.16 [A ~+> D,C ~+> D] evalrealheapsortstep2bb5in.18 ~> evalrealheapsortstep2bb6in.17 [A ~+> D,C ~+> D] evalrealheapsortstep2bb7in.19 ~> evalrealheapsortstep2bb9in.8 [D ~=> C] evalrealheapsortstep2bb7in.19 ~> evalrealheapsortstep2bb9in.9 [D ~=> C] evalrealheapsortstep2stop.20 ~> exitus616 [] evalrealheapsortstep2stop.20 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] evalrealheapsortstep2bb11in.6 ~> evalrealheapsortstep2bb1in.7 [] evalrealheapsortstep2bb10in.10 ~> evalrealheapsortstep2bb11in.6 [A ~+> B,B ~+> B] evalrealheapsortstep2bb9in.8 ~> evalrealheapsortstep2bb10in.10 [] evalrealheapsortstep2bb1in.7 ~> evalrealheapsortstep2bb9in.8 [K ~=> C] evalrealheapsortstep2bb6in.16 ~> evalrealheapsortstep2bb9in.8 [A ~=> C] evalrealheapsortstep2bb4in.15 ~> evalrealheapsortstep2bb6in.16 [A ~+> D,C ~+> D] evalrealheapsortstep2bb2in.12 ~> evalrealheapsortstep2bb4in.15 [] evalrealheapsortstep2bb9in.9 ~> evalrealheapsortstep2bb2in.12 [] evalrealheapsortstep2bb1in.7 ~> evalrealheapsortstep2bb9in.9 [K ~=> C] evalrealheapsortstep2bb7in.19 ~> evalrealheapsortstep2bb9in.9 [D ~=> C] evalrealheapsortstep2bb6in.17 ~> evalrealheapsortstep2bb7in.19 [] evalrealheapsortstep2bb4in.15 ~> evalrealheapsortstep2bb6in.17 [A ~+> D,C ~+> D] evalrealheapsortstep2bb3in.14 ~> evalrealheapsortstep2bb4in.15 [] evalrealheapsortstep2bb2in.11 ~> evalrealheapsortstep2bb3in.14 [] evalrealheapsortstep2bb9in.9 ~> evalrealheapsortstep2bb2in.11 [] evalrealheapsortstep2bb5in.18 ~> evalrealheapsortstep2bb6in.17 [A ~+> D,C ~+> D] evalrealheapsortstep2bb3in.13 ~> evalrealheapsortstep2bb5in.18 [] evalrealheapsortstep2bb2in.11 ~> evalrealheapsortstep2bb3in.13 [] evalrealheapsortstep2bb5in.18 ~> evalrealheapsortstep2bb6in.16 [A ~+> D,C ~+> D] evalrealheapsortstep2bb7in.19 ~> evalrealheapsortstep2bb9in.8 [D ~=> C] + Loop: [A ~+> 0.0.0,C ~+> 0.0.0,K ~*> 0.0.0] evalrealheapsortstep2bb9in.9 ~> evalrealheapsortstep2bb2in.11 [] evalrealheapsortstep2bb7in.19 ~> evalrealheapsortstep2bb9in.9 [D ~=> C] evalrealheapsortstep2bb6in.17 ~> evalrealheapsortstep2bb7in.19 [] evalrealheapsortstep2bb4in.15 ~> evalrealheapsortstep2bb6in.17 [A ~+> D,C ~+> D] evalrealheapsortstep2bb2in.12 ~> evalrealheapsortstep2bb4in.15 [] evalrealheapsortstep2bb9in.9 ~> evalrealheapsortstep2bb2in.12 [] evalrealheapsortstep2bb3in.14 ~> evalrealheapsortstep2bb4in.15 [] evalrealheapsortstep2bb2in.11 ~> evalrealheapsortstep2bb3in.14 [] evalrealheapsortstep2bb5in.18 ~> evalrealheapsortstep2bb6in.17 [A ~+> D,C ~+> D] evalrealheapsortstep2bb3in.13 ~> evalrealheapsortstep2bb5in.18 [] evalrealheapsortstep2bb2in.11 ~> evalrealheapsortstep2bb3in.13 [] + Applied Processor: Lare + Details: evalrealheapsortstep2start.0 ~> exitus616 [A ~=> C ,D ~=> C ,K ~=> C ,A ~+> B ,A ~+> C ,A ~+> D ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> C ,K ~+> D ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> C ,A ~*> D ,A ~*> tick ,K ~*> B ,K ~*> C ,K ~*> D ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick] + evalrealheapsortstep2bb10in.10> [A ~=> C ,D ~=> C ,K ~=> C ,A ~+> B ,A ~+> C ,A ~+> D ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> C ,K ~+> D ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> B ,A ~*> C ,A ~*> D ,A ~*> tick ,B ~*> B ,B ~*> tick ,K ~*> B ,K ~*> C ,K ~*> D ,K ~*> 0.0.0 ,K ~*> tick] + evalrealheapsortstep2bb5in.18> [A ~+> C ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,C ~+> C ,C ~+> D ,C ~+> 0.0.0 ,C ~+> tick ,tick ~+> tick ,A ~*> C ,A ~*> D ,C ~*> C ,C ~*> D ,K ~*> C ,K ~*> D ,K ~*> 0.0.0 ,K ~*> tick] evalrealheapsortstep2bb7in.19> [A ~+> C ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,C ~+> C ,C ~+> D ,C ~+> 0.0.0 ,C ~+> tick ,tick ~+> tick ,A ~*> C ,A ~*> D ,C ~*> C ,C ~*> D ,K ~*> C ,K ~*> D ,K ~*> 0.0.0 ,K ~*> tick] evalrealheapsortstep2bb4in.15> [A ~+> C ,A ~+> D ,A ~+> 0.0.0 ,A ~+> tick ,C ~+> C ,C ~+> D ,C ~+> 0.0.0 ,C ~+> tick ,tick ~+> tick ,A ~*> C ,A ~*> D ,C ~*> C ,C ~*> D ,K ~*> C ,K ~*> D ,K ~*> 0.0.0 ,K ~*> tick] YES(?,POLY)