WORST_CASE(?,O(log(n)*n^1)) * Step 1: UnreachableRules WORST_CASE(?,O(log(n)*n^1)) + Considered Problem: Rules: 0. mergeSort0(A,B,C) -> msplit(A,B,C) True (?,1) 1. mergeSort1(A,B,C) -> mergeSort(B,B,C) True (?,1) 2. mergeSort2(A,B,C) -> mergeSort(C,B,C) True (?,1) 3. mergeSort3(A,B,C) -> merge(B,C,C) True (?,1) 4. mergeSort(A,B,C) -> c4(mergeSort0(A,D,E),mergeSort1(A,D,E),mergeSort2(A,D,E),mergeSort3(A,D,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,1) 5. out2msplit(A,B,C) -> out2msplit(-2 + A,B,C) [A >= 2] (?,1) 6. out1msplit(A,B,C) -> out1msplit(-2 + A,B,C) [A >= 2] (?,1) 7. msplit(A,B,C) -> msplit(-2 + A,B,C) [A >= 2] (?,1) 8. merge(A,B,C) -> merge(-1 + A,B,C) [A >= 1 && B >= 1] (?,1) 9. merge(A,B,C) -> merge(A,-1 + B,C) [A >= 1 && B >= 1] (?,1) 10. start(A,B,C) -> mergeSort(A,B,C) True (1,1) Signature: {(merge,3) ;(mergeSort,3) ;(mergeSort0,3) ;(mergeSort1,3) ;(mergeSort2,3) ;(mergeSort3,3) ;(msplit,3) ;(out1msplit,3) ;(out2msplit,3) ;(start,3)} Flow Graph: [0->{7},1->{4},2->{4},3->{8,9},4->{0,1,2,3},5->{5},6->{6},7->{7},8->{8,9},9->{8,9},10->{4}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are removed: [5,6] * Step 2: LocalSizeboundsProc WORST_CASE(?,O(log(n)*n^1)) + Considered Problem: Rules: 0. mergeSort0(A,B,C) -> msplit(A,B,C) True (?,1) 1. mergeSort1(A,B,C) -> mergeSort(B,B,C) True (?,1) 2. mergeSort2(A,B,C) -> mergeSort(C,B,C) True (?,1) 3. mergeSort3(A,B,C) -> merge(B,C,C) True (?,1) 4. mergeSort(A,B,C) -> c4(mergeSort0(A,D,E),mergeSort1(A,D,E),mergeSort2(A,D,E),mergeSort3(A,D,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,1) 7. msplit(A,B,C) -> msplit(-2 + A,B,C) [A >= 2] (?,1) 8. merge(A,B,C) -> merge(-1 + A,B,C) [A >= 1 && B >= 1] (?,1) 9. merge(A,B,C) -> merge(A,-1 + B,C) [A >= 1 && B >= 1] (?,1) 10. start(A,B,C) -> mergeSort(A,B,C) True (1,1) Signature: {(merge,3) ;(mergeSort,3) ;(mergeSort0,3) ;(mergeSort1,3) ;(mergeSort2,3) ;(mergeSort3,3) ;(msplit,3) ;(out1msplit,3) ;(out2msplit,3) ;(start,3)} Flow Graph: [0->{7},1->{4},2->{4},3->{8,9},4->{0,1,2,3},7->{7},8->{8,9},9->{8,9},10->{4}] + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (< 0,0,A>, A, .= 0) (< 0,0,B>, B, .= 0) (< 0,0,C>, C, .= 0) (< 1,0,A>, B, .= 0) (< 1,0,B>, B, .= 0) (< 1,0,C>, C, .= 0) (< 2,0,A>, C, .= 0) (< 2,0,B>, B, .= 0) (< 2,0,C>, C, .= 0) (< 3,0,A>, B, .= 0) (< 3,0,B>, C, .= 0) (< 3,0,C>, C, .= 0) (< 4,0,A>, A, .= 0) (< 4,0,B>, 1 + A, .+ 1) (< 4,0,C>, A, .= 0) (< 4,1,A>, A, .= 0) (< 4,1,B>, 1 + A, .+ 1) (< 4,1,C>, A, .= 0) (< 4,2,A>, A, .= 0) (< 4,2,B>, 1 + A, .+ 1) (< 4,2,C>, A, .= 0) (< 4,3,A>, A, .= 0) (< 4,3,B>, 1 + A, .+ 1) (< 4,3,C>, A, .= 0) (< 7,0,A>, 2 + A, .+ 2) (< 7,0,B>, B, .= 0) (< 7,0,C>, C, .= 0) (< 8,0,A>, 1 + A, .+ 1) (< 8,0,B>, B, .= 0) (< 8,0,C>, C, .= 0) (< 9,0,A>, A, .= 0) (< 9,0,B>, 1 + B, .+ 1) (< 9,0,C>, C, .= 0) (<10,0,A>, A, .= 0) (<10,0,B>, B, .= 0) (<10,0,C>, C, .= 0) * Step 3: SizeboundsProc WORST_CASE(?,O(log(n)*n^1)) + Considered Problem: Rules: 0. mergeSort0(A,B,C) -> msplit(A,B,C) True (?,1) 1. mergeSort1(A,B,C) -> mergeSort(B,B,C) True (?,1) 2. mergeSort2(A,B,C) -> mergeSort(C,B,C) True (?,1) 3. mergeSort3(A,B,C) -> merge(B,C,C) True (?,1) 4. mergeSort(A,B,C) -> c4(mergeSort0(A,D,E),mergeSort1(A,D,E),mergeSort2(A,D,E),mergeSort3(A,D,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,1) 7. msplit(A,B,C) -> msplit(-2 + A,B,C) [A >= 2] (?,1) 8. merge(A,B,C) -> merge(-1 + A,B,C) [A >= 1 && B >= 1] (?,1) 9. merge(A,B,C) -> merge(A,-1 + B,C) [A >= 1 && B >= 1] (?,1) 10. start(A,B,C) -> mergeSort(A,B,C) True (1,1) Signature: {(merge,3) ;(mergeSort,3) ;(mergeSort0,3) ;(mergeSort1,3) ;(mergeSort2,3) ;(mergeSort3,3) ;(msplit,3) ;(out1msplit,3) ;(out2msplit,3) ;(start,3)} Flow Graph: [0->{7},1->{4},2->{4},3->{8,9},4->{0,1,2,3},7->{7},8->{8,9},9->{8,9},10->{4}] 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>, ?) (< 4,2,A>, ?) (< 4,2,B>, ?) (< 4,2,C>, ?) (< 4,3,A>, ?) (< 4,3,B>, ?) (< 4,3,C>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,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>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, ?) (< 1,0,B>, B) (< 1,0,C>, C) (< 2,0,A>, ?) (< 2,0,B>, B) (< 2,0,C>, C) (< 3,0,A>, B) (< 3,0,B>, C) (< 3,0,C>, C) (< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,1,A>, A) (< 4,1,B>, ?) (< 4,1,C>, ?) (< 4,2,A>, A) (< 4,2,B>, ?) (< 4,2,C>, ?) (< 4,3,A>, A) (< 4,3,B>, ?) (< 4,3,C>, ?) (< 7,0,A>, ?) (< 7,0,B>, B) (< 7,0,C>, C) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, C) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) * Step 4: ChainProcessor WORST_CASE(?,O(log(n)*n^1)) + Considered Problem: Rules: 0. mergeSort0(A,B,C) -> msplit(A,B,C) True (?,1) 1. mergeSort1(A,B,C) -> mergeSort(B,B,C) True (?,1) 2. mergeSort2(A,B,C) -> mergeSort(C,B,C) True (?,1) 3. mergeSort3(A,B,C) -> merge(B,C,C) True (?,1) 4. mergeSort(A,B,C) -> c4(mergeSort0(A,D,E),mergeSort1(A,D,E),mergeSort2(A,D,E),mergeSort3(A,D,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,1) 7. msplit(A,B,C) -> msplit(-2 + A,B,C) [A >= 2] (?,1) 8. merge(A,B,C) -> merge(-1 + A,B,C) [A >= 1 && B >= 1] (?,1) 9. merge(A,B,C) -> merge(A,-1 + B,C) [A >= 1 && B >= 1] (?,1) 10. start(A,B,C) -> mergeSort(A,B,C) True (1,1) Signature: {(merge,3) ;(mergeSort,3) ;(mergeSort0,3) ;(mergeSort1,3) ;(mergeSort2,3) ;(mergeSort3,3) ;(msplit,3) ;(out1msplit,3) ;(out2msplit,3) ;(start,3)} Flow Graph: [0->{7},1->{4},2->{4},3->{8,9},4->{0,1,2,3},7->{7},8->{8,9},9->{8,9},10->{4}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, ?) (< 1,0,B>, B) (< 1,0,C>, C) (< 2,0,A>, ?) (< 2,0,B>, B) (< 2,0,C>, C) (< 3,0,A>, B) (< 3,0,B>, C) (< 3,0,C>, C) (< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,1,A>, A) (< 4,1,B>, ?) (< 4,1,C>, ?) (< 4,2,A>, A) (< 4,2,B>, ?) (< 4,2,C>, ?) (< 4,3,A>, A) (< 4,3,B>, ?) (< 4,3,C>, ?) (< 7,0,A>, ?) (< 7,0,B>, B) (< 7,0,C>, C) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, C) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) + Applied Processor: ChainProcessor False [0,1,2,3,4,7,8,9,10] + Details: We chained rule 4 to obtain the rules [11] . * Step 5: UnreachableRules WORST_CASE(?,O(log(n)*n^1)) + Considered Problem: Rules: 0. mergeSort0(A,B,C) -> msplit(A,B,C) True (?,1) 1. mergeSort1(A,B,C) -> mergeSort(B,B,C) True (?,1) 2. mergeSort2(A,B,C) -> mergeSort(C,B,C) True (?,1) 3. mergeSort3(A,B,C) -> merge(B,C,C) True (?,1) 7. msplit(A,B,C) -> msplit(-2 + A,B,C) [A >= 2] (?,1) 8. merge(A,B,C) -> merge(-1 + A,B,C) [A >= 1 && B >= 1] (?,1) 9. merge(A,B,C) -> merge(A,-1 + B,C) [A >= 1 && B >= 1] (?,1) 10. start(A,B,C) -> mergeSort(A,B,C) True (1,1) 11. mergeSort(A,B,C) -> c4(msplit(A,D,E),mergeSort1(A,D,E),mergeSort2(A,D,E),mergeSort3(A,D,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,2) Signature: {(merge,3) ;(mergeSort,3) ;(mergeSort0,3) ;(mergeSort1,3) ;(mergeSort2,3) ;(mergeSort3,3) ;(msplit,3) ;(out1msplit,3) ;(out2msplit,3) ;(start,3)} Flow Graph: [0->{7},1->{11},2->{11},3->{8,9},7->{7},8->{8,9},9->{8,9},10->{11},11->{1,2,3,7}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 1,0,A>, ?) (< 1,0,B>, B) (< 1,0,C>, C) (< 2,0,A>, ?) (< 2,0,B>, B) (< 2,0,C>, C) (< 3,0,A>, B) (< 3,0,B>, C) (< 3,0,C>, C) (< 7,0,A>, ?) (< 7,0,B>, B) (< 7,0,C>, C) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, C) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C) + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are removed: [0] * Step 6: ChainProcessor WORST_CASE(?,O(log(n)*n^1)) + Considered Problem: Rules: 1. mergeSort1(A,B,C) -> mergeSort(B,B,C) True (?,1) 2. mergeSort2(A,B,C) -> mergeSort(C,B,C) True (?,1) 3. mergeSort3(A,B,C) -> merge(B,C,C) True (?,1) 7. msplit(A,B,C) -> msplit(-2 + A,B,C) [A >= 2] (?,1) 8. merge(A,B,C) -> merge(-1 + A,B,C) [A >= 1 && B >= 1] (?,1) 9. merge(A,B,C) -> merge(A,-1 + B,C) [A >= 1 && B >= 1] (?,1) 10. start(A,B,C) -> mergeSort(A,B,C) True (1,1) 11. mergeSort(A,B,C) -> c4(msplit(A,D,E),mergeSort1(A,D,E),mergeSort2(A,D,E),mergeSort3(A,D,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,2) Signature: {(merge,3) ;(mergeSort,3) ;(mergeSort0,3) ;(mergeSort1,3) ;(mergeSort2,3) ;(mergeSort3,3) ;(msplit,3) ;(out1msplit,3) ;(out2msplit,3) ;(start,3)} Flow Graph: [1->{11},2->{11},3->{8,9},7->{7},8->{8,9},9->{8,9},10->{11},11->{1,2,3,7}] Sizebounds: (< 1,0,A>, ?) (< 1,0,B>, B) (< 1,0,C>, C) (< 2,0,A>, ?) (< 2,0,B>, B) (< 2,0,C>, C) (< 3,0,A>, B) (< 3,0,B>, C) (< 3,0,C>, C) (< 7,0,A>, ?) (< 7,0,B>, B) (< 7,0,C>, C) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, C) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C) + Applied Processor: ChainProcessor False [1,2,3,7,8,9,10,11] + Details: We chained rule 11 to obtain the rules [12] . * Step 7: UnreachableRules WORST_CASE(?,O(log(n)*n^1)) + Considered Problem: Rules: 1. mergeSort1(A,B,C) -> mergeSort(B,B,C) True (?,1) 2. mergeSort2(A,B,C) -> mergeSort(C,B,C) True (?,1) 3. mergeSort3(A,B,C) -> merge(B,C,C) True (?,1) 7. msplit(A,B,C) -> msplit(-2 + A,B,C) [A >= 2] (?,1) 8. merge(A,B,C) -> merge(-1 + A,B,C) [A >= 1 && B >= 1] (?,1) 9. merge(A,B,C) -> merge(A,-1 + B,C) [A >= 1 && B >= 1] (?,1) 10. start(A,B,C) -> mergeSort(A,B,C) True (1,1) 12. mergeSort(A,B,C) -> c4(msplit(A,D,E),mergeSort(D,D,E),mergeSort2(A,D,E),mergeSort3(A,D,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,3) Signature: {(merge,3) ;(mergeSort,3) ;(mergeSort0,3) ;(mergeSort1,3) ;(mergeSort2,3) ;(mergeSort3,3) ;(msplit,3) ;(out1msplit,3) ;(out2msplit,3) ;(start,3)} Flow Graph: [1->{12},2->{12},3->{8,9},7->{7},8->{8,9},9->{8,9},10->{12},12->{2,3,7,12}] Sizebounds: (< 1,0,A>, ?) (< 1,0,B>, B) (< 1,0,C>, C) (< 2,0,A>, ?) (< 2,0,B>, B) (< 2,0,C>, C) (< 3,0,A>, B) (< 3,0,B>, C) (< 3,0,C>, C) (< 7,0,A>, ?) (< 7,0,B>, B) (< 7,0,C>, C) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, C) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<12,0,A>, ?) (<12,0,B>, B) (<12,0,C>, C) + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are removed: [1] * Step 8: ChainProcessor WORST_CASE(?,O(log(n)*n^1)) + Considered Problem: Rules: 2. mergeSort2(A,B,C) -> mergeSort(C,B,C) True (?,1) 3. mergeSort3(A,B,C) -> merge(B,C,C) True (?,1) 7. msplit(A,B,C) -> msplit(-2 + A,B,C) [A >= 2] (?,1) 8. merge(A,B,C) -> merge(-1 + A,B,C) [A >= 1 && B >= 1] (?,1) 9. merge(A,B,C) -> merge(A,-1 + B,C) [A >= 1 && B >= 1] (?,1) 10. start(A,B,C) -> mergeSort(A,B,C) True (1,1) 12. mergeSort(A,B,C) -> c4(msplit(A,D,E),mergeSort(D,D,E),mergeSort2(A,D,E),mergeSort3(A,D,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,3) Signature: {(merge,3) ;(mergeSort,3) ;(mergeSort0,3) ;(mergeSort1,3) ;(mergeSort2,3) ;(mergeSort3,3) ;(msplit,3) ;(out1msplit,3) ;(out2msplit,3) ;(start,3)} Flow Graph: [2->{12},3->{8,9},7->{7},8->{8,9},9->{8,9},10->{12},12->{2,3,7,12}] Sizebounds: (< 2,0,A>, ?) (< 2,0,B>, B) (< 2,0,C>, C) (< 3,0,A>, B) (< 3,0,B>, C) (< 3,0,C>, C) (< 7,0,A>, ?) (< 7,0,B>, B) (< 7,0,C>, C) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, C) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<12,0,A>, ?) (<12,0,B>, B) (<12,0,C>, C) + Applied Processor: ChainProcessor False [2,3,7,8,9,10,12] + Details: We chained rule 12 to obtain the rules [13] . * Step 9: UnreachableRules WORST_CASE(?,O(log(n)*n^1)) + Considered Problem: Rules: 2. mergeSort2(A,B,C) -> mergeSort(C,B,C) True (?,1) 3. mergeSort3(A,B,C) -> merge(B,C,C) True (?,1) 7. msplit(A,B,C) -> msplit(-2 + A,B,C) [A >= 2] (?,1) 8. merge(A,B,C) -> merge(-1 + A,B,C) [A >= 1 && B >= 1] (?,1) 9. merge(A,B,C) -> merge(A,-1 + B,C) [A >= 1 && B >= 1] (?,1) 10. start(A,B,C) -> mergeSort(A,B,C) True (1,1) 13. mergeSort(A,B,C) -> c4(msplit(A,D,E),mergeSort(D,D,E),mergeSort(E,D,E),mergeSort3(A,D,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,4) Signature: {(merge,3) ;(mergeSort,3) ;(mergeSort0,3) ;(mergeSort1,3) ;(mergeSort2,3) ;(mergeSort3,3) ;(msplit,3) ;(out1msplit,3) ;(out2msplit,3) ;(start,3)} Flow Graph: [2->{13},3->{8,9},7->{7},8->{8,9},9->{8,9},10->{13},13->{3,7,13}] Sizebounds: (< 2,0,A>, ?) (< 2,0,B>, B) (< 2,0,C>, C) (< 3,0,A>, B) (< 3,0,B>, C) (< 3,0,C>, C) (< 7,0,A>, ?) (< 7,0,B>, B) (< 7,0,C>, C) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, C) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<13,0,A>, ?) (<13,0,B>, B) (<13,0,C>, C) + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are removed: [2] * Step 10: ChainProcessor WORST_CASE(?,O(log(n)*n^1)) + Considered Problem: Rules: 3. mergeSort3(A,B,C) -> merge(B,C,C) True (?,1) 7. msplit(A,B,C) -> msplit(-2 + A,B,C) [A >= 2] (?,1) 8. merge(A,B,C) -> merge(-1 + A,B,C) [A >= 1 && B >= 1] (?,1) 9. merge(A,B,C) -> merge(A,-1 + B,C) [A >= 1 && B >= 1] (?,1) 10. start(A,B,C) -> mergeSort(A,B,C) True (1,1) 13. mergeSort(A,B,C) -> c4(msplit(A,D,E),mergeSort(D,D,E),mergeSort(E,D,E),mergeSort3(A,D,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,4) Signature: {(merge,3) ;(mergeSort,3) ;(mergeSort0,3) ;(mergeSort1,3) ;(mergeSort2,3) ;(mergeSort3,3) ;(msplit,3) ;(out1msplit,3) ;(out2msplit,3) ;(start,3)} Flow Graph: [3->{8,9},7->{7},8->{8,9},9->{8,9},10->{13},13->{3,7,13}] Sizebounds: (< 3,0,A>, B) (< 3,0,B>, C) (< 3,0,C>, C) (< 7,0,A>, ?) (< 7,0,B>, B) (< 7,0,C>, C) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, C) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<13,0,A>, ?) (<13,0,B>, B) (<13,0,C>, C) + Applied Processor: ChainProcessor False [3,7,8,9,10,13] + Details: We chained rule 13 to obtain the rules [14] . * Step 11: UnreachableRules WORST_CASE(?,O(log(n)*n^1)) + Considered Problem: Rules: 3. mergeSort3(A,B,C) -> merge(B,C,C) True (?,1) 7. msplit(A,B,C) -> msplit(-2 + A,B,C) [A >= 2] (?,1) 8. merge(A,B,C) -> merge(-1 + A,B,C) [A >= 1 && B >= 1] (?,1) 9. merge(A,B,C) -> merge(A,-1 + B,C) [A >= 1 && B >= 1] (?,1) 10. start(A,B,C) -> mergeSort(A,B,C) True (1,1) 14. mergeSort(A,B,C) -> c4(msplit(A,D,E),mergeSort(D,D,E),mergeSort(E,D,E),merge(D,E,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,5) Signature: {(merge,3) ;(mergeSort,3) ;(mergeSort0,3) ;(mergeSort1,3) ;(mergeSort2,3) ;(mergeSort3,3) ;(msplit,3) ;(out1msplit,3) ;(out2msplit,3) ;(start,3)} Flow Graph: [3->{8,9},7->{7},8->{8,9},9->{8,9},10->{14},14->{7,8,9,14}] Sizebounds: (< 3,0,A>, B) (< 3,0,B>, C) (< 3,0,C>, C) (< 7,0,A>, ?) (< 7,0,B>, B) (< 7,0,C>, C) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, C) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<14,0,A>, B) (<14,0,B>, C) (<14,0,C>, C) + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are removed: [3] * Step 12: LocalSizeboundsProc WORST_CASE(?,O(log(n)*n^1)) + Considered Problem: Rules: 7. msplit(A,B,C) -> msplit(-2 + A,B,C) [A >= 2] (?,1) 8. merge(A,B,C) -> merge(-1 + A,B,C) [A >= 1 && B >= 1] (?,1) 9. merge(A,B,C) -> merge(A,-1 + B,C) [A >= 1 && B >= 1] (?,1) 10. start(A,B,C) -> mergeSort(A,B,C) True (1,1) 14. mergeSort(A,B,C) -> c4(msplit(A,D,E),mergeSort(D,D,E),mergeSort(E,D,E),merge(D,E,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,5) Signature: {(merge,3) ;(mergeSort,3) ;(mergeSort0,3) ;(mergeSort1,3) ;(mergeSort2,3) ;(mergeSort3,3) ;(msplit,3) ;(out1msplit,3) ;(out2msplit,3) ;(start,3)} Flow Graph: [7->{7},8->{8,9},9->{8,9},10->{14},14->{7,8,9,14}] Sizebounds: (< 7,0,A>, ?) (< 7,0,B>, B) (< 7,0,C>, C) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, C) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<14,0,A>, B) (<14,0,B>, C) (<14,0,C>, C) + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (< 7,0,A>, 2 + A, .+ 2) (< 7,0,B>, B, .= 0) (< 7,0,C>, C, .= 0) (< 8,0,A>, 1 + A, .+ 1) (< 8,0,B>, B, .= 0) (< 8,0,C>, C, .= 0) (< 9,0,A>, A, .= 0) (< 9,0,B>, 1 + B, .+ 1) (< 9,0,C>, C, .= 0) (<10,0,A>, A, .= 0) (<10,0,B>, B, .= 0) (<10,0,C>, C, .= 0) (<14,0,A>, A, .= 0) (<14,0,B>, 1 + A, .+ 1) (<14,0,C>, A, .= 0) (<14,1,A>, 1 + A, .+ 1) (<14,1,B>, 1 + A, .+ 1) (<14,1,C>, A, .= 0) (<14,2,A>, A, .= 0) (<14,2,B>, 1 + A, .+ 1) (<14,2,C>, A, .= 0) (<14,3,A>, 1 + A, .+ 1) (<14,3,B>, A, .= 0) (<14,3,C>, A, .= 0) * Step 13: SizeboundsProc WORST_CASE(?,O(log(n)*n^1)) + Considered Problem: Rules: 7. msplit(A,B,C) -> msplit(-2 + A,B,C) [A >= 2] (?,1) 8. merge(A,B,C) -> merge(-1 + A,B,C) [A >= 1 && B >= 1] (?,1) 9. merge(A,B,C) -> merge(A,-1 + B,C) [A >= 1 && B >= 1] (?,1) 10. start(A,B,C) -> mergeSort(A,B,C) True (1,1) 14. mergeSort(A,B,C) -> c4(msplit(A,D,E),mergeSort(D,D,E),mergeSort(E,D,E),merge(D,E,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,5) Signature: {(merge,3) ;(mergeSort,3) ;(mergeSort0,3) ;(mergeSort1,3) ;(mergeSort2,3) ;(mergeSort3,3) ;(msplit,3) ;(out1msplit,3) ;(out2msplit,3) ;(start,3)} Flow Graph: [7->{7},8->{8,9},9->{8,9},10->{14},14->{7,8,9,14}] Sizebounds: (< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,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>, ?) (<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?) (<14,1,A>, ?) (<14,1,B>, ?) (<14,1,C>, ?) (<14,2,A>, ?) (<14,2,B>, ?) (<14,2,C>, ?) (<14,3,A>, ?) (<14,3,B>, ?) (<14,3,C>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (< 7,0,A>, ?) (< 7,0,B>, 1 + A) (< 7,0,C>, A) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, A) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<14,0,A>, ?) (<14,0,B>, 1 + A) (<14,0,C>, A) (<14,1,A>, ?) (<14,1,B>, 1 + A) (<14,1,C>, A) (<14,2,A>, ?) (<14,2,B>, 1 + A) (<14,2,C>, A) (<14,3,A>, ?) (<14,3,B>, A) (<14,3,C>, A) * Step 14: LoopRecurrenceProcessor WORST_CASE(?,O(log(n)*n^1)) + Considered Problem: Rules: 7. msplit(A,B,C) -> msplit(-2 + A,B,C) [A >= 2] (?,1) 8. merge(A,B,C) -> merge(-1 + A,B,C) [A >= 1 && B >= 1] (?,1) 9. merge(A,B,C) -> merge(A,-1 + B,C) [A >= 1 && B >= 1] (?,1) 10. start(A,B,C) -> mergeSort(A,B,C) True (1,1) 14. mergeSort(A,B,C) -> c4(msplit(A,D,E),mergeSort(D,D,E),mergeSort(E,D,E),merge(D,E,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,5) Signature: {(merge,3) ;(mergeSort,3) ;(mergeSort0,3) ;(mergeSort1,3) ;(mergeSort2,3) ;(mergeSort3,3) ;(msplit,3) ;(out1msplit,3) ;(out2msplit,3) ;(start,3)} Flow Graph: [7->{7},8->{8,9},9->{8,9},10->{14},14->{7,8,9,14}] Sizebounds: (< 7,0,A>, ?) (< 7,0,B>, 1 + A) (< 7,0,C>, A) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, A) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<14,0,A>, ?) (<14,0,B>, 1 + A) (<14,0,C>, A) (<14,1,A>, ?) (<14,1,B>, 1 + A) (<14,1,C>, A) (<14,2,A>, ?) (<14,2,B>, 1 + A) (<14,2,C>, A) (<14,3,A>, ?) (<14,3,B>, A) (<14,3,C>, A) + Applied Processor: LoopRecurrenceProcessor [7] + Details: Applying the recurrence pattern linear * f to the expression A yields the solution 0 . * Step 15: LoopRecurrenceProcessor WORST_CASE(?,O(log(n)*n^1)) + Considered Problem: Rules: 7. msplit(A,B,C) -> msplit(-2 + A,B,C) [A >= 2] (?,1) 8. merge(A,B,C) -> merge(-1 + A,B,C) [A >= 1 && B >= 1] (?,1) 9. merge(A,B,C) -> merge(A,-1 + B,C) [A >= 1 && B >= 1] (?,1) 10. start(A,B,C) -> mergeSort(A,B,C) True (1,1) 14. mergeSort(A,B,C) -> c4(msplit(A,D,E),mergeSort(D,D,E),mergeSort(E,D,E),merge(D,E,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,5) Signature: {(merge,3) ;(mergeSort,3) ;(mergeSort0,3) ;(mergeSort1,3) ;(mergeSort2,3) ;(mergeSort3,3) ;(msplit,3) ;(out1msplit,3) ;(out2msplit,3) ;(start,3)} Flow Graph: [7->{7},8->{8,9},9->{8,9},10->{14},14->{7,8,9,14}] Sizebounds: (< 7,0,A>, ?) (< 7,0,B>, 1 + A) (< 7,0,C>, A) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, A) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<14,0,A>, ?) (<14,0,B>, 1 + A) (<14,0,C>, A) (<14,1,A>, ?) (<14,1,B>, 1 + A) (<14,1,C>, A) (<14,2,A>, ?) (<14,2,B>, 1 + A) (<14,2,C>, A) (<14,3,A>, ?) (<14,3,B>, A) (<14,3,C>, A) + Applied Processor: LoopRecurrenceProcessor [14] + Details: Applying the recurrence pattern Master Theorem (B) to the expression A yields the solution log(A)^1*(A) + 0 . * Step 16: UnsatPaths WORST_CASE(?,O(log(n)*n^1)) + Considered Problem: Rules: 7. msplit(A,B,C) -> msplit(-2 + A,B,C) [A >= 2] (log(A)^1*(A) + 0,1) 8. merge(A,B,C) -> merge(-1 + A,B,C) [A >= 1 && B >= 1] (log(A)^1*(A) + 0,1) 9. merge(A,B,C) -> merge(A,-1 + B,C) [A >= 1 && B >= 1] (log(A)^1*(A) + 0,1) 10. start(A,B,C) -> mergeSort(A,B,C) True (1,1) 14. mergeSort(A,B,C) -> c4(msplit(A,D,E),mergeSort(D,D,E),mergeSort(E,D,E),merge(D,E,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (log(A)^1*(A) + 0,5) Signature: {(merge,3) ;(mergeSort,3) ;(mergeSort0,3) ;(mergeSort1,3) ;(mergeSort2,3) ;(mergeSort3,3) ;(msplit,3) ;(out1msplit,3) ;(out2msplit,3) ;(start,3)} Flow Graph: [7->{7},8->{8,9},9->{8,9},10->{14},14->{7,8,9,14}] Sizebounds: (< 7,0,A>, ?) (< 7,0,B>, 1 + A) (< 7,0,C>, A) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, A) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) (<14,0,A>, ?) (<14,0,B>, 1 + A) (<14,0,C>, A) (<14,1,A>, ?) (<14,1,B>, 1 + A) (<14,1,C>, A) (<14,2,A>, ?) (<14,2,B>, 1 + A) (<14,2,C>, A) (<14,3,A>, ?) (<14,3,B>, A) (<14,3,C>, A) + Applied Processor: UnsatPaths + Details: The problem is already solved. WORST_CASE(?,O(log(n)*n^1))