YES(?,POLY) * Step 1: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. eval0(A,B,C,D) -> eval1(B,B,1,D) True (1,1) 1. eval1(A,B,C,D) -> end(A,B,C,D) [1 + -1*C >= 0 && -1 + C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A >= 101] (?,1) 2. eval1(A,B,C,D) -> eval3(A,B,C,D) [1 + -1*C >= 0 && -1 + C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && 100 >= A] (?,1) 3. eval3(A,B,C,D) -> eval3(11 + A,B,1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && 100 + -1*B >= 0 && A + -1*B >= 0 && 100 >= A] (?,1) 4. eval3(A,B,C,D) -> eval5(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && 100 + -1*B >= 0 && A + -1*B >= 0 && A >= 101] (?,1) 5. eval5(A,B,C,D) -> eval7(-10 + A,B,-1 + C,D) [-1 + C >= 0 (?,1) && 99 + -1*B + C >= 0 && -102 + A + C >= 0 && 100 + -1*B >= 0 && -1 + A + -1*B >= 0 && -101 + A >= 0 && C >= 2] 6. eval7(A,B,C,D) -> eval5(A,B,C,-10 + A) [-1 + C >= 0 (?,1) && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && A >= 101 && C = 1] 7. eval7(A,B,C,D) -> eval9(A,B,C,D) [-1 + C >= 0 (?,1) && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && 100 >= A] 8. eval7(A,B,C,D) -> eval9(A,B,C,D) [-1 + C >= 0 (?,1) && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && 2 >= C] 9. eval7(A,B,C,D) -> eval9(A,B,C,D) [-1 + C >= 0 (?,1) && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && C >= 0] 10. eval9(A,B,C,D) -> eval11(-10 + A,B,-1 + C,D) [-1 + C >= 0 (?,1) && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && A >= 101] 11. eval9(A,B,C,D) -> eval11(A,B,C,D) [-1 + C >= 0 (?,1) && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && 100 >= A] 12. eval11(A,B,C,D) -> eval5(11 + A,B,1 + C,D) [C >= 0 && 100 + -1*B + C >= 0 && -91 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0] (?,1) Signature: {(end,4);(eval0,4);(eval1,4);(eval11,4);(eval3,4);(eval5,4);(eval7,4);(eval9,4)} Flow Graph: [0->{1,2},1->{},2->{3,4},3->{3,4},4->{5},5->{6,7,8,9},6->{5},7->{10,11},8->{10,11},9->{10,11},10->{12} ,11->{12},12->{5}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,4),(6,5),(7,10)] * Step 2: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. eval0(A,B,C,D) -> eval1(B,B,1,D) True (1,1) 1. eval1(A,B,C,D) -> end(A,B,C,D) [1 + -1*C >= 0 && -1 + C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A >= 101] (?,1) 2. eval1(A,B,C,D) -> eval3(A,B,C,D) [1 + -1*C >= 0 && -1 + C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && 100 >= A] (?,1) 3. eval3(A,B,C,D) -> eval3(11 + A,B,1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && 100 + -1*B >= 0 && A + -1*B >= 0 && 100 >= A] (?,1) 4. eval3(A,B,C,D) -> eval5(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && 100 + -1*B >= 0 && A + -1*B >= 0 && A >= 101] (?,1) 5. eval5(A,B,C,D) -> eval7(-10 + A,B,-1 + C,D) [-1 + C >= 0 (?,1) && 99 + -1*B + C >= 0 && -102 + A + C >= 0 && 100 + -1*B >= 0 && -1 + A + -1*B >= 0 && -101 + A >= 0 && C >= 2] 6. eval7(A,B,C,D) -> eval5(A,B,C,-10 + A) [-1 + C >= 0 (?,1) && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && A >= 101 && C = 1] 7. eval7(A,B,C,D) -> eval9(A,B,C,D) [-1 + C >= 0 (?,1) && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && 100 >= A] 8. eval7(A,B,C,D) -> eval9(A,B,C,D) [-1 + C >= 0 (?,1) && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && 2 >= C] 9. eval7(A,B,C,D) -> eval9(A,B,C,D) [-1 + C >= 0 (?,1) && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && C >= 0] 10. eval9(A,B,C,D) -> eval11(-10 + A,B,-1 + C,D) [-1 + C >= 0 (?,1) && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && A >= 101] 11. eval9(A,B,C,D) -> eval11(A,B,C,D) [-1 + C >= 0 (?,1) && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && 100 >= A] 12. eval11(A,B,C,D) -> eval5(11 + A,B,1 + C,D) [C >= 0 && 100 + -1*B + C >= 0 && -91 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0] (?,1) Signature: {(end,4);(eval0,4);(eval1,4);(eval11,4);(eval3,4);(eval5,4);(eval7,4);(eval9,4)} Flow Graph: [0->{1,2},1->{},2->{3},3->{3,4},4->{5},5->{6,7,8,9},6->{},7->{11},8->{10,11},9->{10,11},10->{12},11->{12} ,12->{5}] + Applied Processor: FromIts + Details: () * Step 3: Unfold WORST_CASE(?,POLY) + Considered Problem: Rules: eval0(A,B,C,D) -> eval1(B,B,1,D) True eval1(A,B,C,D) -> end(A,B,C,D) [1 + -1*C >= 0 && -1 + C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A >= 101] eval1(A,B,C,D) -> eval3(A,B,C,D) [1 + -1*C >= 0 && -1 + C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && 100 >= A] eval3(A,B,C,D) -> eval3(11 + A,B,1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && 100 + -1*B >= 0 && A + -1*B >= 0 && 100 >= A] eval3(A,B,C,D) -> eval5(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && 100 + -1*B >= 0 && A + -1*B >= 0 && A >= 101] eval5(A,B,C,D) -> eval7(-10 + A,B,-1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -102 + A + C >= 0 && 100 + -1*B >= 0 && -1 + A + -1*B >= 0 && -101 + A >= 0 && C >= 2] eval7(A,B,C,D) -> eval5(A,B,C,-10 + A) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && A >= 101 && C = 1] eval7(A,B,C,D) -> eval9(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && 100 >= A] eval7(A,B,C,D) -> eval9(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && 2 >= C] eval7(A,B,C,D) -> eval9(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && C >= 0] eval9(A,B,C,D) -> eval11(-10 + A,B,-1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && A >= 101] eval9(A,B,C,D) -> eval11(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && 100 >= A] eval11(A,B,C,D) -> eval5(11 + A,B,1 + C,D) [C >= 0 && 100 + -1*B + C >= 0 && -91 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0] Signature: {(end,4);(eval0,4);(eval1,4);(eval11,4);(eval3,4);(eval5,4);(eval7,4);(eval9,4)} Rule Graph: [0->{1,2},1->{},2->{3},3->{3,4},4->{5},5->{6,7,8,9},6->{},7->{11},8->{10,11},9->{10,11},10->{12},11->{12} ,12->{5}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: eval0.0(A,B,C,D) -> eval1.1(B,B,1,D) True eval0.0(A,B,C,D) -> eval1.2(B,B,1,D) True eval1.1(A,B,C,D) -> end.13(A,B,C,D) [1 + -1*C >= 0 && -1 + C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A >= 101] eval1.2(A,B,C,D) -> eval3.3(A,B,C,D) [1 + -1*C >= 0 && -1 + C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && 100 >= A] eval3.3(A,B,C,D) -> eval3.3(11 + A,B,1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && 100 + -1*B >= 0 && A + -1*B >= 0 && 100 >= A] eval3.3(A,B,C,D) -> eval3.4(11 + A,B,1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && 100 + -1*B >= 0 && A + -1*B >= 0 && 100 >= A] eval3.4(A,B,C,D) -> eval5.5(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && 100 + -1*B >= 0 && A + -1*B >= 0 && A >= 101] eval5.5(A,B,C,D) -> eval7.6(-10 + A,B,-1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -102 + A + C >= 0 && 100 + -1*B >= 0 && -1 + A + -1*B >= 0 && -101 + A >= 0 && C >= 2] eval5.5(A,B,C,D) -> eval7.7(-10 + A,B,-1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -102 + A + C >= 0 && 100 + -1*B >= 0 && -1 + A + -1*B >= 0 && -101 + A >= 0 && C >= 2] eval5.5(A,B,C,D) -> eval7.8(-10 + A,B,-1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -102 + A + C >= 0 && 100 + -1*B >= 0 && -1 + A + -1*B >= 0 && -101 + A >= 0 && C >= 2] eval5.5(A,B,C,D) -> eval7.9(-10 + A,B,-1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -102 + A + C >= 0 && 100 + -1*B >= 0 && -1 + A + -1*B >= 0 && -101 + A >= 0 && C >= 2] eval7.6(A,B,C,D) -> eval5.13(A,B,C,-10 + A) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && A >= 101 && C = 1] eval7.7(A,B,C,D) -> eval9.11(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && 100 >= A] eval7.8(A,B,C,D) -> eval9.10(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && 2 >= C] eval7.8(A,B,C,D) -> eval9.11(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && 2 >= C] eval7.9(A,B,C,D) -> eval9.10(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && C >= 0] eval7.9(A,B,C,D) -> eval9.11(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && C >= 0] eval9.10(A,B,C,D) -> eval11.12(-10 + A,B,-1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && A >= 101] eval9.11(A,B,C,D) -> eval11.12(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && 100 >= A] eval11.12(A,B,C,D) -> eval5.5(11 + A,B,1 + C,D) [C >= 0 && 100 + -1*B + C >= 0 && -91 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0] Signature: {(end.13,4) ;(eval0.0,4) ;(eval1.1,4) ;(eval1.2,4) ;(eval11.12,4) ;(eval3.3,4) ;(eval3.4,4) ;(eval5.13,4) ;(eval5.5,4) ;(eval7.6,4) ;(eval7.7,4) ;(eval7.8,4) ;(eval7.9,4) ;(eval9.10,4) ;(eval9.11,4)} Rule Graph: [0->{2},1->{3},2->{},3->{4,5},4->{4,5},5->{6},6->{7,8,9,10},7->{11},8->{12},9->{13,14},10->{15,16},11->{} ,12->{18},13->{17},14->{18},15->{17},16->{18},17->{19},18->{19},19->{7,8,9,10}] + Applied Processor: AddSinks + Details: () * Step 5: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: eval0.0(A,B,C,D) -> eval1.1(B,B,1,D) True eval0.0(A,B,C,D) -> eval1.2(B,B,1,D) True eval1.1(A,B,C,D) -> end.13(A,B,C,D) [1 + -1*C >= 0 && -1 + C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A >= 101] eval1.2(A,B,C,D) -> eval3.3(A,B,C,D) [1 + -1*C >= 0 && -1 + C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && 100 >= A] eval3.3(A,B,C,D) -> eval3.3(11 + A,B,1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && 100 + -1*B >= 0 && A + -1*B >= 0 && 100 >= A] eval3.3(A,B,C,D) -> eval3.4(11 + A,B,1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && 100 + -1*B >= 0 && A + -1*B >= 0 && 100 >= A] eval3.4(A,B,C,D) -> eval5.5(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && 100 + -1*B >= 0 && A + -1*B >= 0 && A >= 101] eval5.5(A,B,C,D) -> eval7.6(-10 + A,B,-1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -102 + A + C >= 0 && 100 + -1*B >= 0 && -1 + A + -1*B >= 0 && -101 + A >= 0 && C >= 2] eval5.5(A,B,C,D) -> eval7.7(-10 + A,B,-1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -102 + A + C >= 0 && 100 + -1*B >= 0 && -1 + A + -1*B >= 0 && -101 + A >= 0 && C >= 2] eval5.5(A,B,C,D) -> eval7.8(-10 + A,B,-1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -102 + A + C >= 0 && 100 + -1*B >= 0 && -1 + A + -1*B >= 0 && -101 + A >= 0 && C >= 2] eval5.5(A,B,C,D) -> eval7.9(-10 + A,B,-1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -102 + A + C >= 0 && 100 + -1*B >= 0 && -1 + A + -1*B >= 0 && -101 + A >= 0 && C >= 2] eval7.6(A,B,C,D) -> eval5.13(A,B,C,-10 + A) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && A >= 101 && C = 1] eval7.7(A,B,C,D) -> eval9.11(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && 100 >= A] eval7.8(A,B,C,D) -> eval9.10(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && 2 >= C] eval7.8(A,B,C,D) -> eval9.11(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && 2 >= C] eval7.9(A,B,C,D) -> eval9.10(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && C >= 0] eval7.9(A,B,C,D) -> eval9.11(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && C >= 0] eval9.10(A,B,C,D) -> eval11.12(-10 + A,B,-1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && A >= 101] eval9.11(A,B,C,D) -> eval11.12(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && 100 >= A] eval11.12(A,B,C,D) -> eval5.5(11 + A,B,1 + C,D) [C >= 0 && 100 + -1*B + C >= 0 && -91 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0] eval5.13(A,B,C,D) -> exitus616(A,B,C,D) True end.13(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(end.13,4) ;(eval0.0,4) ;(eval1.1,4) ;(eval1.2,4) ;(eval11.12,4) ;(eval3.3,4) ;(eval3.4,4) ;(eval5.13,4) ;(eval5.5,4) ;(eval7.6,4) ;(eval7.7,4) ;(eval7.8,4) ;(eval7.9,4) ;(eval9.10,4) ;(eval9.11,4) ;(exitus616,4)} Rule Graph: [0->{2},1->{3},2->{21},3->{4,5},4->{4,5},5->{6},6->{7,8,9,10},7->{11},8->{12},9->{13,14},10->{15,16} ,11->{20},12->{18},13->{17},14->{18},15->{17},16->{18},17->{19},18->{19},19->{7,8,9,10}] + 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] | +- p:[4] c: [4] | `- p:[8,19,17,13,9,15,10,18,12,14,16] c: [8,9,10,12,13,14,15,16,17,18,19] * Step 6: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: eval0.0(A,B,C,D) -> eval1.1(B,B,1,D) True eval0.0(A,B,C,D) -> eval1.2(B,B,1,D) True eval1.1(A,B,C,D) -> end.13(A,B,C,D) [1 + -1*C >= 0 && -1 + C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A >= 101] eval1.2(A,B,C,D) -> eval3.3(A,B,C,D) [1 + -1*C >= 0 && -1 + C >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && 100 >= A] eval3.3(A,B,C,D) -> eval3.3(11 + A,B,1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && 100 + -1*B >= 0 && A + -1*B >= 0 && 100 >= A] eval3.3(A,B,C,D) -> eval3.4(11 + A,B,1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && 100 + -1*B >= 0 && A + -1*B >= 0 && 100 >= A] eval3.4(A,B,C,D) -> eval5.5(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && 100 + -1*B >= 0 && A + -1*B >= 0 && A >= 101] eval5.5(A,B,C,D) -> eval7.6(-10 + A,B,-1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -102 + A + C >= 0 && 100 + -1*B >= 0 && -1 + A + -1*B >= 0 && -101 + A >= 0 && C >= 2] eval5.5(A,B,C,D) -> eval7.7(-10 + A,B,-1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -102 + A + C >= 0 && 100 + -1*B >= 0 && -1 + A + -1*B >= 0 && -101 + A >= 0 && C >= 2] eval5.5(A,B,C,D) -> eval7.8(-10 + A,B,-1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -102 + A + C >= 0 && 100 + -1*B >= 0 && -1 + A + -1*B >= 0 && -101 + A >= 0 && C >= 2] eval5.5(A,B,C,D) -> eval7.9(-10 + A,B,-1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -102 + A + C >= 0 && 100 + -1*B >= 0 && -1 + A + -1*B >= 0 && -101 + A >= 0 && C >= 2] eval7.6(A,B,C,D) -> eval5.13(A,B,C,-10 + A) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && A >= 101 && C = 1] eval7.7(A,B,C,D) -> eval9.11(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && 100 >= A] eval7.8(A,B,C,D) -> eval9.10(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && 2 >= C] eval7.8(A,B,C,D) -> eval9.11(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && 2 >= C] eval7.9(A,B,C,D) -> eval9.10(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && C >= 0] eval7.9(A,B,C,D) -> eval9.11(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && C >= 0] eval9.10(A,B,C,D) -> eval11.12(-10 + A,B,-1 + C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && A >= 101] eval9.11(A,B,C,D) -> eval11.12(A,B,C,D) [-1 + C >= 0 && 99 + -1*B + C >= 0 && -92 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0 && 100 >= A] eval11.12(A,B,C,D) -> eval5.5(11 + A,B,1 + C,D) [C >= 0 && 100 + -1*B + C >= 0 && -91 + A + C >= 0 && 100 + -1*B >= 0 && 9 + A + -1*B >= 0 && -91 + A >= 0] eval5.13(A,B,C,D) -> exitus616(A,B,C,D) True end.13(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(end.13,4) ;(eval0.0,4) ;(eval1.1,4) ;(eval1.2,4) ;(eval11.12,4) ;(eval3.3,4) ;(eval3.4,4) ;(eval5.13,4) ;(eval5.5,4) ;(eval7.6,4) ;(eval7.7,4) ;(eval7.8,4) ;(eval7.9,4) ;(eval9.10,4) ;(eval9.11,4) ;(exitus616,4)} Rule Graph: [0->{2},1->{3},2->{21},3->{4,5},4->{4,5},5->{6},6->{7,8,9,10},7->{11},8->{12},9->{13,14},10->{15,16} ,11->{20},12->{18},13->{17},14->{18},15->{17},16->{18},17->{19},18->{19},19->{7,8,9,10}] ,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] | +- p:[4] c: [4] | `- p:[8,19,17,13,9,15,10,18,12,14,16] c: [8,9,10,12,13,14,15,16,17,18,19]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,0.0,0.1] eval0.0 ~> eval1.1 [A <= B, B <= B, C <= K, D <= D] eval0.0 ~> eval1.2 [A <= B, B <= B, C <= K, D <= D] eval1.1 ~> end.13 [A <= A, B <= B, C <= C, D <= D] eval1.2 ~> eval3.3 [A <= A, B <= B, C <= C, D <= D] eval3.3 ~> eval3.3 [A <= 10*K + A + C, B <= B, C <= K + C, D <= D] eval3.3 ~> eval3.4 [A <= 10*K + A + C, B <= B, C <= K + C, D <= D] eval3.4 ~> eval5.5 [A <= A, B <= B, C <= C, D <= D] eval5.5 ~> eval7.6 [A <= A, B <= B, C <= C, D <= D] eval5.5 ~> eval7.7 [A <= A, B <= B, C <= C, D <= D] eval5.5 ~> eval7.8 [A <= A, B <= B, C <= C, D <= D] eval5.5 ~> eval7.9 [A <= A, B <= B, C <= C, D <= D] eval7.6 ~> eval5.13 [A <= A, B <= B, C <= C, D <= A] eval7.7 ~> eval9.11 [A <= A, B <= B, C <= C, D <= D] eval7.8 ~> eval9.10 [A <= A, B <= B, C <= C, D <= D] eval7.8 ~> eval9.11 [A <= A, B <= B, C <= C, D <= D] eval7.9 ~> eval9.10 [A <= A, B <= B, C <= C, D <= D] eval7.9 ~> eval9.11 [A <= A, B <= B, C <= C, D <= D] eval9.10 ~> eval11.12 [A <= A, B <= B, C <= C, D <= D] eval9.11 ~> eval11.12 [A <= A, B <= B, C <= C, D <= D] eval11.12 ~> eval5.5 [A <= 11*K + A, B <= B, C <= A + C, D <= D] eval5.13 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] end.13 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= 200*K + A + B] eval3.3 ~> eval3.3 [A <= 10*K + A + C, B <= B, C <= K + C, D <= D] + Loop: [0.1 <= 92*K + A + 9*C] eval5.5 ~> eval7.7 [A <= A, B <= B, C <= C, D <= D] eval11.12 ~> eval5.5 [A <= 11*K + A, B <= B, C <= A + C, D <= D] eval9.10 ~> eval11.12 [A <= A, B <= B, C <= C, D <= D] eval7.8 ~> eval9.10 [A <= A, B <= B, C <= C, D <= D] eval5.5 ~> eval7.8 [A <= A, B <= B, C <= C, D <= D] eval7.9 ~> eval9.10 [A <= A, B <= B, C <= C, D <= D] eval5.5 ~> eval7.9 [A <= A, B <= B, C <= C, D <= D] eval9.11 ~> eval11.12 [A <= A, B <= B, C <= C, D <= D] eval7.7 ~> eval9.11 [A <= A, B <= B, C <= C, D <= D] eval7.8 ~> eval9.11 [A <= A, B <= B, C <= C, D <= D] eval7.9 ~> eval9.11 [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.1] eval0.0 ~> eval1.1 [B ~=> A,K ~=> C] eval0.0 ~> eval1.2 [B ~=> A,K ~=> C] eval1.1 ~> end.13 [] eval1.2 ~> eval3.3 [] eval3.3 ~> eval3.3 [A ~+> A,C ~+> A,C ~+> C,K ~+> C,K ~*> A] eval3.3 ~> eval3.4 [A ~+> A,C ~+> A,C ~+> C,K ~+> C,K ~*> A] eval3.4 ~> eval5.5 [] eval5.5 ~> eval7.6 [] eval5.5 ~> eval7.7 [] eval5.5 ~> eval7.8 [] eval5.5 ~> eval7.9 [] eval7.6 ~> eval5.13 [A ~=> D] eval7.7 ~> eval9.11 [] eval7.8 ~> eval9.10 [] eval7.8 ~> eval9.11 [] eval7.9 ~> eval9.10 [] eval7.9 ~> eval9.11 [] eval9.10 ~> eval11.12 [] eval9.11 ~> eval11.12 [] eval11.12 ~> eval5.5 [A ~+> A,A ~+> C,C ~+> C,K ~*> A] eval5.13 ~> exitus616 [] end.13 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~*> 0.0] eval3.3 ~> eval3.3 [A ~+> A,C ~+> A,C ~+> C,K ~+> C,K ~*> A] + Loop: [A ~+> 0.1,C ~*> 0.1,K ~*> 0.1] eval5.5 ~> eval7.7 [] eval11.12 ~> eval5.5 [A ~+> A,A ~+> C,C ~+> C,K ~*> A] eval9.10 ~> eval11.12 [] eval7.8 ~> eval9.10 [] eval5.5 ~> eval7.8 [] eval7.9 ~> eval9.10 [] eval5.5 ~> eval7.9 [] eval9.11 ~> eval11.12 [] eval7.7 ~> eval9.11 [] eval7.8 ~> eval9.11 [] eval7.9 ~> eval9.11 [] + Applied Processor: Lare + Details: eval0.0 ~> exitus616 [B ~=> A ,K ~=> C ,B ~+> A ,B ~+> C ,B ~+> D ,B ~+> 0.0 ,B ~+> 0.1 ,B ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> C ,K ~+> D ,K ~+> 0.1 ,K ~+> tick ,B ~*> A ,B ~*> C ,B ~*> D ,B ~*> 0.0 ,B ~*> 0.1 ,B ~*> tick ,K ~*> A ,K ~*> C ,K ~*> D ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> tick] + eval3.3> [A ~+> A ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,C ~+> A ,C ~+> C ,tick ~+> tick ,K ~+> A ,K ~+> C ,A ~*> A ,A ~*> C ,B ~*> A ,B ~*> C ,C ~*> A ,K ~*> A ,K ~*> C ,K ~*> 0.0 ,K ~*> tick] + eval5.5> [A ~+> A ,A ~+> C ,A ~+> 0.1 ,A ~+> tick ,C ~+> C ,tick ~+> tick ,A ~*> A ,A ~*> C ,C ~*> A ,C ~*> C ,C ~*> 0.1 ,C ~*> tick ,K ~*> A ,K ~*> C ,K ~*> 0.1 ,K ~*> tick] YES(?,POLY)