WORST_CASE(?,O(1)) * Step 1: RestrictVarsProcessor WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C) -> f8(0,B,C) True (1,1) 1. f8(A,B,C) -> f14(A,A,C) [0 >= A && 0 >= D] (?,1) 2. f8(A,B,C) -> f14(A,A,C) [0 >= A] (?,1) 3. f23(A,B,C) -> f28(A,B,D) [0 >= A && 0 >= 1 + E] (?,1) 4. f23(A,B,C) -> f28(A,B,D) [0 >= A] (?,1) 5. f23(A,B,C) -> f23(1 + A,B,C) [0 >= A] (?,1) 6. f28(A,B,C) -> f23(1 + A,B,C) True (?,1) 7. f28(A,B,C) -> f23(1 + A,B,C) [0 >= 1 + D] (?,1) 8. f23(A,B,C) -> f38(A,B,C) [A >= 1] (?,1) 9. f8(A,B,C) -> f8(1 + A,A,C) [0 >= A] (?,1) 10. f14(A,B,C) -> f8(1 + A,B,C) True (?,1) 11. f14(A,B,C) -> f8(1 + A,B,C) [0 >= 1 + D] (?,1) 12. f8(A,B,C) -> f23(0,B,C) [A >= 1] (?,1) Signature: {(f0,3);(f14,3);(f23,3);(f28,3);(f38,3);(f8,3)} Flow Graph: [0->{1,2,9,12},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5,8},6->{3,4,5,8},7->{3,4,5,8},8->{},9->{1 ,2,9,12},10->{1,2,9,12},11->{1,2,9,12},12->{3,4,5,8}] + Applied Processor: RestrictVarsProcessor + Details: We removed the arguments [B,C] . * Step 2: LocalSizeboundsProc WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A) -> f8(0) True (1,1) 1. f8(A) -> f14(A) [0 >= A && 0 >= D] (?,1) 2. f8(A) -> f14(A) [0 >= A] (?,1) 3. f23(A) -> f28(A) [0 >= A && 0 >= 1 + E] (?,1) 4. f23(A) -> f28(A) [0 >= A] (?,1) 5. f23(A) -> f23(1 + A) [0 >= A] (?,1) 6. f28(A) -> f23(1 + A) True (?,1) 7. f28(A) -> f23(1 + A) [0 >= 1 + D] (?,1) 8. f23(A) -> f38(A) [A >= 1] (?,1) 9. f8(A) -> f8(1 + A) [0 >= A] (?,1) 10. f14(A) -> f8(1 + A) True (?,1) 11. f14(A) -> f8(1 + A) [0 >= 1 + D] (?,1) 12. f8(A) -> f23(0) [A >= 1] (?,1) Signature: {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)} Flow Graph: [0->{1,2,9,12},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5,8},6->{3,4,5,8},7->{3,4,5,8},8->{},9->{1 ,2,9,12},10->{1,2,9,12},11->{1,2,9,12},12->{3,4,5,8}] + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (< 0,0,A>, 0, .= 0) (< 1,0,A>, A, .= 0) (< 2,0,A>, A, .= 0) (< 3,0,A>, A, .= 0) (< 4,0,A>, A, .= 0) (< 5,0,A>, 1 + A, .+ 1) (< 6,0,A>, 1 + A, .+ 1) (< 7,0,A>, 1 + A, .+ 1) (< 8,0,A>, A, .= 0) (< 9,0,A>, 1 + A, .+ 1) (<10,0,A>, 1 + A, .+ 1) (<11,0,A>, 1 + A, .+ 1) (<12,0,A>, 0, .= 0) * Step 3: SizeboundsProc WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A) -> f8(0) True (1,1) 1. f8(A) -> f14(A) [0 >= A && 0 >= D] (?,1) 2. f8(A) -> f14(A) [0 >= A] (?,1) 3. f23(A) -> f28(A) [0 >= A && 0 >= 1 + E] (?,1) 4. f23(A) -> f28(A) [0 >= A] (?,1) 5. f23(A) -> f23(1 + A) [0 >= A] (?,1) 6. f28(A) -> f23(1 + A) True (?,1) 7. f28(A) -> f23(1 + A) [0 >= 1 + D] (?,1) 8. f23(A) -> f38(A) [A >= 1] (?,1) 9. f8(A) -> f8(1 + A) [0 >= A] (?,1) 10. f14(A) -> f8(1 + A) True (?,1) 11. f14(A) -> f8(1 + A) [0 >= 1 + D] (?,1) 12. f8(A) -> f23(0) [A >= 1] (?,1) Signature: {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)} Flow Graph: [0->{1,2,9,12},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5,8},6->{3,4,5,8},7->{3,4,5,8},8->{},9->{1 ,2,9,12},10->{1,2,9,12},11->{1,2,9,12},12->{3,4,5,8}] Sizebounds: (< 0,0,A>, ?) (< 1,0,A>, ?) (< 2,0,A>, ?) (< 3,0,A>, ?) (< 4,0,A>, ?) (< 5,0,A>, ?) (< 6,0,A>, ?) (< 7,0,A>, ?) (< 8,0,A>, ?) (< 9,0,A>, ?) (<10,0,A>, ?) (<11,0,A>, ?) (<12,0,A>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (< 0,0,A>, 0) (< 1,0,A>, 0) (< 2,0,A>, 0) (< 3,0,A>, 0) (< 4,0,A>, 0) (< 5,0,A>, 1) (< 6,0,A>, 0) (< 7,0,A>, 0) (< 8,0,A>, 1) (< 9,0,A>, 1) (<10,0,A>, 0) (<11,0,A>, 0) (<12,0,A>, 0) * Step 4: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A) -> f8(0) True (1,1) 1. f8(A) -> f14(A) [0 >= A && 0 >= D] (?,1) 2. f8(A) -> f14(A) [0 >= A] (?,1) 3. f23(A) -> f28(A) [0 >= A && 0 >= 1 + E] (?,1) 4. f23(A) -> f28(A) [0 >= A] (?,1) 5. f23(A) -> f23(1 + A) [0 >= A] (?,1) 6. f28(A) -> f23(1 + A) True (?,1) 7. f28(A) -> f23(1 + A) [0 >= 1 + D] (?,1) 8. f23(A) -> f38(A) [A >= 1] (?,1) 9. f8(A) -> f8(1 + A) [0 >= A] (?,1) 10. f14(A) -> f8(1 + A) True (?,1) 11. f14(A) -> f8(1 + A) [0 >= 1 + D] (?,1) 12. f8(A) -> f23(0) [A >= 1] (?,1) Signature: {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)} Flow Graph: [0->{1,2,9,12},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5,8},6->{3,4,5,8},7->{3,4,5,8},8->{},9->{1 ,2,9,12},10->{1,2,9,12},11->{1,2,9,12},12->{3,4,5,8}] Sizebounds: (< 0,0,A>, 0) (< 1,0,A>, 0) (< 2,0,A>, 0) (< 3,0,A>, 0) (< 4,0,A>, 0) (< 5,0,A>, 1) (< 6,0,A>, 0) (< 7,0,A>, 0) (< 8,0,A>, 1) (< 9,0,A>, 1) (<10,0,A>, 0) (<11,0,A>, 0) (<12,0,A>, 0) + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,12),(12,8)] * Step 5: LeafRules WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A) -> f8(0) True (1,1) 1. f8(A) -> f14(A) [0 >= A && 0 >= D] (?,1) 2. f8(A) -> f14(A) [0 >= A] (?,1) 3. f23(A) -> f28(A) [0 >= A && 0 >= 1 + E] (?,1) 4. f23(A) -> f28(A) [0 >= A] (?,1) 5. f23(A) -> f23(1 + A) [0 >= A] (?,1) 6. f28(A) -> f23(1 + A) True (?,1) 7. f28(A) -> f23(1 + A) [0 >= 1 + D] (?,1) 8. f23(A) -> f38(A) [A >= 1] (?,1) 9. f8(A) -> f8(1 + A) [0 >= A] (?,1) 10. f14(A) -> f8(1 + A) True (?,1) 11. f14(A) -> f8(1 + A) [0 >= 1 + D] (?,1) 12. f8(A) -> f23(0) [A >= 1] (?,1) Signature: {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)} Flow Graph: [0->{1,2,9},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5,8},6->{3,4,5,8},7->{3,4,5,8},8->{},9->{1,2,9 ,12},10->{1,2,9,12},11->{1,2,9,12},12->{3,4,5}] Sizebounds: (< 0,0,A>, 0) (< 1,0,A>, 0) (< 2,0,A>, 0) (< 3,0,A>, 0) (< 4,0,A>, 0) (< 5,0,A>, 1) (< 6,0,A>, 0) (< 7,0,A>, 0) (< 8,0,A>, 1) (< 9,0,A>, 1) (<10,0,A>, 0) (<11,0,A>, 0) (<12,0,A>, 0) + Applied Processor: LeafRules + Details: The following transitions are estimated by its predecessors and are removed [8] * Step 6: PolyRank WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A) -> f8(0) True (1,1) 1. f8(A) -> f14(A) [0 >= A && 0 >= D] (?,1) 2. f8(A) -> f14(A) [0 >= A] (?,1) 3. f23(A) -> f28(A) [0 >= A && 0 >= 1 + E] (?,1) 4. f23(A) -> f28(A) [0 >= A] (?,1) 5. f23(A) -> f23(1 + A) [0 >= A] (?,1) 6. f28(A) -> f23(1 + A) True (?,1) 7. f28(A) -> f23(1 + A) [0 >= 1 + D] (?,1) 9. f8(A) -> f8(1 + A) [0 >= A] (?,1) 10. f14(A) -> f8(1 + A) True (?,1) 11. f14(A) -> f8(1 + A) [0 >= 1 + D] (?,1) 12. f8(A) -> f23(0) [A >= 1] (?,1) Signature: {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)} Flow Graph: [0->{1,2,9},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5},6->{3,4,5},7->{3,4,5},9->{1,2,9,12},10->{1 ,2,9,12},11->{1,2,9,12},12->{3,4,5}] Sizebounds: (< 0,0,A>, 0) (< 1,0,A>, 0) (< 2,0,A>, 0) (< 3,0,A>, 0) (< 4,0,A>, 0) (< 5,0,A>, 1) (< 6,0,A>, 0) (< 7,0,A>, 0) (< 9,0,A>, 1) (<10,0,A>, 0) (<11,0,A>, 0) (<12,0,A>, 0) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f0) = 1 p(f14) = 1 p(f23) = 0 p(f28) = 0 p(f8) = 1 The following rules are strictly oriented: [A >= 1] ==> f8(A) = 1 > 0 = f23(0) The following rules are weakly oriented: True ==> f0(A) = 1 >= 1 = f8(0) [0 >= A && 0 >= D] ==> f8(A) = 1 >= 1 = f14(A) [0 >= A] ==> f8(A) = 1 >= 1 = f14(A) [0 >= A && 0 >= 1 + E] ==> f23(A) = 0 >= 0 = f28(A) [0 >= A] ==> f23(A) = 0 >= 0 = f28(A) [0 >= A] ==> f23(A) = 0 >= 0 = f23(1 + A) True ==> f28(A) = 0 >= 0 = f23(1 + A) [0 >= 1 + D] ==> f28(A) = 0 >= 0 = f23(1 + A) [0 >= A] ==> f8(A) = 1 >= 1 = f8(1 + A) True ==> f14(A) = 1 >= 1 = f8(1 + A) [0 >= 1 + D] ==> f14(A) = 1 >= 1 = f8(1 + A) * Step 7: PolyRank WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A) -> f8(0) True (1,1) 1. f8(A) -> f14(A) [0 >= A && 0 >= D] (?,1) 2. f8(A) -> f14(A) [0 >= A] (?,1) 3. f23(A) -> f28(A) [0 >= A && 0 >= 1 + E] (?,1) 4. f23(A) -> f28(A) [0 >= A] (?,1) 5. f23(A) -> f23(1 + A) [0 >= A] (?,1) 6. f28(A) -> f23(1 + A) True (?,1) 7. f28(A) -> f23(1 + A) [0 >= 1 + D] (?,1) 9. f8(A) -> f8(1 + A) [0 >= A] (?,1) 10. f14(A) -> f8(1 + A) True (?,1) 11. f14(A) -> f8(1 + A) [0 >= 1 + D] (?,1) 12. f8(A) -> f23(0) [A >= 1] (1,1) Signature: {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)} Flow Graph: [0->{1,2,9},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5},6->{3,4,5},7->{3,4,5},9->{1,2,9,12},10->{1 ,2,9,12},11->{1,2,9,12},12->{3,4,5}] Sizebounds: (< 0,0,A>, 0) (< 1,0,A>, 0) (< 2,0,A>, 0) (< 3,0,A>, 0) (< 4,0,A>, 0) (< 5,0,A>, 1) (< 6,0,A>, 0) (< 7,0,A>, 0) (< 9,0,A>, 1) (<10,0,A>, 0) (<11,0,A>, 0) (<12,0,A>, 0) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f0) = 2 p(f14) = 2 p(f23) = 2 + -1*x1 p(f28) = 1 + -1*x1 p(f8) = 2 The following rules are strictly oriented: [0 >= A] ==> f23(A) = 2 + -1*A > 1 + -1*A = f28(A) [0 >= A] ==> f23(A) = 2 + -1*A > 1 + -1*A = f23(1 + A) The following rules are weakly oriented: True ==> f0(A) = 2 >= 2 = f8(0) [0 >= A && 0 >= D] ==> f8(A) = 2 >= 2 = f14(A) [0 >= A] ==> f8(A) = 2 >= 2 = f14(A) [0 >= A && 0 >= 1 + E] ==> f23(A) = 2 + -1*A >= 1 + -1*A = f28(A) True ==> f28(A) = 1 + -1*A >= 1 + -1*A = f23(1 + A) [0 >= 1 + D] ==> f28(A) = 1 + -1*A >= 1 + -1*A = f23(1 + A) [0 >= A] ==> f8(A) = 2 >= 2 = f8(1 + A) True ==> f14(A) = 2 >= 2 = f8(1 + A) [0 >= 1 + D] ==> f14(A) = 2 >= 2 = f8(1 + A) [A >= 1] ==> f8(A) = 2 >= 2 = f23(0) * Step 8: PolyRank WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A) -> f8(0) True (1,1) 1. f8(A) -> f14(A) [0 >= A && 0 >= D] (?,1) 2. f8(A) -> f14(A) [0 >= A] (?,1) 3. f23(A) -> f28(A) [0 >= A && 0 >= 1 + E] (?,1) 4. f23(A) -> f28(A) [0 >= A] (2,1) 5. f23(A) -> f23(1 + A) [0 >= A] (2,1) 6. f28(A) -> f23(1 + A) True (?,1) 7. f28(A) -> f23(1 + A) [0 >= 1 + D] (?,1) 9. f8(A) -> f8(1 + A) [0 >= A] (?,1) 10. f14(A) -> f8(1 + A) True (?,1) 11. f14(A) -> f8(1 + A) [0 >= 1 + D] (?,1) 12. f8(A) -> f23(0) [A >= 1] (1,1) Signature: {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)} Flow Graph: [0->{1,2,9},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5},6->{3,4,5},7->{3,4,5},9->{1,2,9,12},10->{1 ,2,9,12},11->{1,2,9,12},12->{3,4,5}] Sizebounds: (< 0,0,A>, 0) (< 1,0,A>, 0) (< 2,0,A>, 0) (< 3,0,A>, 0) (< 4,0,A>, 0) (< 5,0,A>, 1) (< 6,0,A>, 0) (< 7,0,A>, 0) (< 9,0,A>, 1) (<10,0,A>, 0) (<11,0,A>, 0) (<12,0,A>, 0) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f0) = 1 p(f14) = 1 p(f23) = 1 + -1*x1 p(f28) = -1*x1 p(f8) = 1 The following rules are strictly oriented: [0 >= A && 0 >= 1 + E] ==> f23(A) = 1 + -1*A > -1*A = f28(A) [0 >= A] ==> f23(A) = 1 + -1*A > -1*A = f28(A) [0 >= A] ==> f23(A) = 1 + -1*A > -1*A = f23(1 + A) The following rules are weakly oriented: True ==> f0(A) = 1 >= 1 = f8(0) [0 >= A && 0 >= D] ==> f8(A) = 1 >= 1 = f14(A) [0 >= A] ==> f8(A) = 1 >= 1 = f14(A) True ==> f28(A) = -1*A >= -1*A = f23(1 + A) [0 >= 1 + D] ==> f28(A) = -1*A >= -1*A = f23(1 + A) [0 >= A] ==> f8(A) = 1 >= 1 = f8(1 + A) True ==> f14(A) = 1 >= 1 = f8(1 + A) [0 >= 1 + D] ==> f14(A) = 1 >= 1 = f8(1 + A) [A >= 1] ==> f8(A) = 1 >= 1 = f23(0) * Step 9: KnowledgePropagation WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A) -> f8(0) True (1,1) 1. f8(A) -> f14(A) [0 >= A && 0 >= D] (?,1) 2. f8(A) -> f14(A) [0 >= A] (?,1) 3. f23(A) -> f28(A) [0 >= A && 0 >= 1 + E] (1,1) 4. f23(A) -> f28(A) [0 >= A] (1,1) 5. f23(A) -> f23(1 + A) [0 >= A] (1,1) 6. f28(A) -> f23(1 + A) True (?,1) 7. f28(A) -> f23(1 + A) [0 >= 1 + D] (?,1) 9. f8(A) -> f8(1 + A) [0 >= A] (?,1) 10. f14(A) -> f8(1 + A) True (?,1) 11. f14(A) -> f8(1 + A) [0 >= 1 + D] (?,1) 12. f8(A) -> f23(0) [A >= 1] (1,1) Signature: {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)} Flow Graph: [0->{1,2,9},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5},6->{3,4,5},7->{3,4,5},9->{1,2,9,12},10->{1 ,2,9,12},11->{1,2,9,12},12->{3,4,5}] Sizebounds: (< 0,0,A>, 0) (< 1,0,A>, 0) (< 2,0,A>, 0) (< 3,0,A>, 0) (< 4,0,A>, 0) (< 5,0,A>, 1) (< 6,0,A>, 0) (< 7,0,A>, 0) (< 9,0,A>, 1) (<10,0,A>, 0) (<11,0,A>, 0) (<12,0,A>, 0) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 10: PolyRank WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A) -> f8(0) True (1,1) 1. f8(A) -> f14(A) [0 >= A && 0 >= D] (?,1) 2. f8(A) -> f14(A) [0 >= A] (?,1) 3. f23(A) -> f28(A) [0 >= A && 0 >= 1 + E] (1,1) 4. f23(A) -> f28(A) [0 >= A] (1,1) 5. f23(A) -> f23(1 + A) [0 >= A] (1,1) 6. f28(A) -> f23(1 + A) True (2,1) 7. f28(A) -> f23(1 + A) [0 >= 1 + D] (2,1) 9. f8(A) -> f8(1 + A) [0 >= A] (?,1) 10. f14(A) -> f8(1 + A) True (?,1) 11. f14(A) -> f8(1 + A) [0 >= 1 + D] (?,1) 12. f8(A) -> f23(0) [A >= 1] (1,1) Signature: {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)} Flow Graph: [0->{1,2,9},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5},6->{3,4,5},7->{3,4,5},9->{1,2,9,12},10->{1 ,2,9,12},11->{1,2,9,12},12->{3,4,5}] Sizebounds: (< 0,0,A>, 0) (< 1,0,A>, 0) (< 2,0,A>, 0) (< 3,0,A>, 0) (< 4,0,A>, 0) (< 5,0,A>, 1) (< 6,0,A>, 0) (< 7,0,A>, 0) (< 9,0,A>, 1) (<10,0,A>, 0) (<11,0,A>, 0) (<12,0,A>, 0) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [1,9,10,2,11], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f14) = 1 + -1*x1 p(f8) = 2 + -1*x1 The following rules are strictly oriented: [0 >= A] ==> f8(A) = 2 + -1*A > 1 + -1*A = f14(A) [0 >= A] ==> f8(A) = 2 + -1*A > 1 + -1*A = f8(1 + A) The following rules are weakly oriented: [0 >= A && 0 >= D] ==> f8(A) = 2 + -1*A >= 1 + -1*A = f14(A) True ==> f14(A) = 1 + -1*A >= 1 + -1*A = f8(1 + A) [0 >= 1 + D] ==> f14(A) = 1 + -1*A >= 1 + -1*A = f8(1 + A) We use the following global sizebounds: (< 0,0,A>, 0) (< 1,0,A>, 0) (< 2,0,A>, 0) (< 3,0,A>, 0) (< 4,0,A>, 0) (< 5,0,A>, 1) (< 6,0,A>, 0) (< 7,0,A>, 0) (< 9,0,A>, 1) (<10,0,A>, 0) (<11,0,A>, 0) (<12,0,A>, 0) * Step 11: PolyRank WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A) -> f8(0) True (1,1) 1. f8(A) -> f14(A) [0 >= A && 0 >= D] (?,1) 2. f8(A) -> f14(A) [0 >= A] (2,1) 3. f23(A) -> f28(A) [0 >= A && 0 >= 1 + E] (1,1) 4. f23(A) -> f28(A) [0 >= A] (1,1) 5. f23(A) -> f23(1 + A) [0 >= A] (1,1) 6. f28(A) -> f23(1 + A) True (2,1) 7. f28(A) -> f23(1 + A) [0 >= 1 + D] (2,1) 9. f8(A) -> f8(1 + A) [0 >= A] (2,1) 10. f14(A) -> f8(1 + A) True (?,1) 11. f14(A) -> f8(1 + A) [0 >= 1 + D] (?,1) 12. f8(A) -> f23(0) [A >= 1] (1,1) Signature: {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)} Flow Graph: [0->{1,2,9},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5},6->{3,4,5},7->{3,4,5},9->{1,2,9,12},10->{1 ,2,9,12},11->{1,2,9,12},12->{3,4,5}] Sizebounds: (< 0,0,A>, 0) (< 1,0,A>, 0) (< 2,0,A>, 0) (< 3,0,A>, 0) (< 4,0,A>, 0) (< 5,0,A>, 1) (< 6,0,A>, 0) (< 7,0,A>, 0) (< 9,0,A>, 1) (<10,0,A>, 0) (<11,0,A>, 0) (<12,0,A>, 0) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [1,10,2,11], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f14) = 1 + -1*x1 p(f8) = 2 + -1*x1 The following rules are strictly oriented: [0 >= A && 0 >= D] ==> f8(A) = 2 + -1*A > 1 + -1*A = f14(A) [0 >= A] ==> f8(A) = 2 + -1*A > 1 + -1*A = f14(A) The following rules are weakly oriented: True ==> f14(A) = 1 + -1*A >= 1 + -1*A = f8(1 + A) [0 >= 1 + D] ==> f14(A) = 1 + -1*A >= 1 + -1*A = f8(1 + A) We use the following global sizebounds: (< 0,0,A>, 0) (< 1,0,A>, 0) (< 2,0,A>, 0) (< 3,0,A>, 0) (< 4,0,A>, 0) (< 5,0,A>, 1) (< 6,0,A>, 0) (< 7,0,A>, 0) (< 9,0,A>, 1) (<10,0,A>, 0) (<11,0,A>, 0) (<12,0,A>, 0) * Step 12: KnowledgePropagation WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A) -> f8(0) True (1,1) 1. f8(A) -> f14(A) [0 >= A && 0 >= D] (8,1) 2. f8(A) -> f14(A) [0 >= A] (2,1) 3. f23(A) -> f28(A) [0 >= A && 0 >= 1 + E] (1,1) 4. f23(A) -> f28(A) [0 >= A] (1,1) 5. f23(A) -> f23(1 + A) [0 >= A] (1,1) 6. f28(A) -> f23(1 + A) True (2,1) 7. f28(A) -> f23(1 + A) [0 >= 1 + D] (2,1) 9. f8(A) -> f8(1 + A) [0 >= A] (2,1) 10. f14(A) -> f8(1 + A) True (?,1) 11. f14(A) -> f8(1 + A) [0 >= 1 + D] (?,1) 12. f8(A) -> f23(0) [A >= 1] (1,1) Signature: {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)} Flow Graph: [0->{1,2,9},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5},6->{3,4,5},7->{3,4,5},9->{1,2,9,12},10->{1 ,2,9,12},11->{1,2,9,12},12->{3,4,5}] Sizebounds: (< 0,0,A>, 0) (< 1,0,A>, 0) (< 2,0,A>, 0) (< 3,0,A>, 0) (< 4,0,A>, 0) (< 5,0,A>, 1) (< 6,0,A>, 0) (< 7,0,A>, 0) (< 9,0,A>, 1) (<10,0,A>, 0) (<11,0,A>, 0) (<12,0,A>, 0) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 13: LocalSizeboundsProc WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A) -> f8(0) True (1,1) 1. f8(A) -> f14(A) [0 >= A && 0 >= D] (8,1) 2. f8(A) -> f14(A) [0 >= A] (2,1) 3. f23(A) -> f28(A) [0 >= A && 0 >= 1 + E] (1,1) 4. f23(A) -> f28(A) [0 >= A] (1,1) 5. f23(A) -> f23(1 + A) [0 >= A] (1,1) 6. f28(A) -> f23(1 + A) True (2,1) 7. f28(A) -> f23(1 + A) [0 >= 1 + D] (2,1) 9. f8(A) -> f8(1 + A) [0 >= A] (2,1) 10. f14(A) -> f8(1 + A) True (10,1) 11. f14(A) -> f8(1 + A) [0 >= 1 + D] (10,1) 12. f8(A) -> f23(0) [A >= 1] (1,1) Signature: {(f0,1);(f14,1);(f23,1);(f28,1);(f38,1);(f8,1)} Flow Graph: [0->{1,2,9},1->{10,11},2->{10,11},3->{6,7},4->{6,7},5->{3,4,5},6->{3,4,5},7->{3,4,5},9->{1,2,9,12},10->{1 ,2,9,12},11->{1,2,9,12},12->{3,4,5}] Sizebounds: (< 0,0,A>, 0) (< 1,0,A>, 0) (< 2,0,A>, 0) (< 3,0,A>, 0) (< 4,0,A>, 0) (< 5,0,A>, 1) (< 6,0,A>, 0) (< 7,0,A>, 0) (< 9,0,A>, 1) (<10,0,A>, 0) (<11,0,A>, 0) (<12,0,A>, 0) + Applied Processor: LocalSizeboundsProc + Details: The problem is already solved. WORST_CASE(?,O(1))