WORST_CASE(?,O(log(n))) * Step 1: LocalSizeboundsProc WORST_CASE(?,O(log(n))) + Considered Problem: Rules: 0. divByTwo(A) -> m2(A) [A >= 1] (1,1) 1. m0(A) -> m1(A) True (?,1) 2. m5(A) -> c2(m3(A),m0(A)) [A >= 1] (?,1) 3. m2(A) -> m5(A) [A >= 1] (?,1) 4. m6(A) -> m0(B) [A >= 2*B && A >= 1] (?,1) 5. m1(A) -> m6(A) True (?,1) 6. m1(A) -> m4(A) True (?,1) Signature: {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)} Flow Graph: [0->{3},1->{5,6},2->{1},3->{2},4->{1},5->{4},6->{}] + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (<0,0,A>, A, .= 0) (<1,0,A>, A, .= 0) (<2,0,A>, A, .= 0) (<2,1,A>, A, .= 0) (<3,0,A>, A, .= 0) (<4,0,A>, ?, .?) (<5,0,A>, A, .= 0) (<6,0,A>, A, .= 0) * Step 2: SizeboundsProc WORST_CASE(?,O(log(n))) + Considered Problem: Rules: 0. divByTwo(A) -> m2(A) [A >= 1] (1,1) 1. m0(A) -> m1(A) True (?,1) 2. m5(A) -> c2(m3(A),m0(A)) [A >= 1] (?,1) 3. m2(A) -> m5(A) [A >= 1] (?,1) 4. m6(A) -> m0(B) [A >= 2*B && A >= 1] (?,1) 5. m1(A) -> m6(A) True (?,1) 6. m1(A) -> m4(A) True (?,1) Signature: {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)} Flow Graph: [0->{3},1->{5,6},2->{1},3->{2},4->{1},5->{4},6->{}] Sizebounds: (<0,0,A>, ?) (<1,0,A>, ?) (<2,0,A>, ?) (<2,1,A>, ?) (<3,0,A>, ?) (<4,0,A>, ?) (<5,0,A>, ?) (<6,0,A>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (<0,0,A>, A) (<1,0,A>, ?) (<2,0,A>, A) (<2,1,A>, A) (<3,0,A>, A) (<4,0,A>, ?) (<5,0,A>, ?) (<6,0,A>, ?) * Step 3: ChainProcessor WORST_CASE(?,O(log(n))) + Considered Problem: Rules: 0. divByTwo(A) -> m2(A) [A >= 1] (1,1) 1. m0(A) -> m1(A) True (?,1) 2. m5(A) -> c2(m3(A),m0(A)) [A >= 1] (?,1) 3. m2(A) -> m5(A) [A >= 1] (?,1) 4. m6(A) -> m0(B) [A >= 2*B && A >= 1] (?,1) 5. m1(A) -> m6(A) True (?,1) 6. m1(A) -> m4(A) True (?,1) Signature: {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)} Flow Graph: [0->{3},1->{5,6},2->{1},3->{2},4->{1},5->{4},6->{}] Sizebounds: (<0,0,A>, A) (<1,0,A>, ?) (<2,0,A>, A) (<2,1,A>, A) (<3,0,A>, A) (<4,0,A>, ?) (<5,0,A>, ?) (<6,0,A>, ?) + Applied Processor: ChainProcessor False [0,1,2,3,4,5,6] + Details: We chained rule 0 to obtain the rules [7] . * Step 4: UnreachableRules WORST_CASE(?,O(log(n))) + Considered Problem: Rules: 1. m0(A) -> m1(A) True (?,1) 2. m5(A) -> c2(m3(A),m0(A)) [A >= 1] (?,1) 3. m2(A) -> m5(A) [A >= 1] (?,1) 4. m6(A) -> m0(B) [A >= 2*B && A >= 1] (?,1) 5. m1(A) -> m6(A) True (?,1) 6. m1(A) -> m4(A) True (?,1) 7. divByTwo(A) -> m5(A) [A >= 1 && A >= 1] (1,2) Signature: {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)} Flow Graph: [1->{5,6},2->{1},3->{2},4->{1},5->{4},6->{},7->{2}] Sizebounds: (<1,0,A>, ?) (<2,0,A>, A) (<2,1,A>, A) (<3,0,A>, A) (<4,0,A>, ?) (<5,0,A>, ?) (<6,0,A>, ?) (<7,0,A>, A) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [3] * Step 5: ChainProcessor WORST_CASE(?,O(log(n))) + Considered Problem: Rules: 1. m0(A) -> m1(A) True (?,1) 2. m5(A) -> c2(m3(A),m0(A)) [A >= 1] (?,1) 4. m6(A) -> m0(B) [A >= 2*B && A >= 1] (?,1) 5. m1(A) -> m6(A) True (?,1) 6. m1(A) -> m4(A) True (?,1) 7. divByTwo(A) -> m5(A) [A >= 1 && A >= 1] (1,2) Signature: {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)} Flow Graph: [1->{5,6},2->{1},4->{1},5->{4},6->{},7->{2}] Sizebounds: (<1,0,A>, ?) (<2,0,A>, A) (<2,1,A>, A) (<4,0,A>, ?) (<5,0,A>, ?) (<6,0,A>, ?) (<7,0,A>, A) + Applied Processor: ChainProcessor False [1,2,4,5,6,7] + Details: We chained rule 1 to obtain the rules [8,9] . * Step 6: UnreachableRules WORST_CASE(?,O(log(n))) + Considered Problem: Rules: 2. m5(A) -> c2(m3(A),m0(A)) [A >= 1] (?,1) 4. m6(A) -> m0(B) [A >= 2*B && A >= 1] (?,1) 5. m1(A) -> m6(A) True (?,1) 6. m1(A) -> m4(A) True (?,1) 7. divByTwo(A) -> m5(A) [A >= 1 && A >= 1] (1,2) 8. m0(A) -> m6(A) True (?,2) 9. m0(A) -> m4(A) True (?,2) Signature: {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)} Flow Graph: [2->{8,9},4->{8,9},5->{4},6->{},7->{2},8->{4},9->{}] Sizebounds: (<2,0,A>, A) (<2,1,A>, A) (<4,0,A>, ?) (<5,0,A>, ?) (<6,0,A>, ?) (<7,0,A>, A) (<8,0,A>, ?) (<9,0,A>, ?) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [5,6] * Step 7: ChainProcessor WORST_CASE(?,O(log(n))) + Considered Problem: Rules: 2. m5(A) -> c2(m3(A),m0(A)) [A >= 1] (?,1) 4. m6(A) -> m0(B) [A >= 2*B && A >= 1] (?,1) 7. divByTwo(A) -> m5(A) [A >= 1 && A >= 1] (1,2) 8. m0(A) -> m6(A) True (?,2) 9. m0(A) -> m4(A) True (?,2) Signature: {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)} Flow Graph: [2->{8,9},4->{8,9},7->{2},8->{4},9->{}] Sizebounds: (<2,0,A>, A) (<2,1,A>, A) (<4,0,A>, ?) (<7,0,A>, A) (<8,0,A>, ?) (<9,0,A>, ?) + Applied Processor: ChainProcessor False [2,4,7,8,9] + Details: We chained rule 2 to obtain the rules [10,11] . * Step 8: ChainProcessor WORST_CASE(?,O(log(n))) + Considered Problem: Rules: 4. m6(A) -> m0(B) [A >= 2*B && A >= 1] (?,1) 7. divByTwo(A) -> m5(A) [A >= 1 && A >= 1] (1,2) 8. m0(A) -> m6(A) True (?,2) 9. m0(A) -> m4(A) True (?,2) 10. m5(A) -> c2(m3(A),m6(A)) [A >= 1] (?,3) 11. m5(A) -> c2(m3(A),m4(A)) [A >= 1] (?,3) Signature: {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)} Flow Graph: [4->{8,9},7->{10,11},8->{4},9->{},10->{4},11->{}] Sizebounds: (< 4,0,A>, ?) (< 7,0,A>, A) (< 8,0,A>, ?) (< 9,0,A>, ?) (<10,0,A>, ?) (<11,0,A>, ?) + Applied Processor: ChainProcessor False [4,7,8,9,10,11] + Details: We chained rule 4 to obtain the rules [12,13] . * Step 9: UnreachableRules WORST_CASE(?,O(log(n))) + Considered Problem: Rules: 7. divByTwo(A) -> m5(A) [A >= 1 && A >= 1] (1,2) 8. m0(A) -> m6(A) True (?,2) 9. m0(A) -> m4(A) True (?,2) 10. m5(A) -> c2(m3(A),m6(A)) [A >= 1] (?,3) 11. m5(A) -> c2(m3(A),m4(A)) [A >= 1] (?,3) 12. m6(A) -> m6(B) [A >= 2*B && A >= 1] (?,3) 13. m6(A) -> m4(B) [A >= 2*B && A >= 1] (?,3) Signature: {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)} Flow Graph: [7->{10,11},8->{12,13},9->{},10->{12,13},11->{},12->{12,13},13->{}] Sizebounds: (< 7,0,A>, A) (< 8,0,A>, ?) (< 9,0,A>, ?) (<10,0,A>, ?) (<11,0,A>, ?) (<12,0,A>, ?) (<13,0,A>, ?) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [8,9] * Step 10: LeafRules WORST_CASE(?,O(log(n))) + Considered Problem: Rules: 7. divByTwo(A) -> m5(A) [A >= 1 && A >= 1] (1,2) 10. m5(A) -> c2(m3(A),m6(A)) [A >= 1] (?,3) 11. m5(A) -> c2(m3(A),m4(A)) [A >= 1] (?,3) 12. m6(A) -> m6(B) [A >= 2*B && A >= 1] (?,3) 13. m6(A) -> m4(B) [A >= 2*B && A >= 1] (?,3) Signature: {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)} Flow Graph: [7->{10,11},10->{12,13},11->{},12->{12,13},13->{}] Sizebounds: (< 7,0,A>, A) (<10,0,A>, ?) (<11,0,A>, ?) (<12,0,A>, ?) (<13,0,A>, ?) + Applied Processor: LeafRules + Details: The following transitions are estimated by its predecessors and are removed [11,13] * Step 11: LocalSizeboundsProc WORST_CASE(?,O(log(n))) + Considered Problem: Rules: 7. divByTwo(A) -> m5(A) [A >= 1 && A >= 1] (1,2) 10. m5(A) -> c2(m3(A),m6(A)) [A >= 1] (?,3) 12. m6(A) -> m6(B) [A >= 2*B && A >= 1] (?,3) Signature: {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)} Flow Graph: [7->{10},10->{12},12->{12}] Sizebounds: (< 7,0,A>, A) (<10,0,A>, ?) (<12,0,A>, ?) + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (< 7,0,A>, A, .= 0) (<10,0,A>, A, .= 0) (<10,1,A>, A, .= 0) (<12,0,A>, ?, .?) * Step 12: SizeboundsProc WORST_CASE(?,O(log(n))) + Considered Problem: Rules: 7. divByTwo(A) -> m5(A) [A >= 1 && A >= 1] (1,2) 10. m5(A) -> c2(m3(A),m6(A)) [A >= 1] (?,3) 12. m6(A) -> m6(B) [A >= 2*B && A >= 1] (?,3) Signature: {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)} Flow Graph: [7->{10},10->{12},12->{12}] Sizebounds: (< 7,0,A>, ?) (<10,0,A>, ?) (<10,1,A>, ?) (<12,0,A>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (< 7,0,A>, A) (<10,0,A>, A) (<10,1,A>, A) (<12,0,A>, ?) * Step 13: LocationConstraintsProc WORST_CASE(?,O(log(n))) + Considered Problem: Rules: 7. divByTwo(A) -> m5(A) [A >= 1 && A >= 1] (1,2) 10. m5(A) -> c2(m3(A),m6(A)) [A >= 1] (?,3) 12. m6(A) -> m6(B) [A >= 2*B && A >= 1] (?,3) Signature: {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)} Flow Graph: [7->{10},10->{12},12->{12}] Sizebounds: (< 7,0,A>, A) (<10,0,A>, A) (<10,1,A>, A) (<12,0,A>, ?) + Applied Processor: LocationConstraintsProc + Details: We computed the location constraints 7 : True 10 : [A >= 1] 12 : True . * Step 14: PolyRank WORST_CASE(?,O(log(n))) + Considered Problem: Rules: 7. divByTwo(A) -> m5(A) [A >= 1 && A >= 1] (1,2) 10. m5(A) -> c2(m3(A),m6(A)) [A >= 1] (?,3) 12. m6(A) -> m6(B) [A >= 2*B && A >= 1] (?,3) Signature: {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)} Flow Graph: [7->{10},10->{12},12->{12}] Sizebounds: (< 7,0,A>, A) (<10,0,A>, A) (<10,1,A>, A) (<12,0,A>, ?) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Constant} + Details: We apply a polynomial interpretation of shape constant: p(divByTwo) = 1 p(m3) = 0 p(m5) = 1 p(m6) = 0 The following rules are strictly oriented: [A >= 1] ==> m5(A) = 1 > 0 = c2(m3(A),m6(A)) The following rules are weakly oriented: [A >= 1 && A >= 1] ==> divByTwo(A) = 1 >= 1 = m5(A) [A >= 2*B && A >= 1] ==> m6(A) = 0 >= 0 = m6(B) * Step 15: LoopRecurrenceProcessor WORST_CASE(?,O(log(n))) + Considered Problem: Rules: 7. divByTwo(A) -> m5(A) [A >= 1 && A >= 1] (1,2) 10. m5(A) -> c2(m3(A),m6(A)) [A >= 1] (1,3) 12. m6(A) -> m6(B) [A >= 2*B && A >= 1] (?,3) Signature: {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)} Flow Graph: [7->{10},10->{12},12->{12}] Sizebounds: (< 7,0,A>, A) (<10,0,A>, A) (<10,1,A>, A) (<12,0,A>, ?) + Applied Processor: LoopRecurrenceProcessor [12] + Details: Applying the recurrence pattern log to the expression A yields the solution log(A)^1*(1) + 0 . * Step 16: UnsatPaths WORST_CASE(?,O(log(n))) + Considered Problem: Rules: 7. divByTwo(A) -> m5(A) [A >= 1 && A >= 1] (1,2) 10. m5(A) -> c2(m3(A),m6(A)) [A >= 1] (1,3) 12. m6(A) -> m6(B) [A >= 2*B && A >= 1] (log(A)^1*(1) + 0,3) Signature: {(divByTwo,1);(m0,1);(m1,1);(m2,1);(m3,1);(m4,1);(m5,1);(m6,1)} Flow Graph: [7->{10},10->{12},12->{12}] Sizebounds: (< 7,0,A>, A) (<10,0,A>, A) (<10,1,A>, A) (<12,0,A>, ?) + Applied Processor: UnsatPaths + Details: The problem is already solved. WORST_CASE(?,O(log(n)))