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: Decompose 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: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10] | `- p:[3,5,6,7] c: [3,5,6,7] * Step 5: AbstractSize 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}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10] | `- p:[3,5,6,7] c: [3,5,6,7]) + Applied Processor: AbstractSize Minimize + Details: () * Step 6: AbstractFlow WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [A,B,0.0] evalrandom1dstart ~> evalrandom1dentryin [A <= A, B <= B] evalrandom1dentryin ~> evalrandom1dbb5in [A <= A, B <= K] evalrandom1dentryin ~> evalrandom1dreturnin [A <= A, B <= B] evalrandom1dbb5in ~> evalrandom1dbb1in [A <= A, B <= B] evalrandom1dbb5in ~> evalrandom1dreturnin [A <= A, B <= B] evalrandom1dbb1in ~> evalrandom1dbb5in [A <= A, B <= A + B] evalrandom1dbb1in ~> evalrandom1dbb5in [A <= A, B <= A + B] evalrandom1dbb1in ~> evalrandom1dbb5in [A <= A, B <= A + B] evalrandom1dreturnin ~> evalrandom1dstop [A <= A, B <= B] evalrandom1dstop ~> exitus616 [A <= A, B <= B] evalrandom1dstop ~> exitus616 [A <= A, B <= B] + Loop: [0.0 <= A + B] evalrandom1dbb5in ~> evalrandom1dbb1in [A <= A, B <= B] evalrandom1dbb1in ~> evalrandom1dbb5in [A <= A, B <= A + B] evalrandom1dbb1in ~> evalrandom1dbb5in [A <= A, B <= A + B] evalrandom1dbb1in ~> evalrandom1dbb5in [A <= A, B <= A + B] + Applied Processor: AbstractFlow + Details: () * Step 7: Lare WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [tick,huge,K,A,B,0.0] evalrandom1dstart ~> evalrandom1dentryin [] evalrandom1dentryin ~> evalrandom1dbb5in [K ~=> B] evalrandom1dentryin ~> evalrandom1dreturnin [] evalrandom1dbb5in ~> evalrandom1dbb1in [] evalrandom1dbb5in ~> evalrandom1dreturnin [] evalrandom1dbb1in ~> evalrandom1dbb5in [A ~+> B,B ~+> B] evalrandom1dbb1in ~> evalrandom1dbb5in [A ~+> B,B ~+> B] evalrandom1dbb1in ~> evalrandom1dbb5in [A ~+> B,B ~+> B] evalrandom1dreturnin ~> evalrandom1dstop [] evalrandom1dstop ~> exitus616 [] evalrandom1dstop ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0] evalrandom1dbb5in ~> evalrandom1dbb1in [] evalrandom1dbb1in ~> evalrandom1dbb5in [A ~+> B,B ~+> B] evalrandom1dbb1in ~> evalrandom1dbb5in [A ~+> B,B ~+> B] evalrandom1dbb1in ~> evalrandom1dbb5in [A ~+> B,B ~+> B] + Applied Processor: Lare + Details: evalrandom1dstart ~> exitus616 [K ~=> B ,A ~+> B ,A ~+> 0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> 0.0 ,K ~+> tick ,A ~*> B ,K ~*> B] + evalrandom1dbb5in> [A ~+> B ,A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,A ~*> B ,B ~*> B] YES(?,O(n^1))