YES(?,O(n^1)) * Step 1: UnsatPaths WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalwisestart(A,B) -> evalwiseentryin(A,B) True (1,1) 1. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + A] (?,1) 2. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + B] (?,1) 3. evalwiseentryin(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (?,1) 4. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 0 && A + B >= 0 && A >= 0 && B >= 3 + A] (?,1) 5. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 0 && A + B >= 0 && A >= 0 && A >= 3 + B] (?,1) 6. evalwisebb6in(A,B) -> evalwisereturnin(A,B) [B >= 0 && A + B >= 0 && A >= 0 && 2 + A >= B && 2 + B >= A] (?,1) 7. evalwisebb3in(A,B) -> evalwisebb4in(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && A >= 1 + B] (?,1) 8. evalwisebb3in(A,B) -> evalwisebb5in(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && B >= A] (?,1) 9. evalwisebb4in(A,B) -> evalwisebb6in(A,1 + B) [-1 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] (?,1) 10. evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -1*A + B >= 0 && A >= 0] (?,1) 11. evalwisereturnin(A,B) -> evalwisestop(A,B) True (?,1) Signature: {(evalwisebb3in,2) ;(evalwisebb4in,2) ;(evalwisebb5in,2) ;(evalwisebb6in,2) ;(evalwiseentryin,2) ;(evalwisereturnin,2) ;(evalwisestart,2) ;(evalwisestop,2)} Flow Graph: [0->{1,2,3},1->{11},2->{11},3->{4,5,6},4->{7,8},5->{7,8},6->{11},7->{9},8->{10},9->{4,5,6},10->{4,5,6} ,11->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(4,7),(5,8),(9,4),(10,5)] * Step 2: FromIts WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalwisestart(A,B) -> evalwiseentryin(A,B) True (1,1) 1. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + A] (?,1) 2. evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + B] (?,1) 3. evalwiseentryin(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] (?,1) 4. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 0 && A + B >= 0 && A >= 0 && B >= 3 + A] (?,1) 5. evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 0 && A + B >= 0 && A >= 0 && A >= 3 + B] (?,1) 6. evalwisebb6in(A,B) -> evalwisereturnin(A,B) [B >= 0 && A + B >= 0 && A >= 0 && 2 + A >= B && 2 + B >= A] (?,1) 7. evalwisebb3in(A,B) -> evalwisebb4in(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && A >= 1 + B] (?,1) 8. evalwisebb3in(A,B) -> evalwisebb5in(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && B >= A] (?,1) 9. evalwisebb4in(A,B) -> evalwisebb6in(A,1 + B) [-1 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] (?,1) 10. evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -1*A + B >= 0 && A >= 0] (?,1) 11. evalwisereturnin(A,B) -> evalwisestop(A,B) True (?,1) Signature: {(evalwisebb3in,2) ;(evalwisebb4in,2) ;(evalwisebb5in,2) ;(evalwisebb6in,2) ;(evalwiseentryin,2) ;(evalwisereturnin,2) ;(evalwisestart,2) ;(evalwisestop,2)} Flow Graph: [0->{1,2,3},1->{11},2->{11},3->{4,5,6},4->{8},5->{7},6->{11},7->{9},8->{10},9->{5,6},10->{4,6},11->{}] + Applied Processor: FromIts + Details: () * Step 3: AddSinks WORST_CASE(?,O(n^1)) + Considered Problem: Rules: evalwisestart(A,B) -> evalwiseentryin(A,B) True evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + A] evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + B] evalwiseentryin(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 0 && A + B >= 0 && A >= 0 && B >= 3 + A] evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 0 && A + B >= 0 && A >= 0 && A >= 3 + B] evalwisebb6in(A,B) -> evalwisereturnin(A,B) [B >= 0 && A + B >= 0 && A >= 0 && 2 + A >= B && 2 + B >= A] evalwisebb3in(A,B) -> evalwisebb4in(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && A >= 1 + B] evalwisebb3in(A,B) -> evalwisebb5in(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && B >= A] evalwisebb4in(A,B) -> evalwisebb6in(A,1 + B) [-1 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -1*A + B >= 0 && A >= 0] evalwisereturnin(A,B) -> evalwisestop(A,B) True Signature: {(evalwisebb3in,2) ;(evalwisebb4in,2) ;(evalwisebb5in,2) ;(evalwisebb6in,2) ;(evalwiseentryin,2) ;(evalwisereturnin,2) ;(evalwisestart,2) ;(evalwisestop,2)} Rule Graph: [0->{1,2,3},1->{11},2->{11},3->{4,5,6},4->{8},5->{7},6->{11},7->{9},8->{10},9->{5,6},10->{4,6},11->{}] + Applied Processor: AddSinks + Details: () * Step 4: Unfold WORST_CASE(?,O(n^1)) + Considered Problem: Rules: evalwisestart(A,B) -> evalwiseentryin(A,B) True evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + A] evalwiseentryin(A,B) -> evalwisereturnin(A,B) [0 >= 1 + B] evalwiseentryin(A,B) -> evalwisebb6in(B,A) [A >= 0 && B >= 0] evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 0 && A + B >= 0 && A >= 0 && B >= 3 + A] evalwisebb6in(A,B) -> evalwisebb3in(A,B) [B >= 0 && A + B >= 0 && A >= 0 && A >= 3 + B] evalwisebb6in(A,B) -> evalwisereturnin(A,B) [B >= 0 && A + B >= 0 && A >= 0 && 2 + A >= B && 2 + B >= A] evalwisebb3in(A,B) -> evalwisebb4in(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && A >= 1 + B] evalwisebb3in(A,B) -> evalwisebb5in(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && B >= A] evalwisebb4in(A,B) -> evalwisebb6in(A,1 + B) [-1 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] evalwisebb5in(A,B) -> evalwisebb6in(1 + A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -1*A + B >= 0 && A >= 0] evalwisereturnin(A,B) -> evalwisestop(A,B) True evalwisestop(A,B) -> exitus616(A,B) True evalwisestop(A,B) -> exitus616(A,B) True evalwisestop(A,B) -> exitus616(A,B) True evalwisestop(A,B) -> exitus616(A,B) True Signature: {(evalwisebb3in,2) ;(evalwisebb4in,2) ;(evalwisebb5in,2) ;(evalwisebb6in,2) ;(evalwiseentryin,2) ;(evalwisereturnin,2) ;(evalwisestart,2) ;(evalwisestop,2) ;(exitus616,2)} Rule Graph: [0->{1,2,3},1->{11},2->{11},3->{4,5,6},4->{8},5->{7},6->{11},7->{9},8->{10},9->{5,6},10->{4,6},11->{12,13 ,14,15}] + Applied Processor: Unfold + Details: () * Step 5: Decompose WORST_CASE(?,O(n^1)) + Considered Problem: Rules: evalwisestart.0(A,B) -> evalwiseentryin.1(A,B) True evalwisestart.0(A,B) -> evalwiseentryin.2(A,B) True evalwisestart.0(A,B) -> evalwiseentryin.3(A,B) True evalwiseentryin.1(A,B) -> evalwisereturnin.11(A,B) [0 >= 1 + A] evalwiseentryin.2(A,B) -> evalwisereturnin.11(A,B) [0 >= 1 + B] evalwiseentryin.3(A,B) -> evalwisebb6in.4(B,A) [A >= 0 && B >= 0] evalwiseentryin.3(A,B) -> evalwisebb6in.5(B,A) [A >= 0 && B >= 0] evalwiseentryin.3(A,B) -> evalwisebb6in.6(B,A) [A >= 0 && B >= 0] evalwisebb6in.4(A,B) -> evalwisebb3in.8(A,B) [B >= 0 && A + B >= 0 && A >= 0 && B >= 3 + A] evalwisebb6in.5(A,B) -> evalwisebb3in.7(A,B) [B >= 0 && A + B >= 0 && A >= 0 && A >= 3 + B] evalwisebb6in.6(A,B) -> evalwisereturnin.11(A,B) [B >= 0 && A + B >= 0 && A >= 0 && 2 + A >= B && 2 + B >= A] evalwisebb3in.7(A,B) -> evalwisebb4in.9(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && A >= 1 + B] evalwisebb3in.8(A,B) -> evalwisebb5in.10(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && B >= A] evalwisebb4in.9(A,B) -> evalwisebb6in.5(A,1 + B) [-1 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] evalwisebb4in.9(A,B) -> evalwisebb6in.6(A,1 + B) [-1 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] evalwisebb5in.10(A,B) -> evalwisebb6in.4(1 + A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -1*A + B >= 0 && A >= 0] evalwisebb5in.10(A,B) -> evalwisebb6in.6(1 + A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -1*A + B >= 0 && A >= 0] evalwisereturnin.11(A,B) -> evalwisestop.12(A,B) True evalwisereturnin.11(A,B) -> evalwisestop.13(A,B) True evalwisereturnin.11(A,B) -> evalwisestop.14(A,B) True evalwisereturnin.11(A,B) -> evalwisestop.15(A,B) True evalwisestop.12(A,B) -> exitus616.16(A,B) True evalwisestop.13(A,B) -> exitus616.16(A,B) True evalwisestop.14(A,B) -> exitus616.16(A,B) True evalwisestop.15(A,B) -> exitus616.16(A,B) True Signature: {(evalwisebb3in.7,2) ;(evalwisebb3in.8,2) ;(evalwisebb4in.9,2) ;(evalwisebb5in.10,2) ;(evalwisebb6in.4,2) ;(evalwisebb6in.5,2) ;(evalwisebb6in.6,2) ;(evalwiseentryin.1,2) ;(evalwiseentryin.2,2) ;(evalwiseentryin.3,2) ;(evalwisereturnin.11,2) ;(evalwisestart.0,2) ;(evalwisestop.12,2) ;(evalwisestop.13,2) ;(evalwisestop.14,2) ;(evalwisestop.15,2) ;(exitus616.16,2)} Rule Graph: [0->{3},1->{4},2->{5,6,7},3->{17,18,19,20},4->{17,18,19,20},5->{8},6->{9},7->{10},8->{12},9->{11},10->{17 ,18,19,20},11->{13,14},12->{15,16},13->{9},14->{10},15->{8},16->{10},17->{21},18->{22},19->{23},20->{24} ,21->{},22->{},23->{},24->{}] + 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] | +- p:[9,13,11] c: [9,11,13] | `- p:[8,15,12] c: [8,12,15] * Step 6: AbstractSize WORST_CASE(?,O(n^1)) + Considered Problem: (Rules: evalwisestart.0(A,B) -> evalwiseentryin.1(A,B) True evalwisestart.0(A,B) -> evalwiseentryin.2(A,B) True evalwisestart.0(A,B) -> evalwiseentryin.3(A,B) True evalwiseentryin.1(A,B) -> evalwisereturnin.11(A,B) [0 >= 1 + A] evalwiseentryin.2(A,B) -> evalwisereturnin.11(A,B) [0 >= 1 + B] evalwiseentryin.3(A,B) -> evalwisebb6in.4(B,A) [A >= 0 && B >= 0] evalwiseentryin.3(A,B) -> evalwisebb6in.5(B,A) [A >= 0 && B >= 0] evalwiseentryin.3(A,B) -> evalwisebb6in.6(B,A) [A >= 0 && B >= 0] evalwisebb6in.4(A,B) -> evalwisebb3in.8(A,B) [B >= 0 && A + B >= 0 && A >= 0 && B >= 3 + A] evalwisebb6in.5(A,B) -> evalwisebb3in.7(A,B) [B >= 0 && A + B >= 0 && A >= 0 && A >= 3 + B] evalwisebb6in.6(A,B) -> evalwisereturnin.11(A,B) [B >= 0 && A + B >= 0 && A >= 0 && 2 + A >= B && 2 + B >= A] evalwisebb3in.7(A,B) -> evalwisebb4in.9(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && A >= 1 + B] evalwisebb3in.8(A,B) -> evalwisebb5in.10(A,B) [B >= 0 && -3 + A + B >= 0 && A >= 0 && B >= A] evalwisebb4in.9(A,B) -> evalwisebb6in.5(A,1 + B) [-1 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] evalwisebb4in.9(A,B) -> evalwisebb6in.6(A,1 + B) [-1 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -2 + A >= 0] evalwisebb5in.10(A,B) -> evalwisebb6in.4(1 + A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -1*A + B >= 0 && A >= 0] evalwisebb5in.10(A,B) -> evalwisebb6in.6(1 + A,B) [-1 + B >= 0 && -3 + A + B >= 0 && -1*A + B >= 0 && A >= 0] evalwisereturnin.11(A,B) -> evalwisestop.12(A,B) True evalwisereturnin.11(A,B) -> evalwisestop.13(A,B) True evalwisereturnin.11(A,B) -> evalwisestop.14(A,B) True evalwisereturnin.11(A,B) -> evalwisestop.15(A,B) True evalwisestop.12(A,B) -> exitus616.16(A,B) True evalwisestop.13(A,B) -> exitus616.16(A,B) True evalwisestop.14(A,B) -> exitus616.16(A,B) True evalwisestop.15(A,B) -> exitus616.16(A,B) True Signature: {(evalwisebb3in.7,2) ;(evalwisebb3in.8,2) ;(evalwisebb4in.9,2) ;(evalwisebb5in.10,2) ;(evalwisebb6in.4,2) ;(evalwisebb6in.5,2) ;(evalwisebb6in.6,2) ;(evalwiseentryin.1,2) ;(evalwiseentryin.2,2) ;(evalwiseentryin.3,2) ;(evalwisereturnin.11,2) ;(evalwisestart.0,2) ;(evalwisestop.12,2) ;(evalwisestop.13,2) ;(evalwisestop.14,2) ;(evalwisestop.15,2) ;(exitus616.16,2)} Rule Graph: [0->{3},1->{4},2->{5,6,7},3->{17,18,19,20},4->{17,18,19,20},5->{8},6->{9},7->{10},8->{12},9->{11},10->{17 ,18,19,20},11->{13,14},12->{15,16},13->{9},14->{10},15->{8},16->{10},17->{21},18->{22},19->{23},20->{24} ,21->{},22->{},23->{},24->{}] ,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] | +- p:[9,13,11] c: [9,11,13] | `- p:[8,15,12] c: [8,12,15]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [A,B,0.0,0.1] evalwisestart.0 ~> evalwiseentryin.1 [A <= A, B <= B] evalwisestart.0 ~> evalwiseentryin.2 [A <= A, B <= B] evalwisestart.0 ~> evalwiseentryin.3 [A <= A, B <= B] evalwiseentryin.1 ~> evalwisereturnin.11 [A <= A, B <= B] evalwiseentryin.2 ~> evalwisereturnin.11 [A <= A, B <= B] evalwiseentryin.3 ~> evalwisebb6in.4 [A <= B, B <= A] evalwiseentryin.3 ~> evalwisebb6in.5 [A <= B, B <= A] evalwiseentryin.3 ~> evalwisebb6in.6 [A <= B, B <= A] evalwisebb6in.4 ~> evalwisebb3in.8 [A <= A, B <= B] evalwisebb6in.5 ~> evalwisebb3in.7 [A <= A, B <= B] evalwisebb6in.6 ~> evalwisereturnin.11 [A <= A, B <= B] evalwisebb3in.7 ~> evalwisebb4in.9 [A <= A, B <= B] evalwisebb3in.8 ~> evalwisebb5in.10 [A <= A, B <= B] evalwisebb4in.9 ~> evalwisebb6in.5 [A <= A, B <= A] evalwisebb4in.9 ~> evalwisebb6in.6 [A <= A, B <= A] evalwisebb5in.10 ~> evalwisebb6in.4 [A <= A + B, B <= B] evalwisebb5in.10 ~> evalwisebb6in.6 [A <= A + B, B <= B] evalwisereturnin.11 ~> evalwisestop.12 [A <= A, B <= B] evalwisereturnin.11 ~> evalwisestop.13 [A <= A, B <= B] evalwisereturnin.11 ~> evalwisestop.14 [A <= A, B <= B] evalwisereturnin.11 ~> evalwisestop.15 [A <= A, B <= B] evalwisestop.12 ~> exitus616.16 [A <= A, B <= B] evalwisestop.13 ~> exitus616.16 [A <= A, B <= B] evalwisestop.14 ~> exitus616.16 [A <= A, B <= B] evalwisestop.15 ~> exitus616.16 [A <= A, B <= B] + Loop: [0.0 <= K + A + B] evalwisebb6in.5 ~> evalwisebb3in.7 [A <= A, B <= B] evalwisebb4in.9 ~> evalwisebb6in.5 [A <= A, B <= A] evalwisebb3in.7 ~> evalwisebb4in.9 [A <= A, B <= B] + Loop: [0.1 <= A + B] evalwisebb6in.4 ~> evalwisebb3in.8 [A <= A, B <= B] evalwisebb5in.10 ~> evalwisebb6in.4 [A <= A + B, B <= B] evalwisebb3in.8 ~> evalwisebb5in.10 [A <= A, B <= B] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [tick,huge,K,A,B,0.0,0.1] evalwisestart.0 ~> evalwiseentryin.1 [] evalwisestart.0 ~> evalwiseentryin.2 [] evalwisestart.0 ~> evalwiseentryin.3 [] evalwiseentryin.1 ~> evalwisereturnin.11 [] evalwiseentryin.2 ~> evalwisereturnin.11 [] evalwiseentryin.3 ~> evalwisebb6in.4 [A ~=> B,B ~=> A] evalwiseentryin.3 ~> evalwisebb6in.5 [A ~=> B,B ~=> A] evalwiseentryin.3 ~> evalwisebb6in.6 [A ~=> B,B ~=> A] evalwisebb6in.4 ~> evalwisebb3in.8 [] evalwisebb6in.5 ~> evalwisebb3in.7 [] evalwisebb6in.6 ~> evalwisereturnin.11 [] evalwisebb3in.7 ~> evalwisebb4in.9 [] evalwisebb3in.8 ~> evalwisebb5in.10 [] evalwisebb4in.9 ~> evalwisebb6in.5 [A ~=> B] evalwisebb4in.9 ~> evalwisebb6in.6 [A ~=> B] evalwisebb5in.10 ~> evalwisebb6in.4 [A ~+> A,B ~+> A] evalwisebb5in.10 ~> evalwisebb6in.6 [A ~+> A,B ~+> A] evalwisereturnin.11 ~> evalwisestop.12 [] evalwisereturnin.11 ~> evalwisestop.13 [] evalwisereturnin.11 ~> evalwisestop.14 [] evalwisereturnin.11 ~> evalwisestop.15 [] evalwisestop.12 ~> exitus616.16 [] evalwisestop.13 ~> exitus616.16 [] evalwisestop.14 ~> exitus616.16 [] evalwisestop.15 ~> exitus616.16 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] evalwisebb6in.5 ~> evalwisebb3in.7 [] evalwisebb4in.9 ~> evalwisebb6in.5 [A ~=> B] evalwisebb3in.7 ~> evalwisebb4in.9 [] + Loop: [A ~+> 0.1,B ~+> 0.1] evalwisebb6in.4 ~> evalwisebb3in.8 [] evalwisebb5in.10 ~> evalwisebb6in.4 [A ~+> A,B ~+> A] evalwisebb3in.8 ~> evalwisebb5in.10 [] + Applied Processor: Lare + Details: evalwisestart.0 ~> exitus616.16 [A ~=> B ,B ~=> A ,A ~+> A ,A ~+> 0.0 ,A ~+> 0.1 ,A ~+> tick ,B ~+> A ,B ~+> 0.0 ,B ~+> 0.1 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> tick ,A ~*> A ,B ~*> A] + evalwisebb4in.9> [A ~=> B ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> tick] + evalwisebb5in.10> [A ~+> A ,A ~+> 0.1 ,A ~+> tick ,B ~+> A ,B ~+> 0.1 ,B ~+> tick ,tick ~+> tick ,A ~*> A ,B ~*> A] YES(?,O(n^1))