WORST_CASE(?,O(n^2)) * Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalaxstart(A,B,C) -> evalaxentryin(A,B,C) True (1,1) 1. evalaxentryin(A,B,C) -> evalaxbbin(0,B,C) True (?,1) 2. evalaxbbin(A,B,C) -> evalaxbb2in(A,0,C) True (?,1) 3. evalaxbb2in(A,B,C) -> evalaxbb1in(A,B,C) [C >= 2 + B] (?,1) 4. evalaxbb2in(A,B,C) -> evalaxbb3in(A,B,C) [1 + B >= C] (?,1) 5. evalaxbb1in(A,B,C) -> evalaxbb2in(A,1 + B,C) True (?,1) 6. evalaxbb3in(A,B,C) -> evalaxbbin(1 + A,B,C) [1 + B >= C && C >= 3 + A] (?,1) 7. evalaxbb3in(A,B,C) -> evalaxreturnin(A,B,C) [C >= 2 + B] (?,1) 8. evalaxbb3in(A,B,C) -> evalaxreturnin(A,B,C) [2 + A >= C] (?,1) 9. evalaxreturnin(A,B,C) -> evalaxstop(A,B,C) True (?,1) Signature: {(evalaxbb1in,3) ;(evalaxbb2in,3) ;(evalaxbb3in,3) ;(evalaxbbin,3) ;(evalaxentryin,3) ;(evalaxreturnin,3) ;(evalaxstart,3) ;(evalaxstop,3)} Flow Graph: [0->{1},1->{2},2->{3,4},3->{5},4->{6,7,8},5->{3,4},6->{2},7->{9},8->{9},9->{}] + 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>, 0, .= 0) (<1,0,B>, B, .= 0) (<1,0,C>, C, .= 0) (<2,0,A>, A, .= 0) (<2,0,B>, 0, .= 0) (<2,0,C>, C, .= 0) (<3,0,A>, A, .= 0) (<3,0,B>, B, .= 0) (<3,0,C>, C, .= 0) (<4,0,A>, A, .= 0) (<4,0,B>, B, .= 0) (<4,0,C>, C, .= 0) (<5,0,A>, A, .= 0) (<5,0,B>, 1 + B, .+ 1) (<5,0,C>, C, .= 0) (<6,0,A>, 1 + A, .+ 1) (<6,0,B>, B, .= 0) (<6,0,C>, C, .= 0) (<7,0,A>, A, .= 0) (<7,0,B>, B, .= 0) (<7,0,C>, C, .= 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) * Step 2: SizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalaxstart(A,B,C) -> evalaxentryin(A,B,C) True (1,1) 1. evalaxentryin(A,B,C) -> evalaxbbin(0,B,C) True (?,1) 2. evalaxbbin(A,B,C) -> evalaxbb2in(A,0,C) True (?,1) 3. evalaxbb2in(A,B,C) -> evalaxbb1in(A,B,C) [C >= 2 + B] (?,1) 4. evalaxbb2in(A,B,C) -> evalaxbb3in(A,B,C) [1 + B >= C] (?,1) 5. evalaxbb1in(A,B,C) -> evalaxbb2in(A,1 + B,C) True (?,1) 6. evalaxbb3in(A,B,C) -> evalaxbbin(1 + A,B,C) [1 + B >= C && C >= 3 + A] (?,1) 7. evalaxbb3in(A,B,C) -> evalaxreturnin(A,B,C) [C >= 2 + B] (?,1) 8. evalaxbb3in(A,B,C) -> evalaxreturnin(A,B,C) [2 + A >= C] (?,1) 9. evalaxreturnin(A,B,C) -> evalaxstop(A,B,C) True (?,1) Signature: {(evalaxbb1in,3) ;(evalaxbb2in,3) ;(evalaxbb3in,3) ;(evalaxbbin,3) ;(evalaxentryin,3) ;(evalaxreturnin,3) ;(evalaxstart,3) ;(evalaxstop,3)} Flow Graph: [0->{1},1->{2},2->{3,4},3->{5},4->{6,7,8},5->{3,4},6->{2},7->{9},8->{9},9->{}] 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>, ?) (<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>, ?) (<8,0,A>, ?) (<8,0,B>, ?) (<8,0,C>, ?) (<9,0,A>, ?) (<9,0,B>, ?) (<9,0,C>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) (<7,0,A>, ?) (<7,0,B>, C) (<7,0,C>, C) (<8,0,A>, ?) (<8,0,B>, C) (<8,0,C>, C) (<9,0,A>, ?) (<9,0,B>, C) (<9,0,C>, C) * Step 3: UnsatPaths WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalaxstart(A,B,C) -> evalaxentryin(A,B,C) True (1,1) 1. evalaxentryin(A,B,C) -> evalaxbbin(0,B,C) True (?,1) 2. evalaxbbin(A,B,C) -> evalaxbb2in(A,0,C) True (?,1) 3. evalaxbb2in(A,B,C) -> evalaxbb1in(A,B,C) [C >= 2 + B] (?,1) 4. evalaxbb2in(A,B,C) -> evalaxbb3in(A,B,C) [1 + B >= C] (?,1) 5. evalaxbb1in(A,B,C) -> evalaxbb2in(A,1 + B,C) True (?,1) 6. evalaxbb3in(A,B,C) -> evalaxbbin(1 + A,B,C) [1 + B >= C && C >= 3 + A] (?,1) 7. evalaxbb3in(A,B,C) -> evalaxreturnin(A,B,C) [C >= 2 + B] (?,1) 8. evalaxbb3in(A,B,C) -> evalaxreturnin(A,B,C) [2 + A >= C] (?,1) 9. evalaxreturnin(A,B,C) -> evalaxstop(A,B,C) True (?,1) Signature: {(evalaxbb1in,3) ;(evalaxbb2in,3) ;(evalaxbb3in,3) ;(evalaxbbin,3) ;(evalaxentryin,3) ;(evalaxreturnin,3) ;(evalaxstart,3) ;(evalaxstop,3)} Flow Graph: [0->{1},1->{2},2->{3,4},3->{5},4->{6,7,8},5->{3,4},6->{2},7->{9},8->{9},9->{}] Sizebounds: (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) (<7,0,A>, ?) (<7,0,B>, C) (<7,0,C>, C) (<8,0,A>, ?) (<8,0,B>, C) (<8,0,C>, C) (<9,0,A>, ?) (<9,0,B>, C) (<9,0,C>, C) + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(4,7)] * Step 4: UnreachableRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalaxstart(A,B,C) -> evalaxentryin(A,B,C) True (1,1) 1. evalaxentryin(A,B,C) -> evalaxbbin(0,B,C) True (?,1) 2. evalaxbbin(A,B,C) -> evalaxbb2in(A,0,C) True (?,1) 3. evalaxbb2in(A,B,C) -> evalaxbb1in(A,B,C) [C >= 2 + B] (?,1) 4. evalaxbb2in(A,B,C) -> evalaxbb3in(A,B,C) [1 + B >= C] (?,1) 5. evalaxbb1in(A,B,C) -> evalaxbb2in(A,1 + B,C) True (?,1) 6. evalaxbb3in(A,B,C) -> evalaxbbin(1 + A,B,C) [1 + B >= C && C >= 3 + A] (?,1) 7. evalaxbb3in(A,B,C) -> evalaxreturnin(A,B,C) [C >= 2 + B] (?,1) 8. evalaxbb3in(A,B,C) -> evalaxreturnin(A,B,C) [2 + A >= C] (?,1) 9. evalaxreturnin(A,B,C) -> evalaxstop(A,B,C) True (?,1) Signature: {(evalaxbb1in,3) ;(evalaxbb2in,3) ;(evalaxbb3in,3) ;(evalaxbbin,3) ;(evalaxentryin,3) ;(evalaxreturnin,3) ;(evalaxstart,3) ;(evalaxstop,3)} Flow Graph: [0->{1},1->{2},2->{3,4},3->{5},4->{6,8},5->{3,4},6->{2},7->{9},8->{9},9->{}] Sizebounds: (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) (<7,0,A>, ?) (<7,0,B>, C) (<7,0,C>, C) (<8,0,A>, ?) (<8,0,B>, C) (<8,0,C>, C) (<9,0,A>, ?) (<9,0,B>, C) (<9,0,C>, C) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [7] * Step 5: LeafRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalaxstart(A,B,C) -> evalaxentryin(A,B,C) True (1,1) 1. evalaxentryin(A,B,C) -> evalaxbbin(0,B,C) True (?,1) 2. evalaxbbin(A,B,C) -> evalaxbb2in(A,0,C) True (?,1) 3. evalaxbb2in(A,B,C) -> evalaxbb1in(A,B,C) [C >= 2 + B] (?,1) 4. evalaxbb2in(A,B,C) -> evalaxbb3in(A,B,C) [1 + B >= C] (?,1) 5. evalaxbb1in(A,B,C) -> evalaxbb2in(A,1 + B,C) True (?,1) 6. evalaxbb3in(A,B,C) -> evalaxbbin(1 + A,B,C) [1 + B >= C && C >= 3 + A] (?,1) 8. evalaxbb3in(A,B,C) -> evalaxreturnin(A,B,C) [2 + A >= C] (?,1) 9. evalaxreturnin(A,B,C) -> evalaxstop(A,B,C) True (?,1) Signature: {(evalaxbb1in,3) ;(evalaxbb2in,3) ;(evalaxbb3in,3) ;(evalaxbbin,3) ;(evalaxentryin,3) ;(evalaxreturnin,3) ;(evalaxstart,3) ;(evalaxstop,3)} Flow Graph: [0->{1},1->{2},2->{3,4},3->{5},4->{6,8},5->{3,4},6->{2},8->{9},9->{}] Sizebounds: (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) (<8,0,A>, ?) (<8,0,B>, C) (<8,0,C>, C) (<9,0,A>, ?) (<9,0,B>, C) (<9,0,C>, C) + Applied Processor: LeafRules + Details: The following transitions are estimated by its predecessors and are removed [8,9] * Step 6: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalaxstart(A,B,C) -> evalaxentryin(A,B,C) True (1,1) 1. evalaxentryin(A,B,C) -> evalaxbbin(0,B,C) True (?,1) 2. evalaxbbin(A,B,C) -> evalaxbb2in(A,0,C) True (?,1) 3. evalaxbb2in(A,B,C) -> evalaxbb1in(A,B,C) [C >= 2 + B] (?,1) 4. evalaxbb2in(A,B,C) -> evalaxbb3in(A,B,C) [1 + B >= C] (?,1) 5. evalaxbb1in(A,B,C) -> evalaxbb2in(A,1 + B,C) True (?,1) 6. evalaxbb3in(A,B,C) -> evalaxbbin(1 + A,B,C) [1 + B >= C && C >= 3 + A] (?,1) Signature: {(evalaxbb1in,3) ;(evalaxbb2in,3) ;(evalaxbb3in,3) ;(evalaxbbin,3) ;(evalaxentryin,3) ;(evalaxreturnin,3) ;(evalaxstart,3) ;(evalaxstop,3)} Flow Graph: [0->{1},1->{2},2->{3,4},3->{5},4->{6},5->{3,4},6->{2}] Sizebounds: (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalaxbb1in) = -2 + -1*x1 + x3 p(evalaxbb2in) = -2 + -1*x1 + x3 p(evalaxbb3in) = -2 + -1*x1 + x3 p(evalaxbbin) = -2 + -1*x1 + x3 p(evalaxentryin) = 1 + x3 p(evalaxstart) = 1 + x3 The following rules are strictly oriented: [1 + B >= C && C >= 3 + A] ==> evalaxbb3in(A,B,C) = -2 + -1*A + C > -3 + -1*A + C = evalaxbbin(1 + A,B,C) The following rules are weakly oriented: True ==> evalaxstart(A,B,C) = 1 + C >= 1 + C = evalaxentryin(A,B,C) True ==> evalaxentryin(A,B,C) = 1 + C >= -2 + C = evalaxbbin(0,B,C) True ==> evalaxbbin(A,B,C) = -2 + -1*A + C >= -2 + -1*A + C = evalaxbb2in(A,0,C) [C >= 2 + B] ==> evalaxbb2in(A,B,C) = -2 + -1*A + C >= -2 + -1*A + C = evalaxbb1in(A,B,C) [1 + B >= C] ==> evalaxbb2in(A,B,C) = -2 + -1*A + C >= -2 + -1*A + C = evalaxbb3in(A,B,C) True ==> evalaxbb1in(A,B,C) = -2 + -1*A + C >= -2 + -1*A + C = evalaxbb2in(A,1 + B,C) * Step 7: KnowledgePropagation WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalaxstart(A,B,C) -> evalaxentryin(A,B,C) True (1,1) 1. evalaxentryin(A,B,C) -> evalaxbbin(0,B,C) True (?,1) 2. evalaxbbin(A,B,C) -> evalaxbb2in(A,0,C) True (?,1) 3. evalaxbb2in(A,B,C) -> evalaxbb1in(A,B,C) [C >= 2 + B] (?,1) 4. evalaxbb2in(A,B,C) -> evalaxbb3in(A,B,C) [1 + B >= C] (?,1) 5. evalaxbb1in(A,B,C) -> evalaxbb2in(A,1 + B,C) True (?,1) 6. evalaxbb3in(A,B,C) -> evalaxbbin(1 + A,B,C) [1 + B >= C && C >= 3 + A] (1 + C,1) Signature: {(evalaxbb1in,3) ;(evalaxbb2in,3) ;(evalaxbb3in,3) ;(evalaxbbin,3) ;(evalaxentryin,3) ;(evalaxreturnin,3) ;(evalaxstart,3) ;(evalaxstop,3)} Flow Graph: [0->{1},1->{2},2->{3,4},3->{5},4->{6},5->{3,4},6->{2}] Sizebounds: (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 8: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalaxstart(A,B,C) -> evalaxentryin(A,B,C) True (1,1) 1. evalaxentryin(A,B,C) -> evalaxbbin(0,B,C) True (1,1) 2. evalaxbbin(A,B,C) -> evalaxbb2in(A,0,C) True (2 + C,1) 3. evalaxbb2in(A,B,C) -> evalaxbb1in(A,B,C) [C >= 2 + B] (?,1) 4. evalaxbb2in(A,B,C) -> evalaxbb3in(A,B,C) [1 + B >= C] (?,1) 5. evalaxbb1in(A,B,C) -> evalaxbb2in(A,1 + B,C) True (?,1) 6. evalaxbb3in(A,B,C) -> evalaxbbin(1 + A,B,C) [1 + B >= C && C >= 3 + A] (1 + C,1) Signature: {(evalaxbb1in,3) ;(evalaxbb2in,3) ;(evalaxbb3in,3) ;(evalaxbbin,3) ;(evalaxentryin,3) ;(evalaxreturnin,3) ;(evalaxstart,3) ;(evalaxstop,3)} Flow Graph: [0->{1},1->{2},2->{3,4},3->{5},4->{6},5->{3,4},6->{2}] Sizebounds: (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [4,5,3], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalaxbb1in) = 1 p(evalaxbb2in) = 1 p(evalaxbb3in) = 0 The following rules are strictly oriented: [1 + B >= C] ==> evalaxbb2in(A,B,C) = 1 > 0 = evalaxbb3in(A,B,C) The following rules are weakly oriented: [C >= 2 + B] ==> evalaxbb2in(A,B,C) = 1 >= 1 = evalaxbb1in(A,B,C) True ==> evalaxbb1in(A,B,C) = 1 >= 1 = evalaxbb2in(A,1 + B,C) We use the following global sizebounds: (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) * Step 9: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalaxstart(A,B,C) -> evalaxentryin(A,B,C) True (1,1) 1. evalaxentryin(A,B,C) -> evalaxbbin(0,B,C) True (1,1) 2. evalaxbbin(A,B,C) -> evalaxbb2in(A,0,C) True (2 + C,1) 3. evalaxbb2in(A,B,C) -> evalaxbb1in(A,B,C) [C >= 2 + B] (?,1) 4. evalaxbb2in(A,B,C) -> evalaxbb3in(A,B,C) [1 + B >= C] (2 + C,1) 5. evalaxbb1in(A,B,C) -> evalaxbb2in(A,1 + B,C) True (?,1) 6. evalaxbb3in(A,B,C) -> evalaxbbin(1 + A,B,C) [1 + B >= C && C >= 3 + A] (1 + C,1) Signature: {(evalaxbb1in,3) ;(evalaxbb2in,3) ;(evalaxbb3in,3) ;(evalaxbbin,3) ;(evalaxentryin,3) ;(evalaxreturnin,3) ;(evalaxstart,3) ;(evalaxstop,3)} Flow Graph: [0->{1},1->{2},2->{3,4},3->{5},4->{6},5->{3,4},6->{2}] Sizebounds: (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [6,4,5,3], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalaxbb1in) = 1 + -1*x2 + x3 p(evalaxbb2in) = 2 + -1*x2 + x3 p(evalaxbb3in) = 2 + -1*x2 + x3 p(evalaxbbin) = 2 + -1*x2 + x3 The following rules are strictly oriented: [C >= 2 + B] ==> evalaxbb2in(A,B,C) = 2 + -1*B + C > 1 + -1*B + C = evalaxbb1in(A,B,C) The following rules are weakly oriented: [1 + B >= C] ==> evalaxbb2in(A,B,C) = 2 + -1*B + C >= 2 + -1*B + C = evalaxbb3in(A,B,C) True ==> evalaxbb1in(A,B,C) = 1 + -1*B + C >= 1 + -1*B + C = evalaxbb2in(A,1 + B,C) [1 + B >= C && C >= 3 + A] ==> evalaxbb3in(A,B,C) = 2 + -1*B + C >= 2 + -1*B + C = evalaxbbin(1 + A,B,C) We use the following global sizebounds: (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) * Step 10: KnowledgePropagation WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalaxstart(A,B,C) -> evalaxentryin(A,B,C) True (1,1) 1. evalaxentryin(A,B,C) -> evalaxbbin(0,B,C) True (1,1) 2. evalaxbbin(A,B,C) -> evalaxbb2in(A,0,C) True (2 + C,1) 3. evalaxbb2in(A,B,C) -> evalaxbb1in(A,B,C) [C >= 2 + B] (4 + 4*C + C^2,1) 4. evalaxbb2in(A,B,C) -> evalaxbb3in(A,B,C) [1 + B >= C] (2 + C,1) 5. evalaxbb1in(A,B,C) -> evalaxbb2in(A,1 + B,C) True (?,1) 6. evalaxbb3in(A,B,C) -> evalaxbbin(1 + A,B,C) [1 + B >= C && C >= 3 + A] (1 + C,1) Signature: {(evalaxbb1in,3) ;(evalaxbb2in,3) ;(evalaxbb3in,3) ;(evalaxbbin,3) ;(evalaxentryin,3) ;(evalaxreturnin,3) ;(evalaxstart,3) ;(evalaxstop,3)} Flow Graph: [0->{1},1->{2},2->{3,4},3->{5},4->{6},5->{3,4},6->{2}] Sizebounds: (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 11: LocalSizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalaxstart(A,B,C) -> evalaxentryin(A,B,C) True (1,1) 1. evalaxentryin(A,B,C) -> evalaxbbin(0,B,C) True (1,1) 2. evalaxbbin(A,B,C) -> evalaxbb2in(A,0,C) True (2 + C,1) 3. evalaxbb2in(A,B,C) -> evalaxbb1in(A,B,C) [C >= 2 + B] (4 + 4*C + C^2,1) 4. evalaxbb2in(A,B,C) -> evalaxbb3in(A,B,C) [1 + B >= C] (2 + C,1) 5. evalaxbb1in(A,B,C) -> evalaxbb2in(A,1 + B,C) True (4 + 4*C + C^2,1) 6. evalaxbb3in(A,B,C) -> evalaxbbin(1 + A,B,C) [1 + B >= C && C >= 3 + A] (1 + C,1) Signature: {(evalaxbb1in,3) ;(evalaxbb2in,3) ;(evalaxbb3in,3) ;(evalaxbbin,3) ;(evalaxentryin,3) ;(evalaxreturnin,3) ;(evalaxstart,3) ;(evalaxstop,3)} Flow Graph: [0->{1},1->{2},2->{3,4},3->{5},4->{6},5->{3,4},6->{2}] Sizebounds: (<0,0,A>, A) (<0,0,B>, B) (<0,0,C>, C) (<1,0,A>, 0) (<1,0,B>, B) (<1,0,C>, C) (<2,0,A>, C) (<2,0,B>, 0) (<2,0,C>, C) (<3,0,A>, ?) (<3,0,B>, C) (<3,0,C>, C) (<4,0,A>, ?) (<4,0,B>, C) (<4,0,C>, C) (<5,0,A>, ?) (<5,0,B>, C) (<5,0,C>, C) (<6,0,A>, C) (<6,0,B>, C) (<6,0,C>, C) + Applied Processor: LocalSizeboundsProc + Details: The problem is already solved. WORST_CASE(?,O(n^2))