WORST_CASE(?,O(n^2)) * Step 1: RestrictVarsProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. l0(A,B) -> l1(0,B) True (1,1) 1. l1(A,B) -> c2(l2(A,B),l3(A,B)) [B >= 0] (?,1) 2. l1(A,B) -> l4(A,B) [0 >= 1 + B] (?,1) 3. l2(A,B) -> l1(C,-1 + B) [B >= 0] (?,1) 4. l3(A,B) -> l5(C,B) True (?,1) 5. l5(A,B) -> l6(1,B) True (?,1) 6. l6(A,B) -> c2(l7(A,B),l8(A,B)) [B >= 1] (?,1) 7. l6(A,B) -> l9(A,B) [0 >= B] (?,1) 8. l7(A,B) -> l9(C,B) True (?,1) 9. l8(A,B) -> l8(C,-1 + B) [B >= 1] (?,1) Signature: {(l0,2);(l1,2);(l2,2);(l3,2);(l4,2);(l5,2);(l6,2);(l7,2);(l8,2);(l9,2)} Flow Graph: [0->{1,2},1->{3,4},2->{},3->{1,2},4->{5},5->{6,7},6->{8,9},7->{},8->{},9->{9}] + Applied Processor: RestrictVarsProcessor + Details: We removed the arguments [A] . * Step 2: LocalSizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. l0(B) -> l1(B) True (1,1) 1. l1(B) -> c2(l2(B),l3(B)) [B >= 0] (?,1) 2. l1(B) -> l4(B) [0 >= 1 + B] (?,1) 3. l2(B) -> l1(-1 + B) [B >= 0] (?,1) 4. l3(B) -> l5(B) True (?,1) 5. l5(B) -> l6(B) True (?,1) 6. l6(B) -> c2(l7(B),l8(B)) [B >= 1] (?,1) 7. l6(B) -> l9(B) [0 >= B] (?,1) 8. l7(B) -> l9(B) True (?,1) 9. l8(B) -> l8(-1 + B) [B >= 1] (?,1) Signature: {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)} Flow Graph: [0->{1,2},1->{3,4},2->{},3->{1,2},4->{5},5->{6,7},6->{8,9},7->{},8->{},9->{9}] + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (<0,0,B>, B, .= 0) (<1,0,B>, B, .= 0) (<1,1,B>, B, .= 0) (<2,0,B>, B, .= 0) (<3,0,B>, 1 + B, .+ 1) (<4,0,B>, B, .= 0) (<5,0,B>, B, .= 0) (<6,0,B>, B, .= 0) (<6,1,B>, B, .= 0) (<7,0,B>, B, .= 0) (<8,0,B>, B, .= 0) (<9,0,B>, 1 + B, .+ 1) * Step 3: SizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. l0(B) -> l1(B) True (1,1) 1. l1(B) -> c2(l2(B),l3(B)) [B >= 0] (?,1) 2. l1(B) -> l4(B) [0 >= 1 + B] (?,1) 3. l2(B) -> l1(-1 + B) [B >= 0] (?,1) 4. l3(B) -> l5(B) True (?,1) 5. l5(B) -> l6(B) True (?,1) 6. l6(B) -> c2(l7(B),l8(B)) [B >= 1] (?,1) 7. l6(B) -> l9(B) [0 >= B] (?,1) 8. l7(B) -> l9(B) True (?,1) 9. l8(B) -> l8(-1 + B) [B >= 1] (?,1) Signature: {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)} Flow Graph: [0->{1,2},1->{3,4},2->{},3->{1,2},4->{5},5->{6,7},6->{8,9},7->{},8->{},9->{9}] Sizebounds: (<0,0,B>, ?) (<1,0,B>, ?) (<1,1,B>, ?) (<2,0,B>, ?) (<3,0,B>, ?) (<4,0,B>, ?) (<5,0,B>, ?) (<6,0,B>, ?) (<6,1,B>, ?) (<7,0,B>, ?) (<8,0,B>, ?) (<9,0,B>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (<0,0,B>, B) (<1,0,B>, ?) (<1,1,B>, ?) (<2,0,B>, ?) (<3,0,B>, ?) (<4,0,B>, ?) (<5,0,B>, ?) (<6,0,B>, ?) (<6,1,B>, ?) (<7,0,B>, ?) (<8,0,B>, ?) (<9,0,B>, ?) * Step 4: LeafRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. l0(B) -> l1(B) True (1,1) 1. l1(B) -> c2(l2(B),l3(B)) [B >= 0] (?,1) 2. l1(B) -> l4(B) [0 >= 1 + B] (?,1) 3. l2(B) -> l1(-1 + B) [B >= 0] (?,1) 4. l3(B) -> l5(B) True (?,1) 5. l5(B) -> l6(B) True (?,1) 6. l6(B) -> c2(l7(B),l8(B)) [B >= 1] (?,1) 7. l6(B) -> l9(B) [0 >= B] (?,1) 8. l7(B) -> l9(B) True (?,1) 9. l8(B) -> l8(-1 + B) [B >= 1] (?,1) Signature: {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)} Flow Graph: [0->{1,2},1->{3,4},2->{},3->{1,2},4->{5},5->{6,7},6->{8,9},7->{},8->{},9->{9}] Sizebounds: (<0,0,B>, B) (<1,0,B>, ?) (<1,1,B>, ?) (<2,0,B>, ?) (<3,0,B>, ?) (<4,0,B>, ?) (<5,0,B>, ?) (<6,0,B>, ?) (<6,1,B>, ?) (<7,0,B>, ?) (<8,0,B>, ?) (<9,0,B>, ?) + Applied Processor: LeafRules + Details: The following transitions are estimated by its predecessors and are removed [2,7,8] * Step 5: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. l0(B) -> l1(B) True (1,1) 1. l1(B) -> c2(l2(B),l3(B)) [B >= 0] (?,1) 3. l2(B) -> l1(-1 + B) [B >= 0] (?,1) 4. l3(B) -> l5(B) True (?,1) 5. l5(B) -> l6(B) True (?,1) 6. l6(B) -> c2(l7(B),l8(B)) [B >= 1] (?,1) 9. l8(B) -> l8(-1 + B) [B >= 1] (?,1) Signature: {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)} Flow Graph: [0->{1},1->{3,4},3->{1},4->{5},5->{6},6->{9},9->{9}] Sizebounds: (<0,0,B>, B) (<1,0,B>, ?) (<1,1,B>, ?) (<3,0,B>, ?) (<4,0,B>, ?) (<5,0,B>, ?) (<6,0,B>, ?) (<6,1,B>, ?) (<9,0,B>, ?) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [1,3], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(l1) = 1 + x1 p(l2) = 1 + x1 p(l3) = 0 The following rules are strictly oriented: [B >= 0] ==> l2(B) = 1 + B > B = l1(-1 + B) The following rules are weakly oriented: [B >= 0] ==> l1(B) = 1 + B >= 1 + B = c2(l2(B),l3(B)) We use the following global sizebounds: (<0,0,B>, B) (<1,0,B>, ?) (<1,1,B>, ?) (<3,0,B>, ?) (<4,0,B>, ?) (<5,0,B>, ?) (<6,0,B>, ?) (<6,1,B>, ?) (<9,0,B>, ?) * Step 6: KnowledgePropagation WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. l0(B) -> l1(B) True (1,1) 1. l1(B) -> c2(l2(B),l3(B)) [B >= 0] (?,1) 3. l2(B) -> l1(-1 + B) [B >= 0] (1 + B,1) 4. l3(B) -> l5(B) True (?,1) 5. l5(B) -> l6(B) True (?,1) 6. l6(B) -> c2(l7(B),l8(B)) [B >= 1] (?,1) 9. l8(B) -> l8(-1 + B) [B >= 1] (?,1) Signature: {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)} Flow Graph: [0->{1},1->{3,4},3->{1},4->{5},5->{6},6->{9},9->{9}] Sizebounds: (<0,0,B>, B) (<1,0,B>, ?) (<1,1,B>, ?) (<3,0,B>, ?) (<4,0,B>, ?) (<5,0,B>, ?) (<6,0,B>, ?) (<6,1,B>, ?) (<9,0,B>, ?) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 7: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. l0(B) -> l1(B) True (1,1) 1. l1(B) -> c2(l2(B),l3(B)) [B >= 0] (2 + B,1) 3. l2(B) -> l1(-1 + B) [B >= 0] (1 + B,1) 4. l3(B) -> l5(B) True (2 + B,1) 5. l5(B) -> l6(B) True (2 + B,1) 6. l6(B) -> c2(l7(B),l8(B)) [B >= 1] (2 + B,1) 9. l8(B) -> l8(-1 + B) [B >= 1] (?,1) Signature: {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)} Flow Graph: [0->{1},1->{3,4},3->{1},4->{5},5->{6},6->{9},9->{9}] Sizebounds: (<0,0,B>, B) (<1,0,B>, ?) (<1,1,B>, ?) (<3,0,B>, ?) (<4,0,B>, ?) (<5,0,B>, ?) (<6,0,B>, ?) (<6,1,B>, ?) (<9,0,B>, ?) + Applied Processor: ChainProcessor False [0,1,3,4,5,6,9] + Details: We chained rule 1 to obtain the rules [10] . * Step 8: UnreachableRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. l0(B) -> l1(B) True (1,1) 3. l2(B) -> l1(-1 + B) [B >= 0] (1 + B,1) 4. l3(B) -> l5(B) True (2 + B,1) 5. l5(B) -> l6(B) True (2 + B,1) 6. l6(B) -> c2(l7(B),l8(B)) [B >= 1] (2 + B,1) 9. l8(B) -> l8(-1 + B) [B >= 1] (?,1) 10. l1(B) -> c2(l1(-1 + B),l3(B)) [B >= 0 && B >= 0] (2 + B,2) Signature: {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)} Flow Graph: [0->{10},3->{10},4->{5},5->{6},6->{9},9->{9},10->{4,10}] Sizebounds: (< 0,0,B>, B) (< 3,0,B>, ?) (< 4,0,B>, ?) (< 5,0,B>, ?) (< 6,0,B>, ?) (< 6,1,B>, ?) (< 9,0,B>, ?) (<10,0,B>, ?) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [3] * Step 9: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. l0(B) -> l1(B) True (1,1) 4. l3(B) -> l5(B) True (2 + B,1) 5. l5(B) -> l6(B) True (2 + B,1) 6. l6(B) -> c2(l7(B),l8(B)) [B >= 1] (2 + B,1) 9. l8(B) -> l8(-1 + B) [B >= 1] (?,1) 10. l1(B) -> c2(l1(-1 + B),l3(B)) [B >= 0 && B >= 0] (2 + B,2) Signature: {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)} Flow Graph: [0->{10},4->{5},5->{6},6->{9},9->{9},10->{4,10}] Sizebounds: (< 0,0,B>, B) (< 4,0,B>, ?) (< 5,0,B>, ?) (< 6,0,B>, ?) (< 6,1,B>, ?) (< 9,0,B>, ?) (<10,0,B>, ?) + Applied Processor: ChainProcessor False [0,4,5,6,9,10] + Details: We chained rule 4 to obtain the rules [11] . * Step 10: UnreachableRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. l0(B) -> l1(B) True (1,1) 5. l5(B) -> l6(B) True (2 + B,1) 6. l6(B) -> c2(l7(B),l8(B)) [B >= 1] (2 + B,1) 9. l8(B) -> l8(-1 + B) [B >= 1] (?,1) 10. l1(B) -> c2(l1(-1 + B),l3(B)) [B >= 0 && B >= 0] (2 + B,2) 11. l3(B) -> l6(B) True (2 + B,2) Signature: {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)} Flow Graph: [0->{10},5->{6},6->{9},9->{9},10->{10,11},11->{6}] Sizebounds: (< 0,0,B>, B) (< 5,0,B>, ?) (< 6,0,B>, ?) (< 6,1,B>, ?) (< 9,0,B>, ?) (<10,0,B>, ?) (<11,0,B>, ?) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [5] * Step 11: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. l0(B) -> l1(B) True (1,1) 6. l6(B) -> c2(l7(B),l8(B)) [B >= 1] (2 + B,1) 9. l8(B) -> l8(-1 + B) [B >= 1] (?,1) 10. l1(B) -> c2(l1(-1 + B),l3(B)) [B >= 0 && B >= 0] (2 + B,2) 11. l3(B) -> l6(B) True (2 + B,2) Signature: {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)} Flow Graph: [0->{10},6->{9},9->{9},10->{10,11},11->{6}] Sizebounds: (< 0,0,B>, B) (< 6,0,B>, ?) (< 6,1,B>, ?) (< 9,0,B>, ?) (<10,0,B>, ?) (<11,0,B>, ?) + Applied Processor: ChainProcessor False [0,6,9,10,11] + Details: We chained rule 10 to obtain the rules [12] . * Step 12: UnreachableRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. l0(B) -> l1(B) True (1,1) 6. l6(B) -> c2(l7(B),l8(B)) [B >= 1] (2 + B,1) 9. l8(B) -> l8(-1 + B) [B >= 1] (?,1) 11. l3(B) -> l6(B) True (2 + B,2) 12. l1(B) -> c2(l1(-1 + B),l6(-1 + B)) [B >= 0 && B >= 0] (2 + B,4) Signature: {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)} Flow Graph: [0->{12},6->{9},9->{9},11->{6},12->{6,12}] Sizebounds: (< 0,0,B>, B) (< 6,0,B>, ?) (< 6,1,B>, ?) (< 9,0,B>, ?) (<11,0,B>, ?) (<12,0,B>, ?) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [11] * Step 13: LocalSizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. l0(B) -> l1(B) True (1,1) 6. l6(B) -> c2(l7(B),l8(B)) [B >= 1] (2 + B,1) 9. l8(B) -> l8(-1 + B) [B >= 1] (?,1) 12. l1(B) -> c2(l1(-1 + B),l6(-1 + B)) [B >= 0 && B >= 0] (2 + B,4) Signature: {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)} Flow Graph: [0->{12},6->{9},9->{9},12->{6,12}] Sizebounds: (< 0,0,B>, B) (< 6,0,B>, ?) (< 6,1,B>, ?) (< 9,0,B>, ?) (<12,0,B>, ?) + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (< 0,0,B>, B, .= 0) (< 6,0,B>, B, .= 0) (< 6,1,B>, B, .= 0) (< 9,0,B>, 1 + B, .+ 1) (<12,0,B>, 1 + B, .+ 1) (<12,1,B>, 1 + B, .+ 1) * Step 14: SizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. l0(B) -> l1(B) True (1,1) 6. l6(B) -> c2(l7(B),l8(B)) [B >= 1] (2 + B,1) 9. l8(B) -> l8(-1 + B) [B >= 1] (?,1) 12. l1(B) -> c2(l1(-1 + B),l6(-1 + B)) [B >= 0 && B >= 0] (2 + B,4) Signature: {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)} Flow Graph: [0->{12},6->{9},9->{9},12->{6,12}] Sizebounds: (< 0,0,B>, ?) (< 6,0,B>, ?) (< 6,1,B>, ?) (< 9,0,B>, ?) (<12,0,B>, ?) (<12,1,B>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (< 0,0,B>, B) (< 6,0,B>, 4 + 3*B) (< 6,1,B>, 4 + 3*B) (< 9,0,B>, ?) (<12,0,B>, 4 + 3*B) (<12,1,B>, 4 + 3*B) * Step 15: LocationConstraintsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. l0(B) -> l1(B) True (1,1) 6. l6(B) -> c2(l7(B),l8(B)) [B >= 1] (2 + B,1) 9. l8(B) -> l8(-1 + B) [B >= 1] (?,1) 12. l1(B) -> c2(l1(-1 + B),l6(-1 + B)) [B >= 0 && B >= 0] (2 + B,4) Signature: {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)} Flow Graph: [0->{12},6->{9},9->{9},12->{6,12}] Sizebounds: (< 0,0,B>, B) (< 6,0,B>, 4 + 3*B) (< 6,1,B>, 4 + 3*B) (< 9,0,B>, ?) (<12,0,B>, 4 + 3*B) (<12,1,B>, 4 + 3*B) + Applied Processor: LocationConstraintsProc + Details: We computed the location constraints 0 : True 6 : True 9 : True 12 : True . * Step 16: LoopRecurrenceProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. l0(B) -> l1(B) True (1,1) 6. l6(B) -> c2(l7(B),l8(B)) [B >= 1] (2 + B,1) 9. l8(B) -> l8(-1 + B) [B >= 1] (?,1) 12. l1(B) -> c2(l1(-1 + B),l6(-1 + B)) [B >= 0 && B >= 0] (2 + B,4) Signature: {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)} Flow Graph: [0->{12},6->{9},9->{9},12->{6,12}] Sizebounds: (< 0,0,B>, B) (< 6,0,B>, 4 + 3*B) (< 6,1,B>, 4 + 3*B) (< 9,0,B>, ?) (<12,0,B>, 4 + 3*B) (<12,1,B>, 4 + 3*B) + Applied Processor: LoopRecurrenceProcessor [12] + Details: Applying the recurrence pattern linear * f to the expression B yields the solution 2*B + B^2 . * Step 17: LoopRecurrenceProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. l0(B) -> l1(B) True (1,1) 6. l6(B) -> c2(l7(B),l8(B)) [B >= 1] (2 + B,1) 9. l8(B) -> l8(-1 + B) [B >= 1] (2*B + B^2,1) 12. l1(B) -> c2(l1(-1 + B),l6(-1 + B)) [B >= 0 && B >= 0] (2 + B,4) Signature: {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)} Flow Graph: [0->{12},6->{9},9->{9},12->{6,12}] Sizebounds: (< 0,0,B>, B) (< 6,0,B>, 4 + 3*B) (< 6,1,B>, 4 + 3*B) (< 9,0,B>, ?) (<12,0,B>, 4 + 3*B) (<12,1,B>, 4 + 3*B) + Applied Processor: LoopRecurrenceProcessor [9] + Details: Applying the recurrence pattern linear * f to the expression B yields the solution B . * Step 18: UnsatPaths WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. l0(B) -> l1(B) True (1,1) 6. l6(B) -> c2(l7(B),l8(B)) [B >= 1] (2 + B,1) 9. l8(B) -> l8(-1 + B) [B >= 1] (2*B + B^2,1) 12. l1(B) -> c2(l1(-1 + B),l6(-1 + B)) [B >= 0 && B >= 0] (2 + B,4) Signature: {(l0,1);(l1,1);(l2,1);(l3,1);(l4,1);(l5,1);(l6,1);(l7,1);(l8,1);(l9,1)} Flow Graph: [0->{12},6->{9},9->{9},12->{6,12}] Sizebounds: (< 0,0,B>, B) (< 6,0,B>, 4 + 3*B) (< 6,1,B>, 4 + 3*B) (< 9,0,B>, ?) (<12,0,B>, 4 + 3*B) (<12,1,B>, 4 + 3*B) + Applied Processor: UnsatPaths + Details: The problem is already solved. WORST_CASE(?,O(n^2))