WORST_CASE(?,O(n^1)) * Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. random(A,B,C) -> rand(0,B,C) True (1,1) 1. rand(A,B,C) -> end(A,B,C) [B = 0] (?,1) 2. rand0(A,B,C) -> rand(A,-1 + B,C) True (?,1) 3. rand1(A,B,C) -> idinc(A,C,C) True (?,1) 4. rand(A,B,C) -> c2(rand0(D,B,A),rand1(D,B,A)) [B >= 1] (?,1) 5. rand2(A,B,C) -> rand(A,1 + B,C) True (?,1) 6. rand3(A,B,C) -> iddec(A,C,C) True (?,1) 7. rand(A,B,C) -> c2(rand2(D,B,A),rand3(D,B,A)) [0 >= 1 + B] (?,1) 8. idinc(A,B,C) -> end(A,B,C) True (?,1) 9. idinc(A,B,C) -> end(A,B,C) True (?,1) 10. iddec(A,B,C) -> end(A,B,C) True (?,1) 11. iddec(A,B,C) -> end(A,B,C) True (?,1) Signature: {(end,3);(iddec,3);(idinc,3);(rand,3);(rand0,3);(rand1,3);(rand2,3);(rand3,3);(random,3)} Flow Graph: [0->{1,4,7},1->{},2->{1,4,7},3->{8,9},4->{2,3},5->{1,4,7},6->{10,11},7->{5,6},8->{},9->{},10->{},11->{}] + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (< 0,0,A>, 0, .= 0) (< 0,0,B>, B, .= 0) (< 0,0,C>, C, .= 0) (< 1,0,A>, A, .= 0) (< 1,0,B>, B, .= 0) (< 1,0,C>, C, .= 0) (< 2,0,A>, A, .= 0) (< 2,0,B>, 1 + B, .+ 1) (< 2,0,C>, C, .= 0) (< 3,0,A>, A, .= 0) (< 3,0,B>, C, .= 0) (< 3,0,C>, C, .= 0) (< 4,0,A>, ?, .?) (< 4,0,B>, B, .= 0) (< 4,0,C>, A, .= 0) (< 4,1,A>, ?, .?) (< 4,1,B>, B, .= 0) (< 4,1,C>, A, .= 0) (< 5,0,A>, A, .= 0) (< 5,0,B>, 1 + B, .+ 1) (< 5,0,C>, C, .= 0) (< 6,0,A>, A, .= 0) (< 6,0,B>, C, .= 0) (< 6,0,C>, C, .= 0) (< 7,0,A>, ?, .?) (< 7,0,B>, B, .= 0) (< 7,0,C>, A, .= 0) (< 7,1,A>, ?, .?) (< 7,1,B>, B, .= 0) (< 7,1,C>, A, .= 0) (< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0) (< 8,0,C>, C, .= 0) (< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0) (< 9,0,C>, C, .= 0) (<10,0,A>, A, .= 0) (<10,0,B>, B, .= 0) (<10,0,C>, C, .= 0) (<11,0,A>, A, .= 0) (<11,0,B>, B, .= 0) (<11,0,C>, C, .= 0) * Step 2: SizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. random(A,B,C) -> rand(0,B,C) True (1,1) 1. rand(A,B,C) -> end(A,B,C) [B = 0] (?,1) 2. rand0(A,B,C) -> rand(A,-1 + B,C) True (?,1) 3. rand1(A,B,C) -> idinc(A,C,C) True (?,1) 4. rand(A,B,C) -> c2(rand0(D,B,A),rand1(D,B,A)) [B >= 1] (?,1) 5. rand2(A,B,C) -> rand(A,1 + B,C) True (?,1) 6. rand3(A,B,C) -> iddec(A,C,C) True (?,1) 7. rand(A,B,C) -> c2(rand2(D,B,A),rand3(D,B,A)) [0 >= 1 + B] (?,1) 8. idinc(A,B,C) -> end(A,B,C) True (?,1) 9. idinc(A,B,C) -> end(A,B,C) True (?,1) 10. iddec(A,B,C) -> end(A,B,C) True (?,1) 11. iddec(A,B,C) -> end(A,B,C) True (?,1) Signature: {(end,3);(iddec,3);(idinc,3);(rand,3);(rand0,3);(rand1,3);(rand2,3);(rand3,3);(random,3)} Flow Graph: [0->{1,4,7},1->{},2->{1,4,7},3->{8,9},4->{2,3},5->{1,4,7},6->{10,11},7->{5,6},8->{},9->{},10->{},11->{}] Sizebounds: (< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,1,A>, ?) (< 4,1,B>, ?) (< 4,1,C>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,1,A>, ?) (< 7,1,B>, ?) (< 7,1,C>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (< 0,0,A>, 0) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,1,A>, ?) (< 4,1,B>, ?) (< 4,1,C>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,1,A>, ?) (< 7,1,B>, ?) (< 7,1,C>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) * Step 3: LeafRules WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. random(A,B,C) -> rand(0,B,C) True (1,1) 1. rand(A,B,C) -> end(A,B,C) [B = 0] (?,1) 2. rand0(A,B,C) -> rand(A,-1 + B,C) True (?,1) 3. rand1(A,B,C) -> idinc(A,C,C) True (?,1) 4. rand(A,B,C) -> c2(rand0(D,B,A),rand1(D,B,A)) [B >= 1] (?,1) 5. rand2(A,B,C) -> rand(A,1 + B,C) True (?,1) 6. rand3(A,B,C) -> iddec(A,C,C) True (?,1) 7. rand(A,B,C) -> c2(rand2(D,B,A),rand3(D,B,A)) [0 >= 1 + B] (?,1) 8. idinc(A,B,C) -> end(A,B,C) True (?,1) 9. idinc(A,B,C) -> end(A,B,C) True (?,1) 10. iddec(A,B,C) -> end(A,B,C) True (?,1) 11. iddec(A,B,C) -> end(A,B,C) True (?,1) Signature: {(end,3);(iddec,3);(idinc,3);(rand,3);(rand0,3);(rand1,3);(rand2,3);(rand3,3);(random,3)} Flow Graph: [0->{1,4,7},1->{},2->{1,4,7},3->{8,9},4->{2,3},5->{1,4,7},6->{10,11},7->{5,6},8->{},9->{},10->{},11->{}] Sizebounds: (< 0,0,A>, 0) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,1,A>, ?) (< 4,1,B>, ?) (< 4,1,C>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,1,A>, ?) (< 7,1,B>, ?) (< 7,1,C>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) + Applied Processor: LeafRules + Details: The following transitions are estimated by its predecessors and are removed [3,6,1,8,9,10,11] * Step 4: ChainProcessor WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. random(A,B,C) -> rand(0,B,C) True (1,1) 2. rand0(A,B,C) -> rand(A,-1 + B,C) True (?,1) 4. rand(A,B,C) -> c2(rand0(D,B,A),rand1(D,B,A)) [B >= 1] (?,1) 5. rand2(A,B,C) -> rand(A,1 + B,C) True (?,1) 7. rand(A,B,C) -> c2(rand2(D,B,A),rand3(D,B,A)) [0 >= 1 + B] (?,1) Signature: {(end,3);(iddec,3);(idinc,3);(rand,3);(rand0,3);(rand1,3);(rand2,3);(rand3,3);(random,3)} Flow Graph: [0->{4,7},2->{4,7},4->{2},5->{4,7},7->{5}] Sizebounds: (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<2,0,A>, ?) (<2,0,B>, ?) (<2,0,C>, ?) (<4,0,A>, ?) (<4,0,B>, ?) (<4,0,C>, ?) (<4,1,A>, ?) (<4,1,B>, ?) (<4,1,C>, ?) (<5,0,A>, ?) (<5,0,B>, ?) (<5,0,C>, ?) (<7,0,A>, ?) (<7,0,B>, ?) (<7,0,C>, ?) (<7,1,A>, ?) (<7,1,B>, ?) (<7,1,C>, ?) + Applied Processor: ChainProcessor False [0,2,4,5,7] + Details: We chained rule 4 to obtain the rules [8] . * Step 5: UnreachableRules WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. random(A,B,C) -> rand(0,B,C) True (1,1) 2. rand0(A,B,C) -> rand(A,-1 + B,C) True (?,1) 5. rand2(A,B,C) -> rand(A,1 + B,C) True (?,1) 7. rand(A,B,C) -> c2(rand2(D,B,A),rand3(D,B,A)) [0 >= 1 + B] (?,1) 8. rand(A,B,C) -> c2(rand(D,-1 + B,A),rand1(D,B,A)) [B >= 1] (?,2) Signature: {(end,3);(iddec,3);(idinc,3);(rand,3);(rand0,3);(rand1,3);(rand2,3);(rand3,3);(random,3)} Flow Graph: [0->{7,8},2->{7,8},5->{7,8},7->{5},8->{7,8}] Sizebounds: (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<2,0,A>, ?) (<2,0,B>, ?) (<2,0,C>, ?) (<5,0,A>, ?) (<5,0,B>, ?) (<5,0,C>, ?) (<7,0,A>, ?) (<7,0,B>, ?) (<7,0,C>, ?) (<7,1,A>, ?) (<7,1,B>, ?) (<7,1,C>, ?) (<8,0,A>, ?) (<8,0,B>, ?) (<8,0,C>, ?) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [2] * Step 6: ChainProcessor WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. random(A,B,C) -> rand(0,B,C) True (1,1) 5. rand2(A,B,C) -> rand(A,1 + B,C) True (?,1) 7. rand(A,B,C) -> c2(rand2(D,B,A),rand3(D,B,A)) [0 >= 1 + B] (?,1) 8. rand(A,B,C) -> c2(rand(D,-1 + B,A),rand1(D,B,A)) [B >= 1] (?,2) Signature: {(end,3);(iddec,3);(idinc,3);(rand,3);(rand0,3);(rand1,3);(rand2,3);(rand3,3);(random,3)} Flow Graph: [0->{7,8},5->{7,8},7->{5},8->{7,8}] Sizebounds: (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<5,0,A>, ?) (<5,0,B>, ?) (<5,0,C>, ?) (<7,0,A>, ?) (<7,0,B>, ?) (<7,0,C>, ?) (<7,1,A>, ?) (<7,1,B>, ?) (<7,1,C>, ?) (<8,0,A>, ?) (<8,0,B>, ?) (<8,0,C>, ?) + Applied Processor: ChainProcessor False [0,5,7,8] + Details: We chained rule 7 to obtain the rules [9] . * Step 7: UnreachableRules WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. random(A,B,C) -> rand(0,B,C) True (1,1) 5. rand2(A,B,C) -> rand(A,1 + B,C) True (?,1) 8. rand(A,B,C) -> c2(rand(D,-1 + B,A),rand1(D,B,A)) [B >= 1] (?,2) 9. rand(A,B,C) -> c2(rand(D,1 + B,A),rand3(D,B,A)) [0 >= 1 + B] (?,2) Signature: {(end,3);(iddec,3);(idinc,3);(rand,3);(rand0,3);(rand1,3);(rand2,3);(rand3,3);(random,3)} Flow Graph: [0->{8,9},5->{8,9},8->{8,9},9->{8,9}] Sizebounds: (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<5,0,A>, ?) (<5,0,B>, ?) (<5,0,C>, ?) (<8,0,A>, ?) (<8,0,B>, ?) (<8,0,C>, ?) (<9,0,A>, ?) (<9,0,B>, ?) (<9,0,C>, ?) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [5] * Step 8: UnsatPaths WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. random(A,B,C) -> rand(0,B,C) True (1,1) 8. rand(A,B,C) -> c2(rand(D,-1 + B,A),rand1(D,B,A)) [B >= 1] (?,2) 9. rand(A,B,C) -> c2(rand(D,1 + B,A),rand3(D,B,A)) [0 >= 1 + B] (?,2) Signature: {(end,3);(iddec,3);(idinc,3);(rand,3);(rand0,3);(rand1,3);(rand2,3);(rand3,3);(random,3)} Flow Graph: [0->{8,9},8->{8,9},9->{8,9}] Sizebounds: (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<8,0,A>, ?) (<8,0,B>, ?) (<8,0,C>, ?) (<9,0,A>, ?) (<9,0,B>, ?) (<9,0,C>, ?) + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(8,9),(9,8)] * Step 9: LocalSizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. random(A,B,C) -> rand(0,B,C) True (1,1) 8. rand(A,B,C) -> c2(rand(D,-1 + B,A),rand1(D,B,A)) [B >= 1] (?,2) 9. rand(A,B,C) -> c2(rand(D,1 + B,A),rand3(D,B,A)) [0 >= 1 + B] (?,2) Signature: {(end,3);(iddec,3);(idinc,3);(rand,3);(rand0,3);(rand1,3);(rand2,3);(rand3,3);(random,3)} Flow Graph: [0->{8,9},8->{8},9->{9}] Sizebounds: (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<8,0,A>, ?) (<8,0,B>, ?) (<8,0,C>, ?) (<9,0,A>, ?) (<9,0,B>, ?) (<9,0,C>, ?) + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (<0,0,A>, 0, .= 0) (<0,0,B>, B, .= 0) (<0,0,C>, C, .= 0) (<8,0,A>, ?, .?) (<8,0,B>, 1 + B, .+ 1) (<8,0,C>, A, .= 0) (<8,1,A>, ?, .?) (<8,1,B>, B, .= 0) (<8,1,C>, A, .= 0) (<9,0,A>, ?, .?) (<9,0,B>, 1 + B, .+ 1) (<9,0,C>, A, .= 0) (<9,1,A>, ?, .?) (<9,1,B>, B, .= 0) (<9,1,C>, A, .= 0) * Step 10: SizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. random(A,B,C) -> rand(0,B,C) True (1,1) 8. rand(A,B,C) -> c2(rand(D,-1 + B,A),rand1(D,B,A)) [B >= 1] (?,2) 9. rand(A,B,C) -> c2(rand(D,1 + B,A),rand3(D,B,A)) [0 >= 1 + B] (?,2) Signature: {(end,3);(iddec,3);(idinc,3);(rand,3);(rand0,3);(rand1,3);(rand2,3);(rand3,3);(random,3)} Flow Graph: [0->{8,9},8->{8},9->{9}] Sizebounds: (<0,0,A>, ?) (<0,0,B>, ?) (<0,0,C>, ?) (<8,0,A>, ?) (<8,0,B>, ?) (<8,0,C>, ?) (<8,1,A>, ?) (<8,1,B>, ?) (<8,1,C>, ?) (<9,0,A>, ?) (<9,0,B>, ?) (<9,0,C>, ?) (<9,1,A>, ?) (<9,1,B>, ?) (<9,1,C>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<8,0,A>, ?) (<8,0,B>, ?) (<8,0,C>, ?) (<8,1,A>, ?) (<8,1,B>, ?) (<8,1,C>, ?) (<9,0,A>, ?) (<9,0,B>, ?) (<9,0,C>, ?) (<9,1,A>, ?) (<9,1,B>, ?) (<9,1,C>, ?) * Step 11: LocationConstraintsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. random(A,B,C) -> rand(0,B,C) True (1,1) 8. rand(A,B,C) -> c2(rand(D,-1 + B,A),rand1(D,B,A)) [B >= 1] (?,2) 9. rand(A,B,C) -> c2(rand(D,1 + B,A),rand3(D,B,A)) [0 >= 1 + B] (?,2) Signature: {(end,3);(iddec,3);(idinc,3);(rand,3);(rand0,3);(rand1,3);(rand2,3);(rand3,3);(random,3)} Flow Graph: [0->{8,9},8->{8},9->{9}] Sizebounds: (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<8,0,A>, ?) (<8,0,B>, ?) (<8,0,C>, ?) (<8,1,A>, ?) (<8,1,B>, ?) (<8,1,C>, ?) (<9,0,A>, ?) (<9,0,B>, ?) (<9,0,C>, ?) (<9,1,A>, ?) (<9,1,B>, ?) (<9,1,C>, ?) + Applied Processor: LocationConstraintsProc + Details: We computed the location constraints 0 : True 8 : True 9 : True . * Step 12: LoopRecurrenceProcessor WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. random(A,B,C) -> rand(0,B,C) True (1,1) 8. rand(A,B,C) -> c2(rand(D,-1 + B,A),rand1(D,B,A)) [B >= 1] (?,2) 9. rand(A,B,C) -> c2(rand(D,1 + B,A),rand3(D,B,A)) [0 >= 1 + B] (?,2) Signature: {(end,3);(iddec,3);(idinc,3);(rand,3);(rand0,3);(rand1,3);(rand2,3);(rand3,3);(random,3)} Flow Graph: [0->{8,9},8->{8},9->{9}] Sizebounds: (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<8,0,A>, ?) (<8,0,B>, ?) (<8,0,C>, ?) (<8,1,A>, ?) (<8,1,B>, ?) (<8,1,C>, ?) (<9,0,A>, ?) (<9,0,B>, ?) (<9,0,C>, ?) (<9,1,A>, ?) (<9,1,B>, ?) (<9,1,C>, ?) + Applied Processor: LoopRecurrenceProcessor [8] + Details: Applying the recurrence pattern linear * f to the expression B yields the solution B . * Step 13: SizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. random(A,B,C) -> rand(0,B,C) True (1,1) 8. rand(A,B,C) -> c2(rand(D,-1 + B,A),rand1(D,B,A)) [B >= 1] (B,2) 9. rand(A,B,C) -> c2(rand(D,1 + B,A),rand3(D,B,A)) [0 >= 1 + B] (?,2) Signature: {(end,3);(iddec,3);(idinc,3);(rand,3);(rand0,3);(rand1,3);(rand2,3);(rand3,3);(random,3)} Flow Graph: [0->{8,9},8->{8},9->{9}] Sizebounds: (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<8,0,A>, ?) (<8,0,B>, ?) (<8,0,C>, ?) (<8,1,A>, ?) (<8,1,B>, ?) (<8,1,C>, ?) (<9,0,A>, ?) (<9,0,B>, ?) (<9,0,C>, ?) (<9,1,A>, ?) (<9,1,B>, ?) (<9,1,C>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<8,0,A>, ?) (<8,0,B>, 2*B) (<8,0,C>, ?) (<8,1,A>, ?) (<8,1,B>, 2*B) (<8,1,C>, ?) (<9,0,A>, ?) (<9,0,B>, ?) (<9,0,C>, ?) (<9,1,A>, ?) (<9,1,B>, ?) (<9,1,C>, ?) * Step 14: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. random(A,B,C) -> rand(0,B,C) True (1,1) 8. rand(A,B,C) -> c2(rand(D,-1 + B,A),rand1(D,B,A)) [B >= 1] (B,2) 9. rand(A,B,C) -> c2(rand(D,1 + B,A),rand3(D,B,A)) [0 >= 1 + B] (?,2) Signature: {(end,3);(iddec,3);(idinc,3);(rand,3);(rand0,3);(rand1,3);(rand2,3);(rand3,3);(random,3)} Flow Graph: [0->{8,9},8->{8},9->{9}] Sizebounds: (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<8,0,A>, ?) (<8,0,B>, 2*B) (<8,0,C>, ?) (<8,1,A>, ?) (<8,1,B>, 2*B) (<8,1,C>, ?) (<9,0,A>, ?) (<9,0,B>, ?) (<9,0,C>, ?) (<9,1,A>, ?) (<9,1,B>, ?) (<9,1,C>, ?) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [9], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(rand) = -1*x2 p(rand3) = 0 The following rules are strictly oriented: [0 >= 1 + B] ==> rand(A,B,C) = -1*B > -1 + -1*B = c2(rand(D,1 + B,A),rand3(D,B,A)) The following rules are weakly oriented: We use the following global sizebounds: (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<8,0,A>, ?) (<8,0,B>, 2*B) (<8,0,C>, ?) (<8,1,A>, ?) (<8,1,B>, 2*B) (<8,1,C>, ?) (<9,0,A>, ?) (<9,0,B>, ?) (<9,0,C>, ?) (<9,1,A>, ?) (<9,1,B>, ?) (<9,1,C>, ?) * Step 15: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. random(A,B,C) -> rand(0,B,C) True (1,1) 8. rand(A,B,C) -> c2(rand(D,-1 + B,A),rand1(D,B,A)) [B >= 1] (B,2) 9. rand(A,B,C) -> c2(rand(D,1 + B,A),rand3(D,B,A)) [0 >= 1 + B] (B,2) Signature: {(end,3);(iddec,3);(idinc,3);(rand,3);(rand0,3);(rand1,3);(rand2,3);(rand3,3);(random,3)} Flow Graph: [0->{8,9},8->{8},9->{9}] Sizebounds: (<0,0,A>, 0) (<0,0,B>, B) (<0,0,C>, C) (<8,0,A>, ?) (<8,0,B>, 2*B) (<8,0,C>, ?) (<8,1,A>, ?) (<8,1,B>, 2*B) (<8,1,C>, ?) (<9,0,A>, ?) (<9,0,B>, ?) (<9,0,C>, ?) (<9,1,A>, ?) (<9,1,B>, ?) (<9,1,C>, ?) + Applied Processor: KnowledgePropagation + Details: The problem is already solved. WORST_CASE(?,O(n^1))