YES(?,O(n^1)) * Step 1: UnsatPaths WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalrandom1dstart(A,B) -> evalrandom1dentryin(A,B) True (1,1) 1. evalrandom1dentryin(A,B) -> evalrandom1dbb5in(A,1) [A >= 1] (?,1) 2. evalrandom1dentryin(A,B) -> evalrandom1dreturnin(A,B) [0 >= A] (?,1) 3. evalrandom1dbb5in(A,B) -> evalrandom1dbb1in(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= B] (?,1) 4. evalrandom1dbb5in(A,B) -> evalrandom1dreturnin(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + A] (?,1) 5. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + C] (?,1) 6. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1] (?,1) 7. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] (?,1) 8. evalrandom1dreturnin(A,B) -> evalrandom1dstop(A,B) True (?,1) Signature: {(evalrandom1dbb1in,2) ;(evalrandom1dbb5in,2) ;(evalrandom1dentryin,2) ;(evalrandom1dreturnin,2) ;(evalrandom1dstart,2) ;(evalrandom1dstop,2)} Flow Graph: [0->{1,2},1->{3,4},2->{8},3->{5,6,7},4->{8},5->{3,4},6->{3,4},7->{3,4},8->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,4)] * Step 2: FromIts WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalrandom1dstart(A,B) -> evalrandom1dentryin(A,B) True (1,1) 1. evalrandom1dentryin(A,B) -> evalrandom1dbb5in(A,1) [A >= 1] (?,1) 2. evalrandom1dentryin(A,B) -> evalrandom1dreturnin(A,B) [0 >= A] (?,1) 3. evalrandom1dbb5in(A,B) -> evalrandom1dbb1in(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= B] (?,1) 4. evalrandom1dbb5in(A,B) -> evalrandom1dreturnin(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + A] (?,1) 5. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + C] (?,1) 6. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1] (?,1) 7. evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] (?,1) 8. evalrandom1dreturnin(A,B) -> evalrandom1dstop(A,B) True (?,1) Signature: {(evalrandom1dbb1in,2) ;(evalrandom1dbb5in,2) ;(evalrandom1dentryin,2) ;(evalrandom1dreturnin,2) ;(evalrandom1dstart,2) ;(evalrandom1dstop,2)} Flow Graph: [0->{1,2},1->{3},2->{8},3->{5,6,7},4->{8},5->{3,4},6->{3,4},7->{3,4},8->{}] + Applied Processor: FromIts + Details: () * Step 3: AddSinks WORST_CASE(?,O(n^1)) + Considered Problem: Rules: evalrandom1dstart(A,B) -> evalrandom1dentryin(A,B) True evalrandom1dentryin(A,B) -> evalrandom1dbb5in(A,1) [A >= 1] evalrandom1dentryin(A,B) -> evalrandom1dreturnin(A,B) [0 >= A] evalrandom1dbb5in(A,B) -> evalrandom1dbb1in(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= B] evalrandom1dbb5in(A,B) -> evalrandom1dreturnin(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + A] evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + C] evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1] evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] evalrandom1dreturnin(A,B) -> evalrandom1dstop(A,B) True Signature: {(evalrandom1dbb1in,2) ;(evalrandom1dbb5in,2) ;(evalrandom1dentryin,2) ;(evalrandom1dreturnin,2) ;(evalrandom1dstart,2) ;(evalrandom1dstop,2)} Rule Graph: [0->{1,2},1->{3},2->{8},3->{5,6,7},4->{8},5->{3,4},6->{3,4},7->{3,4},8->{}] + Applied Processor: AddSinks + Details: () * Step 4: Unfold WORST_CASE(?,O(n^1)) + Considered Problem: Rules: evalrandom1dstart(A,B) -> evalrandom1dentryin(A,B) True evalrandom1dentryin(A,B) -> evalrandom1dbb5in(A,1) [A >= 1] evalrandom1dentryin(A,B) -> evalrandom1dreturnin(A,B) [0 >= A] evalrandom1dbb5in(A,B) -> evalrandom1dbb1in(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= B] evalrandom1dbb5in(A,B) -> evalrandom1dreturnin(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + A] evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + C] evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1] evalrandom1dbb1in(A,B) -> evalrandom1dbb5in(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] evalrandom1dreturnin(A,B) -> evalrandom1dstop(A,B) True evalrandom1dstop(A,B) -> exitus616(A,B) True evalrandom1dstop(A,B) -> exitus616(A,B) True Signature: {(evalrandom1dbb1in,2) ;(evalrandom1dbb5in,2) ;(evalrandom1dentryin,2) ;(evalrandom1dreturnin,2) ;(evalrandom1dstart,2) ;(evalrandom1dstop,2) ;(exitus616,2)} Rule Graph: [0->{1,2},1->{3},2->{8},3->{5,6,7},4->{8},5->{3,4},6->{3,4},7->{3,4},8->{9,10}] + Applied Processor: Unfold + Details: () * Step 5: Decompose WORST_CASE(?,O(n^1)) + Considered Problem: Rules: evalrandom1dstart.0(A,B) -> evalrandom1dentryin.1(A,B) True evalrandom1dstart.0(A,B) -> evalrandom1dentryin.2(A,B) True evalrandom1dentryin.1(A,B) -> evalrandom1dbb5in.3(A,1) [A >= 1] evalrandom1dentryin.2(A,B) -> evalrandom1dreturnin.8(A,B) [0 >= A] evalrandom1dbb5in.3(A,B) -> evalrandom1dbb1in.5(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= B] evalrandom1dbb5in.3(A,B) -> evalrandom1dbb1in.6(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= B] evalrandom1dbb5in.3(A,B) -> evalrandom1dbb1in.7(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= B] evalrandom1dbb5in.4(A,B) -> evalrandom1dreturnin.8(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + A] evalrandom1dbb1in.5(A,B) -> evalrandom1dbb5in.3(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + C] evalrandom1dbb1in.5(A,B) -> evalrandom1dbb5in.4(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + C] evalrandom1dbb1in.6(A,B) -> evalrandom1dbb5in.3(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1] evalrandom1dbb1in.6(A,B) -> evalrandom1dbb5in.4(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1] evalrandom1dbb1in.7(A,B) -> evalrandom1dbb5in.3(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] evalrandom1dbb1in.7(A,B) -> evalrandom1dbb5in.4(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] evalrandom1dreturnin.8(A,B) -> evalrandom1dstop.9(A,B) True evalrandom1dreturnin.8(A,B) -> evalrandom1dstop.10(A,B) True evalrandom1dstop.9(A,B) -> exitus616.11(A,B) True evalrandom1dstop.10(A,B) -> exitus616.11(A,B) True Signature: {(evalrandom1dbb1in.5,2) ;(evalrandom1dbb1in.6,2) ;(evalrandom1dbb1in.7,2) ;(evalrandom1dbb5in.3,2) ;(evalrandom1dbb5in.4,2) ;(evalrandom1dentryin.1,2) ;(evalrandom1dentryin.2,2) ;(evalrandom1dreturnin.8,2) ;(evalrandom1dstart.0,2) ;(evalrandom1dstop.10,2) ;(evalrandom1dstop.9,2) ;(exitus616.11,2)} Rule Graph: [0->{2},1->{3},2->{4,5,6},3->{14,15},4->{8,9},5->{10,11},6->{12,13},7->{14,15},8->{4,5,6},9->{7},10->{4,5 ,6},11->{7},12->{4,5,6},13->{7},14->{16},15->{17},16->{},17->{}] + 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] | `- p:[4,8,10,5,12,6] c: [4,5,6,8,10,12] * Step 6: AbstractSize WORST_CASE(?,O(n^1)) + Considered Problem: (Rules: evalrandom1dstart.0(A,B) -> evalrandom1dentryin.1(A,B) True evalrandom1dstart.0(A,B) -> evalrandom1dentryin.2(A,B) True evalrandom1dentryin.1(A,B) -> evalrandom1dbb5in.3(A,1) [A >= 1] evalrandom1dentryin.2(A,B) -> evalrandom1dreturnin.8(A,B) [0 >= A] evalrandom1dbb5in.3(A,B) -> evalrandom1dbb1in.5(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= B] evalrandom1dbb5in.3(A,B) -> evalrandom1dbb1in.6(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= B] evalrandom1dbb5in.3(A,B) -> evalrandom1dbb1in.7(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= B] evalrandom1dbb5in.4(A,B) -> evalrandom1dreturnin.8(A,B) [-1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= 1 + A] evalrandom1dbb1in.5(A,B) -> evalrandom1dbb5in.3(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + C] evalrandom1dbb1in.5(A,B) -> evalrandom1dbb5in.4(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + C] evalrandom1dbb1in.6(A,B) -> evalrandom1dbb5in.3(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1] evalrandom1dbb1in.6(A,B) -> evalrandom1dbb5in.4(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1] evalrandom1dbb1in.7(A,B) -> evalrandom1dbb5in.3(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] evalrandom1dbb1in.7(A,B) -> evalrandom1dbb5in.4(A,1 + B) [A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0] evalrandom1dreturnin.8(A,B) -> evalrandom1dstop.9(A,B) True evalrandom1dreturnin.8(A,B) -> evalrandom1dstop.10(A,B) True evalrandom1dstop.9(A,B) -> exitus616.11(A,B) True evalrandom1dstop.10(A,B) -> exitus616.11(A,B) True Signature: {(evalrandom1dbb1in.5,2) ;(evalrandom1dbb1in.6,2) ;(evalrandom1dbb1in.7,2) ;(evalrandom1dbb5in.3,2) ;(evalrandom1dbb5in.4,2) ;(evalrandom1dentryin.1,2) ;(evalrandom1dentryin.2,2) ;(evalrandom1dreturnin.8,2) ;(evalrandom1dstart.0,2) ;(evalrandom1dstop.10,2) ;(evalrandom1dstop.9,2) ;(exitus616.11,2)} Rule Graph: [0->{2},1->{3},2->{4,5,6},3->{14,15},4->{8,9},5->{10,11},6->{12,13},7->{14,15},8->{4,5,6},9->{7},10->{4,5 ,6},11->{7},12->{4,5,6},13->{7},14->{16},15->{17},16->{},17->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17] | `- p:[4,8,10,5,12,6] c: [4,5,6,8,10,12]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [A,B,0.0] evalrandom1dstart.0 ~> evalrandom1dentryin.1 [A <= A, B <= B] evalrandom1dstart.0 ~> evalrandom1dentryin.2 [A <= A, B <= B] evalrandom1dentryin.1 ~> evalrandom1dbb5in.3 [A <= A, B <= K] evalrandom1dentryin.2 ~> evalrandom1dreturnin.8 [A <= A, B <= B] evalrandom1dbb5in.3 ~> evalrandom1dbb1in.5 [A <= A, B <= B] evalrandom1dbb5in.3 ~> evalrandom1dbb1in.6 [A <= A, B <= B] evalrandom1dbb5in.3 ~> evalrandom1dbb1in.7 [A <= A, B <= B] evalrandom1dbb5in.4 ~> evalrandom1dreturnin.8 [A <= A, B <= B] evalrandom1dbb1in.5 ~> evalrandom1dbb5in.3 [A <= A, B <= A + B] evalrandom1dbb1in.5 ~> evalrandom1dbb5in.4 [A <= A, B <= A + B] evalrandom1dbb1in.6 ~> evalrandom1dbb5in.3 [A <= A, B <= A + B] evalrandom1dbb1in.6 ~> evalrandom1dbb5in.4 [A <= A, B <= A + B] evalrandom1dbb1in.7 ~> evalrandom1dbb5in.3 [A <= A, B <= A + B] evalrandom1dbb1in.7 ~> evalrandom1dbb5in.4 [A <= A, B <= A + B] evalrandom1dreturnin.8 ~> evalrandom1dstop.9 [A <= A, B <= B] evalrandom1dreturnin.8 ~> evalrandom1dstop.10 [A <= A, B <= B] evalrandom1dstop.9 ~> exitus616.11 [A <= A, B <= B] evalrandom1dstop.10 ~> exitus616.11 [A <= A, B <= B] + Loop: [0.0 <= A + B] evalrandom1dbb5in.3 ~> evalrandom1dbb1in.5 [A <= A, B <= B] evalrandom1dbb1in.5 ~> evalrandom1dbb5in.3 [A <= A, B <= A + B] evalrandom1dbb1in.6 ~> evalrandom1dbb5in.3 [A <= A, B <= A + B] evalrandom1dbb5in.3 ~> evalrandom1dbb1in.6 [A <= A, B <= B] evalrandom1dbb1in.7 ~> evalrandom1dbb5in.3 [A <= A, B <= A + B] evalrandom1dbb5in.3 ~> evalrandom1dbb1in.7 [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] evalrandom1dstart.0 ~> evalrandom1dentryin.1 [] evalrandom1dstart.0 ~> evalrandom1dentryin.2 [] evalrandom1dentryin.1 ~> evalrandom1dbb5in.3 [K ~=> B] evalrandom1dentryin.2 ~> evalrandom1dreturnin.8 [] evalrandom1dbb5in.3 ~> evalrandom1dbb1in.5 [] evalrandom1dbb5in.3 ~> evalrandom1dbb1in.6 [] evalrandom1dbb5in.3 ~> evalrandom1dbb1in.7 [] evalrandom1dbb5in.4 ~> evalrandom1dreturnin.8 [] evalrandom1dbb1in.5 ~> evalrandom1dbb5in.3 [A ~+> B,B ~+> B] evalrandom1dbb1in.5 ~> evalrandom1dbb5in.4 [A ~+> B,B ~+> B] evalrandom1dbb1in.6 ~> evalrandom1dbb5in.3 [A ~+> B,B ~+> B] evalrandom1dbb1in.6 ~> evalrandom1dbb5in.4 [A ~+> B,B ~+> B] evalrandom1dbb1in.7 ~> evalrandom1dbb5in.3 [A ~+> B,B ~+> B] evalrandom1dbb1in.7 ~> evalrandom1dbb5in.4 [A ~+> B,B ~+> B] evalrandom1dreturnin.8 ~> evalrandom1dstop.9 [] evalrandom1dreturnin.8 ~> evalrandom1dstop.10 [] evalrandom1dstop.9 ~> exitus616.11 [] evalrandom1dstop.10 ~> exitus616.11 [] + Loop: [A ~+> 0.0,B ~+> 0.0] evalrandom1dbb5in.3 ~> evalrandom1dbb1in.5 [] evalrandom1dbb1in.5 ~> evalrandom1dbb5in.3 [A ~+> B,B ~+> B] evalrandom1dbb1in.6 ~> evalrandom1dbb5in.3 [A ~+> B,B ~+> B] evalrandom1dbb5in.3 ~> evalrandom1dbb1in.6 [] evalrandom1dbb1in.7 ~> evalrandom1dbb5in.3 [A ~+> B,B ~+> B] evalrandom1dbb5in.3 ~> evalrandom1dbb1in.7 [] + Applied Processor: Lare + Details: evalrandom1dstart.0 ~> exitus616.11 [A ~+> B ,A ~+> 0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,K ~*> B] + evalrandom1dbb1in.5> [A ~+> B ,A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,A ~*> B ,B ~*> B] evalrandom1dbb1in.7> [A ~+> B ,A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,A ~*> B ,B ~*> B] evalrandom1dbb1in.6> [A ~+> B ,A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,A ~*> B ,B ~*> B] YES(?,O(n^1))