YES(?,POLY) * Step 1: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalEx4start(A,B,C,D) -> evalEx4entryin(A,B,C,D) True (1,1) 1. evalEx4entryin(A,B,C,D) -> evalEx4bb4in(1,A,C,D) True (?,1) 2. evalEx4bb4in(A,B,C,D) -> evalEx4bb2in(A,B,0,B) [A = 1] (?,1) 3. evalEx4bb4in(A,B,C,D) -> evalEx4returnin(A,B,C,D) [0 >= A] (?,1) 4. evalEx4bb4in(A,B,C,D) -> evalEx4returnin(A,B,C,D) [A >= 2] (?,1) 5. evalEx4bb2in(A,B,C,D) -> evalEx4bb4in(C,D,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= D] (?,1) 6. evalEx4bb2in(A,B,C,D) -> evalEx4bb3in(A,B,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && D >= 1] (?,1) 7. evalEx4bb3in(A,B,C,D) -> evalEx4bb1in(A,B,C,D) [B + -1*D >= 0 (?,1) && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= 1 + E] 8. evalEx4bb3in(A,B,C,D) -> evalEx4bb1in(A,B,C,D) [B + -1*D >= 0 (?,1) && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && E >= 1] 9. evalEx4bb3in(A,B,C,D) -> evalEx4bb4in(C,D,C,D) [B + -1*D >= 0 (?,1) && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] 10. evalEx4bb1in(A,B,C,D) -> evalEx4bb2in(A,B,1,-1 + D) [B + -1*D >= 0 (?,1) && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] 11. evalEx4returnin(A,B,C,D) -> evalEx4stop(A,B,C,D) True (?,1) Signature: {(evalEx4bb1in,4) ;(evalEx4bb2in,4) ;(evalEx4bb3in,4) ;(evalEx4bb4in,4) ;(evalEx4entryin,4) ;(evalEx4returnin,4) ;(evalEx4start,4) ;(evalEx4stop,4)} Flow Graph: [0->{1},1->{2,3,4},2->{5,6},3->{11},4->{11},5->{2,3,4},6->{7,8,9},7->{10},8->{10},9->{2,3,4},10->{5,6} ,11->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,3),(1,4)] * Step 2: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. evalEx4start(A,B,C,D) -> evalEx4entryin(A,B,C,D) True (1,1) 1. evalEx4entryin(A,B,C,D) -> evalEx4bb4in(1,A,C,D) True (?,1) 2. evalEx4bb4in(A,B,C,D) -> evalEx4bb2in(A,B,0,B) [A = 1] (?,1) 3. evalEx4bb4in(A,B,C,D) -> evalEx4returnin(A,B,C,D) [0 >= A] (?,1) 4. evalEx4bb4in(A,B,C,D) -> evalEx4returnin(A,B,C,D) [A >= 2] (?,1) 5. evalEx4bb2in(A,B,C,D) -> evalEx4bb4in(C,D,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= D] (?,1) 6. evalEx4bb2in(A,B,C,D) -> evalEx4bb3in(A,B,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && D >= 1] (?,1) 7. evalEx4bb3in(A,B,C,D) -> evalEx4bb1in(A,B,C,D) [B + -1*D >= 0 (?,1) && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= 1 + E] 8. evalEx4bb3in(A,B,C,D) -> evalEx4bb1in(A,B,C,D) [B + -1*D >= 0 (?,1) && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && E >= 1] 9. evalEx4bb3in(A,B,C,D) -> evalEx4bb4in(C,D,C,D) [B + -1*D >= 0 (?,1) && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] 10. evalEx4bb1in(A,B,C,D) -> evalEx4bb2in(A,B,1,-1 + D) [B + -1*D >= 0 (?,1) && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] 11. evalEx4returnin(A,B,C,D) -> evalEx4stop(A,B,C,D) True (?,1) Signature: {(evalEx4bb1in,4) ;(evalEx4bb2in,4) ;(evalEx4bb3in,4) ;(evalEx4bb4in,4) ;(evalEx4entryin,4) ;(evalEx4returnin,4) ;(evalEx4start,4) ;(evalEx4stop,4)} Flow Graph: [0->{1},1->{2},2->{5,6},3->{11},4->{11},5->{2,3,4},6->{7,8,9},7->{10},8->{10},9->{2,3,4},10->{5,6},11->{}] + Applied Processor: FromIts + Details: () * Step 3: Unfold WORST_CASE(?,POLY) + Considered Problem: Rules: evalEx4start(A,B,C,D) -> evalEx4entryin(A,B,C,D) True evalEx4entryin(A,B,C,D) -> evalEx4bb4in(1,A,C,D) True evalEx4bb4in(A,B,C,D) -> evalEx4bb2in(A,B,0,B) [A = 1] evalEx4bb4in(A,B,C,D) -> evalEx4returnin(A,B,C,D) [0 >= A] evalEx4bb4in(A,B,C,D) -> evalEx4returnin(A,B,C,D) [A >= 2] evalEx4bb2in(A,B,C,D) -> evalEx4bb4in(C,D,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= D] evalEx4bb2in(A,B,C,D) -> evalEx4bb3in(A,B,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && D >= 1] evalEx4bb3in(A,B,C,D) -> evalEx4bb1in(A,B,C,D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= 1 + E] evalEx4bb3in(A,B,C,D) -> evalEx4bb1in(A,B,C,D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && E >= 1] evalEx4bb3in(A,B,C,D) -> evalEx4bb4in(C,D,C,D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] evalEx4bb1in(A,B,C,D) -> evalEx4bb2in(A,B,1,-1 + D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] evalEx4returnin(A,B,C,D) -> evalEx4stop(A,B,C,D) True Signature: {(evalEx4bb1in,4) ;(evalEx4bb2in,4) ;(evalEx4bb3in,4) ;(evalEx4bb4in,4) ;(evalEx4entryin,4) ;(evalEx4returnin,4) ;(evalEx4start,4) ;(evalEx4stop,4)} Rule Graph: [0->{1},1->{2},2->{5,6},3->{11},4->{11},5->{2,3,4},6->{7,8,9},7->{10},8->{10},9->{2,3,4},10->{5,6},11->{}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: evalEx4start.0(A,B,C,D) -> evalEx4entryin.1(A,B,C,D) True evalEx4entryin.1(A,B,C,D) -> evalEx4bb4in.2(1,A,C,D) True evalEx4bb4in.2(A,B,C,D) -> evalEx4bb2in.5(A,B,0,B) [A = 1] evalEx4bb4in.2(A,B,C,D) -> evalEx4bb2in.6(A,B,0,B) [A = 1] evalEx4bb4in.3(A,B,C,D) -> evalEx4returnin.11(A,B,C,D) [0 >= A] evalEx4bb4in.4(A,B,C,D) -> evalEx4returnin.11(A,B,C,D) [A >= 2] evalEx4bb2in.5(A,B,C,D) -> evalEx4bb4in.2(C,D,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= D] evalEx4bb2in.5(A,B,C,D) -> evalEx4bb4in.3(C,D,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= D] evalEx4bb2in.5(A,B,C,D) -> evalEx4bb4in.4(C,D,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= D] evalEx4bb2in.6(A,B,C,D) -> evalEx4bb3in.7(A,B,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && D >= 1] evalEx4bb2in.6(A,B,C,D) -> evalEx4bb3in.8(A,B,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && D >= 1] evalEx4bb2in.6(A,B,C,D) -> evalEx4bb3in.9(A,B,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && D >= 1] evalEx4bb3in.7(A,B,C,D) -> evalEx4bb1in.10(A,B,C,D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= 1 + E] evalEx4bb3in.8(A,B,C,D) -> evalEx4bb1in.10(A,B,C,D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && E >= 1] evalEx4bb3in.9(A,B,C,D) -> evalEx4bb4in.2(C,D,C,D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] evalEx4bb3in.9(A,B,C,D) -> evalEx4bb4in.3(C,D,C,D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] evalEx4bb3in.9(A,B,C,D) -> evalEx4bb4in.4(C,D,C,D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] evalEx4bb1in.10(A,B,C,D) -> evalEx4bb2in.5(A,B,1,-1 + D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] evalEx4bb1in.10(A,B,C,D) -> evalEx4bb2in.6(A,B,1,-1 + D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] evalEx4returnin.11(A,B,C,D) -> evalEx4stop.12(A,B,C,D) True Signature: {(evalEx4bb1in.10,4) ;(evalEx4bb2in.5,4) ;(evalEx4bb2in.6,4) ;(evalEx4bb3in.7,4) ;(evalEx4bb3in.8,4) ;(evalEx4bb3in.9,4) ;(evalEx4bb4in.2,4) ;(evalEx4bb4in.3,4) ;(evalEx4bb4in.4,4) ;(evalEx4entryin.1,4) ;(evalEx4returnin.11,4) ;(evalEx4start.0,4) ;(evalEx4stop.12,4)} Rule Graph: [0->{1},1->{2,3},2->{6,7,8},3->{9,10,11},4->{19},5->{19},6->{2,3},7->{4},8->{5},9->{12},10->{13},11->{14 ,15,16},12->{17,18},13->{17,18},14->{2,3},15->{4},16->{5},17->{6,7,8},18->{9,10,11},19->{}] + Applied Processor: AddSinks + Details: () * Step 5: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: evalEx4start.0(A,B,C,D) -> evalEx4entryin.1(A,B,C,D) True evalEx4entryin.1(A,B,C,D) -> evalEx4bb4in.2(1,A,C,D) True evalEx4bb4in.2(A,B,C,D) -> evalEx4bb2in.5(A,B,0,B) [A = 1] evalEx4bb4in.2(A,B,C,D) -> evalEx4bb2in.6(A,B,0,B) [A = 1] evalEx4bb4in.3(A,B,C,D) -> evalEx4returnin.11(A,B,C,D) [0 >= A] evalEx4bb4in.4(A,B,C,D) -> evalEx4returnin.11(A,B,C,D) [A >= 2] evalEx4bb2in.5(A,B,C,D) -> evalEx4bb4in.2(C,D,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= D] evalEx4bb2in.5(A,B,C,D) -> evalEx4bb4in.3(C,D,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= D] evalEx4bb2in.5(A,B,C,D) -> evalEx4bb4in.4(C,D,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= D] evalEx4bb2in.6(A,B,C,D) -> evalEx4bb3in.7(A,B,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && D >= 1] evalEx4bb2in.6(A,B,C,D) -> evalEx4bb3in.8(A,B,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && D >= 1] evalEx4bb2in.6(A,B,C,D) -> evalEx4bb3in.9(A,B,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && D >= 1] evalEx4bb3in.7(A,B,C,D) -> evalEx4bb1in.10(A,B,C,D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= 1 + E] evalEx4bb3in.8(A,B,C,D) -> evalEx4bb1in.10(A,B,C,D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && E >= 1] evalEx4bb3in.9(A,B,C,D) -> evalEx4bb4in.2(C,D,C,D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] evalEx4bb3in.9(A,B,C,D) -> evalEx4bb4in.3(C,D,C,D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] evalEx4bb3in.9(A,B,C,D) -> evalEx4bb4in.4(C,D,C,D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] evalEx4bb1in.10(A,B,C,D) -> evalEx4bb2in.5(A,B,1,-1 + D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] evalEx4bb1in.10(A,B,C,D) -> evalEx4bb2in.6(A,B,1,-1 + D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] evalEx4returnin.11(A,B,C,D) -> evalEx4stop.12(A,B,C,D) True evalEx4stop.12(A,B,C,D) -> exitus616(A,B,C,D) True evalEx4stop.12(A,B,C,D) -> exitus616(A,B,C,D) True evalEx4stop.12(A,B,C,D) -> exitus616(A,B,C,D) True evalEx4stop.12(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(evalEx4bb1in.10,4) ;(evalEx4bb2in.5,4) ;(evalEx4bb2in.6,4) ;(evalEx4bb3in.7,4) ;(evalEx4bb3in.8,4) ;(evalEx4bb3in.9,4) ;(evalEx4bb4in.2,4) ;(evalEx4bb4in.3,4) ;(evalEx4bb4in.4,4) ;(evalEx4entryin.1,4) ;(evalEx4returnin.11,4) ;(evalEx4start.0,4) ;(evalEx4stop.12,4) ;(exitus616,4)} Rule Graph: [0->{1},1->{2,3},2->{6,7,8},3->{9,10,11},4->{19},5->{19},6->{2,3},7->{4},8->{5},9->{12},10->{13},11->{14 ,15,16},12->{17,18},13->{17,18},14->{2,3},15->{4},16->{5},17->{6,7,8},18->{9,10,11},19->{20,21,22,23}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23] | `- p:[2,6,17,12,9,3,14,11,18,13,10] c: [9,10,11,12,13,14,17,18] | `- p:[2,6] c: [2,6] * Step 6: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: evalEx4start.0(A,B,C,D) -> evalEx4entryin.1(A,B,C,D) True evalEx4entryin.1(A,B,C,D) -> evalEx4bb4in.2(1,A,C,D) True evalEx4bb4in.2(A,B,C,D) -> evalEx4bb2in.5(A,B,0,B) [A = 1] evalEx4bb4in.2(A,B,C,D) -> evalEx4bb2in.6(A,B,0,B) [A = 1] evalEx4bb4in.3(A,B,C,D) -> evalEx4returnin.11(A,B,C,D) [0 >= A] evalEx4bb4in.4(A,B,C,D) -> evalEx4returnin.11(A,B,C,D) [A >= 2] evalEx4bb2in.5(A,B,C,D) -> evalEx4bb4in.2(C,D,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= D] evalEx4bb2in.5(A,B,C,D) -> evalEx4bb4in.3(C,D,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= D] evalEx4bb2in.5(A,B,C,D) -> evalEx4bb4in.4(C,D,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= D] evalEx4bb2in.6(A,B,C,D) -> evalEx4bb3in.7(A,B,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && D >= 1] evalEx4bb2in.6(A,B,C,D) -> evalEx4bb3in.8(A,B,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && D >= 1] evalEx4bb2in.6(A,B,C,D) -> evalEx4bb3in.9(A,B,C,D) [B + -1*D >= 0 && C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && D >= 1] evalEx4bb3in.7(A,B,C,D) -> evalEx4bb1in.10(A,B,C,D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= 1 + E] evalEx4bb3in.8(A,B,C,D) -> evalEx4bb1in.10(A,B,C,D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && E >= 1] evalEx4bb3in.9(A,B,C,D) -> evalEx4bb4in.2(C,D,C,D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] evalEx4bb3in.9(A,B,C,D) -> evalEx4bb4in.3(C,D,C,D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] evalEx4bb3in.9(A,B,C,D) -> evalEx4bb4in.4(C,D,C,D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] evalEx4bb1in.10(A,B,C,D) -> evalEx4bb2in.5(A,B,1,-1 + D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] evalEx4bb1in.10(A,B,C,D) -> evalEx4bb2in.6(A,B,1,-1 + D) [B + -1*D >= 0 && -1 + D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && -2 + A + D >= 0 && -1*A + D >= 0 && C >= 0 && -1 + B + C >= 0 && -1 + A + C >= 0 && 1 + -1*A + C >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0] evalEx4returnin.11(A,B,C,D) -> evalEx4stop.12(A,B,C,D) True evalEx4stop.12(A,B,C,D) -> exitus616(A,B,C,D) True evalEx4stop.12(A,B,C,D) -> exitus616(A,B,C,D) True evalEx4stop.12(A,B,C,D) -> exitus616(A,B,C,D) True evalEx4stop.12(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(evalEx4bb1in.10,4) ;(evalEx4bb2in.5,4) ;(evalEx4bb2in.6,4) ;(evalEx4bb3in.7,4) ;(evalEx4bb3in.8,4) ;(evalEx4bb3in.9,4) ;(evalEx4bb4in.2,4) ;(evalEx4bb4in.3,4) ;(evalEx4bb4in.4,4) ;(evalEx4entryin.1,4) ;(evalEx4returnin.11,4) ;(evalEx4start.0,4) ;(evalEx4stop.12,4) ;(exitus616,4)} Rule Graph: [0->{1},1->{2,3},2->{6,7,8},3->{9,10,11},4->{19},5->{19},6->{2,3},7->{4},8->{5},9->{12},10->{13},11->{14 ,15,16},12->{17,18},13->{17,18},14->{2,3},15->{4},16->{5},17->{6,7,8},18->{9,10,11},19->{20,21,22,23}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23] | `- p:[2,6,17,12,9,3,14,11,18,13,10] c: [9,10,11,12,13,14,17,18] | `- p:[2,6] c: [2,6]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,0.0,0.0.0] evalEx4start.0 ~> evalEx4entryin.1 [A <= A, B <= B, C <= C, D <= D] evalEx4entryin.1 ~> evalEx4bb4in.2 [A <= K, B <= A, C <= C, D <= D] evalEx4bb4in.2 ~> evalEx4bb2in.5 [A <= A, B <= B, C <= 0*K, D <= B] evalEx4bb4in.2 ~> evalEx4bb2in.6 [A <= A, B <= B, C <= 0*K, D <= B] evalEx4bb4in.3 ~> evalEx4returnin.11 [A <= A, B <= B, C <= C, D <= D] evalEx4bb4in.4 ~> evalEx4returnin.11 [A <= A, B <= B, C <= C, D <= D] evalEx4bb2in.5 ~> evalEx4bb4in.2 [A <= C, B <= D, C <= C, D <= D] evalEx4bb2in.5 ~> evalEx4bb4in.3 [A <= C, B <= D, C <= C, D <= D] evalEx4bb2in.5 ~> evalEx4bb4in.4 [A <= C, B <= D, C <= C, D <= D] evalEx4bb2in.6 ~> evalEx4bb3in.7 [A <= A, B <= B, C <= C, D <= D] evalEx4bb2in.6 ~> evalEx4bb3in.8 [A <= A, B <= B, C <= C, D <= D] evalEx4bb2in.6 ~> evalEx4bb3in.9 [A <= A, B <= B, C <= C, D <= D] evalEx4bb3in.7 ~> evalEx4bb1in.10 [A <= A, B <= B, C <= C, D <= D] evalEx4bb3in.8 ~> evalEx4bb1in.10 [A <= A, B <= B, C <= C, D <= D] evalEx4bb3in.9 ~> evalEx4bb4in.2 [A <= C, B <= D, C <= C, D <= D] evalEx4bb3in.9 ~> evalEx4bb4in.3 [A <= C, B <= D, C <= C, D <= D] evalEx4bb3in.9 ~> evalEx4bb4in.4 [A <= C, B <= D, C <= C, D <= D] evalEx4bb1in.10 ~> evalEx4bb2in.5 [A <= A, B <= B, C <= K, D <= D] evalEx4bb1in.10 ~> evalEx4bb2in.6 [A <= A, B <= B, C <= K, D <= D] evalEx4returnin.11 ~> evalEx4stop.12 [A <= A, B <= B, C <= C, D <= D] evalEx4stop.12 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] evalEx4stop.12 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] evalEx4stop.12 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] evalEx4stop.12 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= K + A + B] evalEx4bb4in.2 ~> evalEx4bb2in.5 [A <= A, B <= B, C <= 0*K, D <= B] evalEx4bb2in.5 ~> evalEx4bb4in.2 [A <= C, B <= D, C <= C, D <= D] evalEx4bb1in.10 ~> evalEx4bb2in.5 [A <= A, B <= B, C <= K, D <= D] evalEx4bb3in.7 ~> evalEx4bb1in.10 [A <= A, B <= B, C <= C, D <= D] evalEx4bb2in.6 ~> evalEx4bb3in.7 [A <= A, B <= B, C <= C, D <= D] evalEx4bb4in.2 ~> evalEx4bb2in.6 [A <= A, B <= B, C <= 0*K, D <= B] evalEx4bb3in.9 ~> evalEx4bb4in.2 [A <= C, B <= D, C <= C, D <= D] evalEx4bb2in.6 ~> evalEx4bb3in.9 [A <= A, B <= B, C <= C, D <= D] evalEx4bb1in.10 ~> evalEx4bb2in.6 [A <= A, B <= B, C <= K, D <= D] evalEx4bb3in.8 ~> evalEx4bb1in.10 [A <= A, B <= B, C <= C, D <= D] evalEx4bb2in.6 ~> evalEx4bb3in.8 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0.0 <= K + A + C] evalEx4bb4in.2 ~> evalEx4bb2in.5 [A <= A, B <= B, C <= 0*K, D <= B] evalEx4bb2in.5 ~> evalEx4bb4in.2 [A <= C, B <= D, 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] evalEx4start.0 ~> evalEx4entryin.1 [] evalEx4entryin.1 ~> evalEx4bb4in.2 [A ~=> B,K ~=> A] evalEx4bb4in.2 ~> evalEx4bb2in.5 [B ~=> D,K ~=> C] evalEx4bb4in.2 ~> evalEx4bb2in.6 [B ~=> D,K ~=> C] evalEx4bb4in.3 ~> evalEx4returnin.11 [] evalEx4bb4in.4 ~> evalEx4returnin.11 [] evalEx4bb2in.5 ~> evalEx4bb4in.2 [C ~=> A,D ~=> B] evalEx4bb2in.5 ~> evalEx4bb4in.3 [C ~=> A,D ~=> B] evalEx4bb2in.5 ~> evalEx4bb4in.4 [C ~=> A,D ~=> B] evalEx4bb2in.6 ~> evalEx4bb3in.7 [] evalEx4bb2in.6 ~> evalEx4bb3in.8 [] evalEx4bb2in.6 ~> evalEx4bb3in.9 [] evalEx4bb3in.7 ~> evalEx4bb1in.10 [] evalEx4bb3in.8 ~> evalEx4bb1in.10 [] evalEx4bb3in.9 ~> evalEx4bb4in.2 [C ~=> A,D ~=> B] evalEx4bb3in.9 ~> evalEx4bb4in.3 [C ~=> A,D ~=> B] evalEx4bb3in.9 ~> evalEx4bb4in.4 [C ~=> A,D ~=> B] evalEx4bb1in.10 ~> evalEx4bb2in.5 [K ~=> C] evalEx4bb1in.10 ~> evalEx4bb2in.6 [K ~=> C] evalEx4returnin.11 ~> evalEx4stop.12 [] evalEx4stop.12 ~> exitus616 [] evalEx4stop.12 ~> exitus616 [] evalEx4stop.12 ~> exitus616 [] evalEx4stop.12 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] evalEx4bb4in.2 ~> evalEx4bb2in.5 [B ~=> D,K ~=> C] evalEx4bb2in.5 ~> evalEx4bb4in.2 [C ~=> A,D ~=> B] evalEx4bb1in.10 ~> evalEx4bb2in.5 [K ~=> C] evalEx4bb3in.7 ~> evalEx4bb1in.10 [] evalEx4bb2in.6 ~> evalEx4bb3in.7 [] evalEx4bb4in.2 ~> evalEx4bb2in.6 [B ~=> D,K ~=> C] evalEx4bb3in.9 ~> evalEx4bb4in.2 [C ~=> A,D ~=> B] evalEx4bb2in.6 ~> evalEx4bb3in.9 [] evalEx4bb1in.10 ~> evalEx4bb2in.6 [K ~=> C] evalEx4bb3in.8 ~> evalEx4bb1in.10 [] evalEx4bb2in.6 ~> evalEx4bb3in.8 [] + Loop: [A ~+> 0.0.0,C ~+> 0.0.0,K ~+> 0.0.0] evalEx4bb4in.2 ~> evalEx4bb2in.5 [B ~=> D,K ~=> C] evalEx4bb2in.5 ~> evalEx4bb4in.2 [C ~=> A,D ~=> B] + Applied Processor: Lare + Details: evalEx4start.0 ~> exitus616 [A ~=> B ,A ~=> D ,C ~=> A ,D ~=> B ,K ~=> A ,K ~=> C ,A ~+> 0.0 ,A ~+> tick ,C ~+> 0.0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> tick ,C ~*> 0.0.0 ,C ~*> tick ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick] + evalEx4bb2in.5> [B ~=> D ,C ~=> A ,D ~=> B ,K ~=> A ,K ~=> C ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,C ~+> 0.0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> tick ,B ~*> tick ,C ~*> 0.0.0 ,C ~*> tick ,K ~*> 0.0.0 ,K ~*> tick] evalEx4bb3in.9> [B ~=> D ,C ~=> A ,D ~=> B ,K ~=> A ,K ~=> C ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,C ~+> 0.0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> tick ,B ~*> tick ,C ~*> 0.0.0 ,C ~*> tick ,K ~*> 0.0.0 ,K ~*> tick] + evalEx4bb2in.5> [C ~=> A ,D ~=> B ,K ~=> A ,K ~=> C ,A ~+> 0.0.0 ,A ~+> tick ,C ~+> 0.0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick] evalEx4bb4in.2> [C ~=> A ,D ~=> B ,K ~=> A ,K ~=> C ,A ~+> 0.0.0 ,A ~+> tick ,C ~+> 0.0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick] evalEx4bb2in.5> [B ~=> D ,K ~=> A ,K ~=> C ,A ~+> 0.0.0 ,A ~+> tick ,C ~+> 0.0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick] evalEx4bb4in.2> [B ~=> D ,K ~=> A ,K ~=> C ,A ~+> 0.0.0 ,A ~+> tick ,C ~+> 0.0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> tick] YES(?,POLY)