WORST_CASE(?,O(n^2)) * Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (?,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (?,1) 3. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplereturnin(A,B,C,D,E) [B >= A] (?,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [E >= C] (?,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [C >= 1 + E] (?,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [0 >= 1 + F] (?,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [F >= 1] (?,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) True (?,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) True (?,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) True (?,1) 11. evalNestedMultiplereturnin(A,B,C,D,E) -> evalNestedMultiplestop(A,B,C,D,E) True (?,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Flow Graph: [0->{1},1->{2,3},2->{4,5},3->{11},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2,3},11->{}] + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (< 0,0,A>, A, .= 0) (< 0,0,B>, B, .= 0) (< 0,0,C>, C, .= 0) (< 0,0,D>, D, .= 0) (< 0,0,E>, E, .= 0) (< 1,0,A>, B, .= 0) (< 1,0,B>, A, .= 0) (< 1,0,C>, D, .= 0) (< 1,0,D>, C, .= 0) (< 1,0,E>, E, .= 0) (< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0) (< 2,0,C>, C, .= 0) (< 2,0,D>, D, .= 0) (< 2,0,E>, D, .= 0) (< 3,0,A>, A, .= 0) (< 3,0,B>, B, .= 0) (< 3,0,C>, C, .= 0) (< 3,0,D>, D, .= 0) (< 3,0,E>, E, .= 0) (< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0) (< 4,0,C>, C, .= 0) (< 4,0,D>, D, .= 0) (< 4,0,E>, E, .= 0) (< 5,0,A>, A, .= 0) (< 5,0,B>, B, .= 0) (< 5,0,C>, C, .= 0) (< 5,0,D>, D, .= 0) (< 5,0,E>, E, .= 0) (< 6,0,A>, A, .= 0) (< 6,0,B>, B, .= 0) (< 6,0,C>, C, .= 0) (< 6,0,D>, D, .= 0) (< 6,0,E>, E, .= 0) (< 7,0,A>, A, .= 0) (< 7,0,B>, B, .= 0) (< 7,0,C>, C, .= 0) (< 7,0,D>, D, .= 0) (< 7,0,E>, E, .= 0) (< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0) (< 8,0,C>, C, .= 0) (< 8,0,D>, D, .= 0) (< 8,0,E>, E, .= 0) (< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0) (< 9,0,C>, C, .= 0) (< 9,0,D>, D, .= 0) (< 9,0,E>, 1 + E, .+ 1) (<10,0,A>, A, .= 0) (<10,0,B>, 1 + B, .+ 1) (<10,0,C>, C, .= 0) (<10,0,D>, E, .= 0) (<10,0,E>, E, .= 0) (<11,0,A>, A, .= 0) (<11,0,B>, B, .= 0) (<11,0,C>, C, .= 0) (<11,0,D>, D, .= 0) (<11,0,E>, E, .= 0) * Step 2: SizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (?,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (?,1) 3. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplereturnin(A,B,C,D,E) [B >= A] (?,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [E >= C] (?,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [C >= 1 + E] (?,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [0 >= 1 + F] (?,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [F >= 1] (?,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) True (?,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) True (?,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) True (?,1) 11. evalNestedMultiplereturnin(A,B,C,D,E) -> evalNestedMultiplestop(A,B,C,D,E) True (?,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Flow Graph: [0->{1},1->{2,3},2->{4,5},3->{11},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2,3},11->{}] Sizebounds: (< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,E>, ?) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 1,0,D>, ?) (< 1,0,E>, ?) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,E>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,E>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,E>, ?) (<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 1,0,A>, B) (< 1,0,B>, A) (< 1,0,C>, D) (< 1,0,D>, C) (< 1,0,E>, E) (< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, D) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 3,0,A>, B) (< 3,0,B>, ?) (< 3,0,C>, D) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 4,0,A>, B) (< 4,0,B>, ?) (< 4,0,C>, D) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 5,0,A>, B) (< 5,0,B>, ?) (< 5,0,C>, D) (< 5,0,D>, ?) (< 5,0,E>, D) (< 6,0,A>, B) (< 6,0,B>, ?) (< 6,0,C>, D) (< 6,0,D>, ?) (< 6,0,E>, D) (< 7,0,A>, B) (< 7,0,B>, ?) (< 7,0,C>, D) (< 7,0,D>, ?) (< 7,0,E>, D) (< 8,0,A>, B) (< 8,0,B>, ?) (< 8,0,C>, D) (< 8,0,D>, ?) (< 8,0,E>, D) (< 9,0,A>, B) (< 9,0,B>, ?) (< 9,0,C>, D) (< 9,0,D>, ?) (< 9,0,E>, D) (<10,0,A>, B) (<10,0,B>, ?) (<10,0,C>, D) (<10,0,D>, ?) (<10,0,E>, ?) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, ?) (<11,0,E>, ?) * Step 3: LeafRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (?,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (?,1) 3. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplereturnin(A,B,C,D,E) [B >= A] (?,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [E >= C] (?,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [C >= 1 + E] (?,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [0 >= 1 + F] (?,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [F >= 1] (?,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) True (?,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) True (?,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) True (?,1) 11. evalNestedMultiplereturnin(A,B,C,D,E) -> evalNestedMultiplestop(A,B,C,D,E) True (?,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Flow Graph: [0->{1},1->{2,3},2->{4,5},3->{11},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2,3},11->{}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 1,0,A>, B) (< 1,0,B>, A) (< 1,0,C>, D) (< 1,0,D>, C) (< 1,0,E>, E) (< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, D) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 3,0,A>, B) (< 3,0,B>, ?) (< 3,0,C>, D) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 4,0,A>, B) (< 4,0,B>, ?) (< 4,0,C>, D) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 5,0,A>, B) (< 5,0,B>, ?) (< 5,0,C>, D) (< 5,0,D>, ?) (< 5,0,E>, D) (< 6,0,A>, B) (< 6,0,B>, ?) (< 6,0,C>, D) (< 6,0,D>, ?) (< 6,0,E>, D) (< 7,0,A>, B) (< 7,0,B>, ?) (< 7,0,C>, D) (< 7,0,D>, ?) (< 7,0,E>, D) (< 8,0,A>, B) (< 8,0,B>, ?) (< 8,0,C>, D) (< 8,0,D>, ?) (< 8,0,E>, D) (< 9,0,A>, B) (< 9,0,B>, ?) (< 9,0,C>, D) (< 9,0,D>, ?) (< 9,0,E>, D) (<10,0,A>, B) (<10,0,B>, ?) (<10,0,C>, D) (<10,0,D>, ?) (<10,0,E>, ?) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, ?) (<11,0,E>, ?) + Applied Processor: LeafRules + Details: The following transitions are estimated by its predecessors and are removed [3,11] * Step 4: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (?,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (?,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [E >= C] (?,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [C >= 1 + E] (?,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [0 >= 1 + F] (?,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [F >= 1] (?,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) True (?,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) True (?,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) True (?,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Flow Graph: [0->{1},1->{2},2->{4,5},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 1,0,A>, B) (< 1,0,B>, A) (< 1,0,C>, D) (< 1,0,D>, C) (< 1,0,E>, E) (< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, D) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 4,0,A>, B) (< 4,0,B>, ?) (< 4,0,C>, D) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 5,0,A>, B) (< 5,0,B>, ?) (< 5,0,C>, D) (< 5,0,D>, ?) (< 5,0,E>, D) (< 6,0,A>, B) (< 6,0,B>, ?) (< 6,0,C>, D) (< 6,0,D>, ?) (< 6,0,E>, D) (< 7,0,A>, B) (< 7,0,B>, ?) (< 7,0,C>, D) (< 7,0,D>, ?) (< 7,0,E>, D) (< 8,0,A>, B) (< 8,0,B>, ?) (< 8,0,C>, D) (< 8,0,D>, ?) (< 8,0,E>, D) (< 9,0,A>, B) (< 9,0,B>, ?) (< 9,0,C>, D) (< 9,0,D>, ?) (< 9,0,E>, D) (<10,0,A>, B) (<10,0,B>, ?) (<10,0,C>, D) (<10,0,D>, ?) (<10,0,E>, ?) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalNestedMultiplebb1in) = 1 + x1 + -1*x2 p(evalNestedMultiplebb2in) = 1 + x1 + -1*x2 p(evalNestedMultiplebb3in) = 1 + x1 + -1*x2 p(evalNestedMultiplebb4in) = 1 + x1 + -1*x2 p(evalNestedMultiplebb5in) = 2 + x1 + -1*x2 p(evalNestedMultipleentryin) = 2 + -1*x1 + x2 p(evalNestedMultiplestart) = 2 + -1*x1 + x2 The following rules are strictly oriented: [A >= 1 + B] ==> evalNestedMultiplebb5in(A,B,C,D,E) = 2 + A + -1*B > 1 + A + -1*B = evalNestedMultiplebb2in(A,B,C,D,D) The following rules are weakly oriented: True ==> evalNestedMultiplestart(A,B,C,D,E) = 2 + -1*A + B >= 2 + -1*A + B = evalNestedMultipleentryin(A,B,C,D,E) True ==> evalNestedMultipleentryin(A,B,C,D,E) = 2 + -1*A + B >= 2 + -1*A + B = evalNestedMultiplebb5in(B,A,D,C,E) [E >= C] ==> evalNestedMultiplebb2in(A,B,C,D,E) = 1 + A + -1*B >= 1 + A + -1*B = evalNestedMultiplebb4in(A,B,C,D,E) [C >= 1 + E] ==> evalNestedMultiplebb2in(A,B,C,D,E) = 1 + A + -1*B >= 1 + A + -1*B = evalNestedMultiplebb3in(A,B,C,D,E) [0 >= 1 + F] ==> evalNestedMultiplebb3in(A,B,C,D,E) = 1 + A + -1*B >= 1 + A + -1*B = evalNestedMultiplebb1in(A,B,C,D,E) [F >= 1] ==> evalNestedMultiplebb3in(A,B,C,D,E) = 1 + A + -1*B >= 1 + A + -1*B = evalNestedMultiplebb1in(A,B,C,D,E) True ==> evalNestedMultiplebb3in(A,B,C,D,E) = 1 + A + -1*B >= 1 + A + -1*B = evalNestedMultiplebb4in(A,B,C,D,E) True ==> evalNestedMultiplebb1in(A,B,C,D,E) = 1 + A + -1*B >= 1 + A + -1*B = evalNestedMultiplebb2in(A,B,C,D,1 + E) True ==> evalNestedMultiplebb4in(A,B,C,D,E) = 1 + A + -1*B >= 1 + A + -1*B = evalNestedMultiplebb5in(A,1 + B,C,E,E) * Step 5: KnowledgePropagation WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (?,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (2 + A + B,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [E >= C] (?,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [C >= 1 + E] (?,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [0 >= 1 + F] (?,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [F >= 1] (?,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) True (?,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) True (?,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) True (?,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Flow Graph: [0->{1},1->{2},2->{4,5},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 1,0,A>, B) (< 1,0,B>, A) (< 1,0,C>, D) (< 1,0,D>, C) (< 1,0,E>, E) (< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, D) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 4,0,A>, B) (< 4,0,B>, ?) (< 4,0,C>, D) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 5,0,A>, B) (< 5,0,B>, ?) (< 5,0,C>, D) (< 5,0,D>, ?) (< 5,0,E>, D) (< 6,0,A>, B) (< 6,0,B>, ?) (< 6,0,C>, D) (< 6,0,D>, ?) (< 6,0,E>, D) (< 7,0,A>, B) (< 7,0,B>, ?) (< 7,0,C>, D) (< 7,0,D>, ?) (< 7,0,E>, D) (< 8,0,A>, B) (< 8,0,B>, ?) (< 8,0,C>, D) (< 8,0,D>, ?) (< 8,0,E>, D) (< 9,0,A>, B) (< 9,0,B>, ?) (< 9,0,C>, D) (< 9,0,D>, ?) (< 9,0,E>, D) (<10,0,A>, B) (<10,0,B>, ?) (<10,0,C>, D) (<10,0,D>, ?) (<10,0,E>, ?) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 6: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (1,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (2 + A + B,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [E >= C] (?,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [C >= 1 + E] (?,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [0 >= 1 + F] (?,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [F >= 1] (?,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) True (?,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) True (?,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) True (?,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Flow Graph: [0->{1},1->{2},2->{4,5},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 1,0,A>, B) (< 1,0,B>, A) (< 1,0,C>, D) (< 1,0,D>, C) (< 1,0,E>, E) (< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, D) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 4,0,A>, B) (< 4,0,B>, ?) (< 4,0,C>, D) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 5,0,A>, B) (< 5,0,B>, ?) (< 5,0,C>, D) (< 5,0,D>, ?) (< 5,0,E>, D) (< 6,0,A>, B) (< 6,0,B>, ?) (< 6,0,C>, D) (< 6,0,D>, ?) (< 6,0,E>, D) (< 7,0,A>, B) (< 7,0,B>, ?) (< 7,0,C>, D) (< 7,0,D>, ?) (< 7,0,E>, D) (< 8,0,A>, B) (< 8,0,B>, ?) (< 8,0,C>, D) (< 8,0,D>, ?) (< 8,0,E>, D) (< 9,0,A>, B) (< 9,0,B>, ?) (< 9,0,C>, D) (< 9,0,D>, ?) (< 9,0,E>, D) (<10,0,A>, B) (<10,0,B>, ?) (<10,0,C>, D) (<10,0,D>, ?) (<10,0,E>, ?) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [10,4,9,6,5,7,8], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalNestedMultiplebb1in) = 1 p(evalNestedMultiplebb2in) = 1 p(evalNestedMultiplebb3in) = 1 p(evalNestedMultiplebb4in) = 1 p(evalNestedMultiplebb5in) = 0 The following rules are strictly oriented: True ==> evalNestedMultiplebb4in(A,B,C,D,E) = 1 > 0 = evalNestedMultiplebb5in(A,1 + B,C,E,E) The following rules are weakly oriented: [E >= C] ==> evalNestedMultiplebb2in(A,B,C,D,E) = 1 >= 1 = evalNestedMultiplebb4in(A,B,C,D,E) [C >= 1 + E] ==> evalNestedMultiplebb2in(A,B,C,D,E) = 1 >= 1 = evalNestedMultiplebb3in(A,B,C,D,E) [0 >= 1 + F] ==> evalNestedMultiplebb3in(A,B,C,D,E) = 1 >= 1 = evalNestedMultiplebb1in(A,B,C,D,E) [F >= 1] ==> evalNestedMultiplebb3in(A,B,C,D,E) = 1 >= 1 = evalNestedMultiplebb1in(A,B,C,D,E) True ==> evalNestedMultiplebb3in(A,B,C,D,E) = 1 >= 1 = evalNestedMultiplebb4in(A,B,C,D,E) True ==> evalNestedMultiplebb1in(A,B,C,D,E) = 1 >= 1 = evalNestedMultiplebb2in(A,B,C,D,1 + E) We use the following global sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 1,0,A>, B) (< 1,0,B>, A) (< 1,0,C>, D) (< 1,0,D>, C) (< 1,0,E>, E) (< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, D) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 4,0,A>, B) (< 4,0,B>, ?) (< 4,0,C>, D) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 5,0,A>, B) (< 5,0,B>, ?) (< 5,0,C>, D) (< 5,0,D>, ?) (< 5,0,E>, D) (< 6,0,A>, B) (< 6,0,B>, ?) (< 6,0,C>, D) (< 6,0,D>, ?) (< 6,0,E>, D) (< 7,0,A>, B) (< 7,0,B>, ?) (< 7,0,C>, D) (< 7,0,D>, ?) (< 7,0,E>, D) (< 8,0,A>, B) (< 8,0,B>, ?) (< 8,0,C>, D) (< 8,0,D>, ?) (< 8,0,E>, D) (< 9,0,A>, B) (< 9,0,B>, ?) (< 9,0,C>, D) (< 9,0,D>, ?) (< 9,0,E>, D) (<10,0,A>, B) (<10,0,B>, ?) (<10,0,C>, D) (<10,0,D>, ?) (<10,0,E>, ?) * Step 7: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (1,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (2 + A + B,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [E >= C] (?,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [C >= 1 + E] (?,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [0 >= 1 + F] (?,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [F >= 1] (?,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) True (?,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) True (?,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) True (2 + A + B,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Flow Graph: [0->{1},1->{2},2->{4,5},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 1,0,A>, B) (< 1,0,B>, A) (< 1,0,C>, D) (< 1,0,D>, C) (< 1,0,E>, E) (< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, D) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 4,0,A>, B) (< 4,0,B>, ?) (< 4,0,C>, D) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 5,0,A>, B) (< 5,0,B>, ?) (< 5,0,C>, D) (< 5,0,D>, ?) (< 5,0,E>, D) (< 6,0,A>, B) (< 6,0,B>, ?) (< 6,0,C>, D) (< 6,0,D>, ?) (< 6,0,E>, D) (< 7,0,A>, B) (< 7,0,B>, ?) (< 7,0,C>, D) (< 7,0,D>, ?) (< 7,0,E>, D) (< 8,0,A>, B) (< 8,0,B>, ?) (< 8,0,C>, D) (< 8,0,D>, ?) (< 8,0,E>, D) (< 9,0,A>, B) (< 9,0,B>, ?) (< 9,0,C>, D) (< 9,0,D>, ?) (< 9,0,E>, D) (<10,0,A>, B) (<10,0,B>, ?) (<10,0,C>, D) (<10,0,D>, ?) (<10,0,E>, ?) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [2,4,9,6,5,7,8], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalNestedMultiplebb1in) = 1 p(evalNestedMultiplebb2in) = 1 p(evalNestedMultiplebb3in) = 1 p(evalNestedMultiplebb4in) = 0 p(evalNestedMultiplebb5in) = 1 The following rules are strictly oriented: True ==> evalNestedMultiplebb3in(A,B,C,D,E) = 1 > 0 = evalNestedMultiplebb4in(A,B,C,D,E) The following rules are weakly oriented: [A >= 1 + B] ==> evalNestedMultiplebb5in(A,B,C,D,E) = 1 >= 1 = evalNestedMultiplebb2in(A,B,C,D,D) [E >= C] ==> evalNestedMultiplebb2in(A,B,C,D,E) = 1 >= 0 = evalNestedMultiplebb4in(A,B,C,D,E) [C >= 1 + E] ==> evalNestedMultiplebb2in(A,B,C,D,E) = 1 >= 1 = evalNestedMultiplebb3in(A,B,C,D,E) [0 >= 1 + F] ==> evalNestedMultiplebb3in(A,B,C,D,E) = 1 >= 1 = evalNestedMultiplebb1in(A,B,C,D,E) [F >= 1] ==> evalNestedMultiplebb3in(A,B,C,D,E) = 1 >= 1 = evalNestedMultiplebb1in(A,B,C,D,E) True ==> evalNestedMultiplebb1in(A,B,C,D,E) = 1 >= 1 = evalNestedMultiplebb2in(A,B,C,D,1 + E) We use the following global sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 1,0,A>, B) (< 1,0,B>, A) (< 1,0,C>, D) (< 1,0,D>, C) (< 1,0,E>, E) (< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, D) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 4,0,A>, B) (< 4,0,B>, ?) (< 4,0,C>, D) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 5,0,A>, B) (< 5,0,B>, ?) (< 5,0,C>, D) (< 5,0,D>, ?) (< 5,0,E>, D) (< 6,0,A>, B) (< 6,0,B>, ?) (< 6,0,C>, D) (< 6,0,D>, ?) (< 6,0,E>, D) (< 7,0,A>, B) (< 7,0,B>, ?) (< 7,0,C>, D) (< 7,0,D>, ?) (< 7,0,E>, D) (< 8,0,A>, B) (< 8,0,B>, ?) (< 8,0,C>, D) (< 8,0,D>, ?) (< 8,0,E>, D) (< 9,0,A>, B) (< 9,0,B>, ?) (< 9,0,C>, D) (< 9,0,D>, ?) (< 9,0,E>, D) (<10,0,A>, B) (<10,0,B>, ?) (<10,0,C>, D) (<10,0,D>, ?) (<10,0,E>, ?) * Step 8: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (1,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (2 + A + B,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [E >= C] (?,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [C >= 1 + E] (?,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [0 >= 1 + F] (?,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [F >= 1] (?,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) True (3 + A + B,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) True (?,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) True (2 + A + B,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Flow Graph: [0->{1},1->{2},2->{4,5},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 1,0,A>, B) (< 1,0,B>, A) (< 1,0,C>, D) (< 1,0,D>, C) (< 1,0,E>, E) (< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, D) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 4,0,A>, B) (< 4,0,B>, ?) (< 4,0,C>, D) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 5,0,A>, B) (< 5,0,B>, ?) (< 5,0,C>, D) (< 5,0,D>, ?) (< 5,0,E>, D) (< 6,0,A>, B) (< 6,0,B>, ?) (< 6,0,C>, D) (< 6,0,D>, ?) (< 6,0,E>, D) (< 7,0,A>, B) (< 7,0,B>, ?) (< 7,0,C>, D) (< 7,0,D>, ?) (< 7,0,E>, D) (< 8,0,A>, B) (< 8,0,B>, ?) (< 8,0,C>, D) (< 8,0,D>, ?) (< 8,0,E>, D) (< 9,0,A>, B) (< 9,0,B>, ?) (< 9,0,C>, D) (< 9,0,D>, ?) (< 9,0,E>, D) (<10,0,A>, B) (<10,0,B>, ?) (<10,0,C>, D) (<10,0,D>, ?) (<10,0,E>, ?) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [10,4,9,6,5,7,8], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalNestedMultiplebb1in) = 1 p(evalNestedMultiplebb2in) = 1 p(evalNestedMultiplebb3in) = 1 p(evalNestedMultiplebb4in) = 0 p(evalNestedMultiplebb5in) = 0 The following rules are strictly oriented: [E >= C] ==> evalNestedMultiplebb2in(A,B,C,D,E) = 1 > 0 = evalNestedMultiplebb4in(A,B,C,D,E) True ==> evalNestedMultiplebb3in(A,B,C,D,E) = 1 > 0 = evalNestedMultiplebb4in(A,B,C,D,E) The following rules are weakly oriented: [C >= 1 + E] ==> evalNestedMultiplebb2in(A,B,C,D,E) = 1 >= 1 = evalNestedMultiplebb3in(A,B,C,D,E) [0 >= 1 + F] ==> evalNestedMultiplebb3in(A,B,C,D,E) = 1 >= 1 = evalNestedMultiplebb1in(A,B,C,D,E) [F >= 1] ==> evalNestedMultiplebb3in(A,B,C,D,E) = 1 >= 1 = evalNestedMultiplebb1in(A,B,C,D,E) True ==> evalNestedMultiplebb1in(A,B,C,D,E) = 1 >= 1 = evalNestedMultiplebb2in(A,B,C,D,1 + E) True ==> evalNestedMultiplebb4in(A,B,C,D,E) = 0 >= 0 = evalNestedMultiplebb5in(A,1 + B,C,E,E) We use the following global sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 1,0,A>, B) (< 1,0,B>, A) (< 1,0,C>, D) (< 1,0,D>, C) (< 1,0,E>, E) (< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, D) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 4,0,A>, B) (< 4,0,B>, ?) (< 4,0,C>, D) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 5,0,A>, B) (< 5,0,B>, ?) (< 5,0,C>, D) (< 5,0,D>, ?) (< 5,0,E>, D) (< 6,0,A>, B) (< 6,0,B>, ?) (< 6,0,C>, D) (< 6,0,D>, ?) (< 6,0,E>, D) (< 7,0,A>, B) (< 7,0,B>, ?) (< 7,0,C>, D) (< 7,0,D>, ?) (< 7,0,E>, D) (< 8,0,A>, B) (< 8,0,B>, ?) (< 8,0,C>, D) (< 8,0,D>, ?) (< 8,0,E>, D) (< 9,0,A>, B) (< 9,0,B>, ?) (< 9,0,C>, D) (< 9,0,D>, ?) (< 9,0,E>, D) (<10,0,A>, B) (<10,0,B>, ?) (<10,0,C>, D) (<10,0,D>, ?) (<10,0,E>, ?) * Step 9: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (1,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (2 + A + B,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [E >= C] (2 + A + B,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [C >= 1 + E] (?,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [0 >= 1 + F] (?,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [F >= 1] (?,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) True (2 + A + B,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) True (?,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) True (2 + A + B,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Flow Graph: [0->{1},1->{2},2->{4,5},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 1,0,A>, B) (< 1,0,B>, A) (< 1,0,C>, D) (< 1,0,D>, C) (< 1,0,E>, E) (< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, D) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 4,0,A>, B) (< 4,0,B>, ?) (< 4,0,C>, D) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 5,0,A>, B) (< 5,0,B>, ?) (< 5,0,C>, D) (< 5,0,D>, ?) (< 5,0,E>, D) (< 6,0,A>, B) (< 6,0,B>, ?) (< 6,0,C>, D) (< 6,0,D>, ?) (< 6,0,E>, D) (< 7,0,A>, B) (< 7,0,B>, ?) (< 7,0,C>, D) (< 7,0,D>, ?) (< 7,0,E>, D) (< 8,0,A>, B) (< 8,0,B>, ?) (< 8,0,C>, D) (< 8,0,D>, ?) (< 8,0,E>, D) (< 9,0,A>, B) (< 9,0,B>, ?) (< 9,0,C>, D) (< 9,0,D>, ?) (< 9,0,E>, D) (<10,0,A>, B) (<10,0,B>, ?) (<10,0,C>, D) (<10,0,D>, ?) (<10,0,E>, ?) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [2,10,4,9,6,5,7], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalNestedMultiplebb1in) = 1 + x3 + -1*x5 p(evalNestedMultiplebb2in) = 2 + x3 + -1*x5 p(evalNestedMultiplebb3in) = 1 + x3 + -1*x5 p(evalNestedMultiplebb4in) = 2 + x3 + -1*x5 p(evalNestedMultiplebb5in) = 2 + x3 + -1*x4 The following rules are strictly oriented: [C >= 1 + E] ==> evalNestedMultiplebb2in(A,B,C,D,E) = 2 + C + -1*E > 1 + C + -1*E = evalNestedMultiplebb3in(A,B,C,D,E) The following rules are weakly oriented: [A >= 1 + B] ==> evalNestedMultiplebb5in(A,B,C,D,E) = 2 + C + -1*D >= 2 + C + -1*D = evalNestedMultiplebb2in(A,B,C,D,D) [E >= C] ==> evalNestedMultiplebb2in(A,B,C,D,E) = 2 + C + -1*E >= 2 + C + -1*E = evalNestedMultiplebb4in(A,B,C,D,E) [0 >= 1 + F] ==> evalNestedMultiplebb3in(A,B,C,D,E) = 1 + C + -1*E >= 1 + C + -1*E = evalNestedMultiplebb1in(A,B,C,D,E) [F >= 1] ==> evalNestedMultiplebb3in(A,B,C,D,E) = 1 + C + -1*E >= 1 + C + -1*E = evalNestedMultiplebb1in(A,B,C,D,E) True ==> evalNestedMultiplebb1in(A,B,C,D,E) = 1 + C + -1*E >= 1 + C + -1*E = evalNestedMultiplebb2in(A,B,C,D,1 + E) True ==> evalNestedMultiplebb4in(A,B,C,D,E) = 2 + C + -1*E >= 2 + C + -1*E = evalNestedMultiplebb5in(A,1 + B,C,E,E) We use the following global sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 1,0,A>, B) (< 1,0,B>, A) (< 1,0,C>, D) (< 1,0,D>, C) (< 1,0,E>, E) (< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, D) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 4,0,A>, B) (< 4,0,B>, ?) (< 4,0,C>, D) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 5,0,A>, B) (< 5,0,B>, ?) (< 5,0,C>, D) (< 5,0,D>, ?) (< 5,0,E>, D) (< 6,0,A>, B) (< 6,0,B>, ?) (< 6,0,C>, D) (< 6,0,D>, ?) (< 6,0,E>, D) (< 7,0,A>, B) (< 7,0,B>, ?) (< 7,0,C>, D) (< 7,0,D>, ?) (< 7,0,E>, D) (< 8,0,A>, B) (< 8,0,B>, ?) (< 8,0,C>, D) (< 8,0,D>, ?) (< 8,0,E>, D) (< 9,0,A>, B) (< 9,0,B>, ?) (< 9,0,C>, D) (< 9,0,D>, ?) (< 9,0,E>, D) (<10,0,A>, B) (<10,0,B>, ?) (<10,0,C>, D) (<10,0,D>, ?) (<10,0,E>, ?) * Step 10: KnowledgePropagation WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (1,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (2 + A + B,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [E >= C] (2 + A + B,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [C >= 1 + E] (6 + 2*A + 2*A*D + 2*B + 2*B*D + C + 5*D,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [0 >= 1 + F] (?,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [F >= 1] (?,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) True (2 + A + B,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) True (?,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) True (2 + A + B,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Flow Graph: [0->{1},1->{2},2->{4,5},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 1,0,A>, B) (< 1,0,B>, A) (< 1,0,C>, D) (< 1,0,D>, C) (< 1,0,E>, E) (< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, D) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 4,0,A>, B) (< 4,0,B>, ?) (< 4,0,C>, D) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 5,0,A>, B) (< 5,0,B>, ?) (< 5,0,C>, D) (< 5,0,D>, ?) (< 5,0,E>, D) (< 6,0,A>, B) (< 6,0,B>, ?) (< 6,0,C>, D) (< 6,0,D>, ?) (< 6,0,E>, D) (< 7,0,A>, B) (< 7,0,B>, ?) (< 7,0,C>, D) (< 7,0,D>, ?) (< 7,0,E>, D) (< 8,0,A>, B) (< 8,0,B>, ?) (< 8,0,C>, D) (< 8,0,D>, ?) (< 8,0,E>, D) (< 9,0,A>, B) (< 9,0,B>, ?) (< 9,0,C>, D) (< 9,0,D>, ?) (< 9,0,E>, D) (<10,0,A>, B) (<10,0,B>, ?) (<10,0,C>, D) (<10,0,D>, ?) (<10,0,E>, ?) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 11: LocalSizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (1,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (2 + A + B,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [E >= C] (2 + A + B,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [C >= 1 + E] (6 + 2*A + 2*A*D + 2*B + 2*B*D + C + 5*D,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [0 >= 1 + F] (6 + 2*A + 2*A*D + 2*B + 2*B*D + C + 5*D,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [F >= 1] (6 + 2*A + 2*A*D + 2*B + 2*B*D + C + 5*D,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) True (2 + A + B,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) True (12 + 4*A + 4*A*D + 4*B + 4*B*D + 2*C + 10*D,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) True (2 + A + B,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Flow Graph: [0->{1},1->{2},2->{4,5},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) (< 0,0,D>, D) (< 0,0,E>, E) (< 1,0,A>, B) (< 1,0,B>, A) (< 1,0,C>, D) (< 1,0,D>, C) (< 1,0,E>, E) (< 2,0,A>, B) (< 2,0,B>, B) (< 2,0,C>, D) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 4,0,A>, B) (< 4,0,B>, ?) (< 4,0,C>, D) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 5,0,A>, B) (< 5,0,B>, ?) (< 5,0,C>, D) (< 5,0,D>, ?) (< 5,0,E>, D) (< 6,0,A>, B) (< 6,0,B>, ?) (< 6,0,C>, D) (< 6,0,D>, ?) (< 6,0,E>, D) (< 7,0,A>, B) (< 7,0,B>, ?) (< 7,0,C>, D) (< 7,0,D>, ?) (< 7,0,E>, D) (< 8,0,A>, B) (< 8,0,B>, ?) (< 8,0,C>, D) (< 8,0,D>, ?) (< 8,0,E>, D) (< 9,0,A>, B) (< 9,0,B>, ?) (< 9,0,C>, D) (< 9,0,D>, ?) (< 9,0,E>, D) (<10,0,A>, B) (<10,0,B>, ?) (<10,0,C>, D) (<10,0,D>, ?) (<10,0,E>, ?) + Applied Processor: LocalSizeboundsProc + Details: The problem is already solved. WORST_CASE(?,O(n^2))