MAYBE Initial complexity problem: 1: T: (1, 1) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultipleentryin(a, b, c, d, e) (?, 1) evalNestedMultipleentryin(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e) (?, 1) evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ] (?, 1) evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplereturnin(a, b, c, d, e) [ b >= a ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) [ e >= c ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ 0 >= f + 1 ] (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ f >= 1 ] (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) (?, 1) evalNestedMultiplebb1in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) (?, 1) evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e) (?, 1) evalNestedMultiplereturnin(a, b, c, d, e) -> evalNestedMultiplestop(a, b, c, d, e) start location: evalNestedMultiplestart leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem: 2: T: (1, 1) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultipleentryin(a, b, c, d, e) (?, 1) evalNestedMultipleentryin(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e) (?, 1) evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) [ e >= c ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ 0 >= f + 1 ] (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ f >= 1 ] (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) (?, 1) evalNestedMultiplebb1in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) (?, 1) evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e) start location: evalNestedMultiplestart leaf cost: 2 Repeatedly propagating knowledge in problem 2 produces the following problem: 3: T: (1, 1) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultipleentryin(a, b, c, d, e) (1, 1) evalNestedMultipleentryin(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e) (?, 1) evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) [ e >= c ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ 0 >= f + 1 ] (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ f >= 1 ] (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) (?, 1) evalNestedMultiplebb1in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) (?, 1) evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e) start location: evalNestedMultiplestart leaf cost: 2 A polynomial rank function with Pol(evalNestedMultiplestart) = -3*V_1 + 3*V_2 Pol(evalNestedMultipleentryin) = -3*V_1 + 3*V_2 Pol(evalNestedMultiplebb5in) = 3*V_1 - 3*V_2 Pol(evalNestedMultiplebb2in) = 3*V_1 - 3*V_2 - 1 Pol(evalNestedMultiplebb4in) = 3*V_1 - 3*V_2 - 2 Pol(evalNestedMultiplebb3in) = 3*V_1 - 3*V_2 - 1 Pol(evalNestedMultiplebb1in) = 3*V_1 - 3*V_2 - 1 orients all transitions weakly and the transition evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ] strictly and produces the following problem: 4: T: (1, 1) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultipleentryin(a, b, c, d, e) (1, 1) evalNestedMultipleentryin(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e) (3*a + 3*b, 1) evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) [ e >= c ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ 0 >= f + 1 ] (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ f >= 1 ] (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) (?, 1) evalNestedMultiplebb1in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) (?, 1) evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e) start location: evalNestedMultiplestart leaf cost: 2 A polynomial rank function with Pol(evalNestedMultiplebb4in) = 1 Pol(evalNestedMultiplebb5in) = 0 Pol(evalNestedMultiplebb3in) = 2 Pol(evalNestedMultiplebb1in) = 2 Pol(evalNestedMultiplebb2in) = 2 and size complexities S("evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e)", 0-0) = b S("evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e)", 0-1) = ? S("evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e)", 0-2) = d S("evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e)", 0-3) = ? S("evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e)", 0-4) = ? S("evalNestedMultiplebb1in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1)", 0-0) = b S("evalNestedMultiplebb1in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1)", 0-1) = ? S("evalNestedMultiplebb1in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1)", 0-2) = d S("evalNestedMultiplebb1in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1)", 0-3) = ? S("evalNestedMultiplebb1in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1)", 0-4) = ? S("evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e)", 0-0) = b S("evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e)", 0-1) = ? S("evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e)", 0-2) = d S("evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e)", 0-3) = ? S("evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e)", 0-4) = ? S("evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ f >= 1 ]", 0-0) = b S("evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ f >= 1 ]", 0-1) = ? S("evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ f >= 1 ]", 0-2) = d S("evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ f >= 1 ]", 0-3) = ? S("evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ f >= 1 ]", 0-4) = ? S("evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ 0 >= f + 1 ]", 0-0) = b S("evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ 0 >= f + 1 ]", 0-1) = ? S("evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ 0 >= f + 1 ]", 0-2) = d S("evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ 0 >= f + 1 ]", 0-3) = ? S("evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ 0 >= f + 1 ]", 0-4) = ? S("evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ]", 0-0) = b S("evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ]", 0-1) = ? S("evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ]", 0-2) = d S("evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ]", 0-3) = ? S("evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ]", 0-4) = ? S("evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) [ e >= c ]", 0-0) = b S("evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) [ e >= c ]", 0-1) = ? S("evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) [ e >= c ]", 0-2) = d S("evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) [ e >= c ]", 0-3) = ? S("evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) [ e >= c ]", 0-4) = ? S("evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ]", 0-0) = b S("evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ]", 0-1) = ? S("evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ]", 0-2) = d S("evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ]", 0-3) = ? S("evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ]", 0-4) = ? S("evalNestedMultipleentryin(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e)", 0-0) = b S("evalNestedMultipleentryin(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e)", 0-1) = a S("evalNestedMultipleentryin(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e)", 0-2) = d S("evalNestedMultipleentryin(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e)", 0-3) = c S("evalNestedMultipleentryin(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e)", 0-4) = e S("evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultipleentryin(a, b, c, d, e)", 0-0) = a S("evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultipleentryin(a, b, c, d, e)", 0-1) = b S("evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultipleentryin(a, b, c, d, e)", 0-2) = c S("evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultipleentryin(a, b, c, d, e)", 0-3) = d S("evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultipleentryin(a, b, c, d, e)", 0-4) = e orients the transitions evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ f >= 1 ] evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ 0 >= f + 1 ] evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) [ e >= c ] evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] evalNestedMultiplebb1in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) weakly and the transitions evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) [ e >= c ] strictly and produces the following problem: 5: T: (1, 1) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultipleentryin(a, b, c, d, e) (1, 1) evalNestedMultipleentryin(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e) (3*a + 3*b, 1) evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ] (6*a + 6*b, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) [ e >= c ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ 0 >= f + 1 ] (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ f >= 1 ] (6*a + 6*b, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) (?, 1) evalNestedMultiplebb1in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) (6*a + 6*b, 1) evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e) start location: evalNestedMultiplestart leaf cost: 2 By chaining the transition evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultipleentryin(a, b, c, d, e) with all transitions in problem 5, the following new transition is obtained: evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e) We thus obtain the following problem: 6: T: (1, 2) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e) (1, 1) evalNestedMultipleentryin(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e) (3*a + 3*b, 1) evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ] (6*a + 6*b, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) [ e >= c ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ 0 >= f + 1 ] (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ f >= 1 ] (6*a + 6*b, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) (?, 1) evalNestedMultiplebb1in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) (6*a + 6*b, 1) evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e) start location: evalNestedMultiplestart leaf cost: 2 Testing for reachability in the complexity graph removes the following transition from problem 6: evalNestedMultipleentryin(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e) We thus obtain the following problem: 7: T: (?, 1) evalNestedMultiplebb1in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) (6*a + 6*b, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ f >= 1 ] (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ 0 >= f + 1 ] (6*a + 6*b, 1) evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e) (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (6*a + 6*b, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) [ e >= c ] (3*a + 3*b, 1) evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ] (1, 2) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e) start location: evalNestedMultiplestart leaf cost: 2 By chaining the transition evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) with all transitions in problem 7, the following new transition is obtained: evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e) We thus obtain the following problem: 8: T: (6*a + 6*b, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e) (?, 1) evalNestedMultiplebb1in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ f >= 1 ] (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ 0 >= f + 1 ] (6*a + 6*b, 1) evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e) (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (6*a + 6*b, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) [ e >= c ] (3*a + 3*b, 1) evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ] (1, 2) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e) start location: evalNestedMultiplestart leaf cost: 2 By chaining the transition evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e) with all transitions in problem 8, the following new transition is obtained: evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] We thus obtain the following problem: 9: T: (6*a + 6*b, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] (?, 1) evalNestedMultiplebb1in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ f >= 1 ] (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ 0 >= f + 1 ] (6*a + 6*b, 1) evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e) (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (6*a + 6*b, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) [ e >= c ] (3*a + 3*b, 1) evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ] (1, 2) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e) start location: evalNestedMultiplestart leaf cost: 2 By chaining the transition evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ f >= 1 ] with all transitions in problem 9, the following new transition is obtained: evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ f >= 1 ] We thus obtain the following problem: 10: T: (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ f >= 1 ] (6*a + 6*b, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] (?, 1) evalNestedMultiplebb1in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) (?, 1) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ 0 >= f + 1 ] (6*a + 6*b, 1) evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e) (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (6*a + 6*b, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) [ e >= c ] (3*a + 3*b, 1) evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ] (1, 2) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e) start location: evalNestedMultiplestart leaf cost: 2 By chaining the transition evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb1in(a, b, c, d, e) [ 0 >= f + 1 ] with all transitions in problem 10, the following new transition is obtained: evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ 0 >= f + 1 ] We thus obtain the following problem: 11: T: (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ 0 >= f + 1 ] (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ f >= 1 ] (6*a + 6*b, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] (?, 1) evalNestedMultiplebb1in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) (6*a + 6*b, 1) evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e) (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (6*a + 6*b, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) [ e >= c ] (3*a + 3*b, 1) evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ] (1, 2) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e) start location: evalNestedMultiplestart leaf cost: 2 Testing for reachability in the complexity graph removes the following transition from problem 11: evalNestedMultiplebb1in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) We thus obtain the following problem: 12: T: (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ 0 >= f + 1 ] (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ f >= 1 ] (6*a + 6*b, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] (6*a + 6*b, 1) evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e) (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (6*a + 6*b, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) [ e >= c ] (3*a + 3*b, 1) evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ] (1, 2) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e) start location: evalNestedMultiplestart leaf cost: 2 By chaining the transition evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb5in(a, b + 1, c, e, e) with all transitions in problem 12, the following new transition is obtained: evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] We thus obtain the following problem: 13: T: (6*a + 6*b, 2) evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ 0 >= f + 1 ] (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ f >= 1 ] (6*a + 6*b, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (6*a + 6*b, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) [ e >= c ] (3*a + 3*b, 1) evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ] (1, 2) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e) start location: evalNestedMultiplestart leaf cost: 2 By chaining the transition evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb4in(a, b, c, d, e) [ e >= c ] with all transitions in problem 13, the following new transition is obtained: evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ e >= c /\ a >= b + 2 ] We thus obtain the following problem: 14: T: (6*a + 6*b, 3) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ e >= c /\ a >= b + 2 ] (6*a + 6*b, 2) evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ 0 >= f + 1 ] (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ f >= 1 ] (6*a + 6*b, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (3*a + 3*b, 1) evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ] (1, 2) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e) start location: evalNestedMultiplestart leaf cost: 2 Testing for reachability in the complexity graph removes the following transition from problem 14: evalNestedMultiplebb4in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] We thus obtain the following problem: 15: T: (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ 0 >= f + 1 ] (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ f >= 1 ] (6*a + 6*b, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] (6*a + 6*b, 3) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ e >= c /\ a >= b + 2 ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (3*a + 3*b, 1) evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ] (1, 2) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e) start location: evalNestedMultiplestart leaf cost: 2 By chaining the transition evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb5in(b, a, d, c, e) with all transitions in problem 15, the following new transition is obtained: evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb2in(b, a, d, c, c) [ b >= a + 1 ] We thus obtain the following problem: 16: T: (1, 3) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb2in(b, a, d, c, c) [ b >= a + 1 ] (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ 0 >= f + 1 ] (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ f >= 1 ] (6*a + 6*b, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] (6*a + 6*b, 3) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ e >= c /\ a >= b + 2 ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (3*a + 3*b, 1) evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ] start location: evalNestedMultiplestart leaf cost: 2 Testing for reachability in the complexity graph removes the following transition from problem 16: evalNestedMultiplebb5in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, d) [ a >= b + 1 ] We thus obtain the following problem: 17: T: (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ 0 >= f + 1 ] (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ f >= 1 ] (6*a + 6*b, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] (6*a + 6*b, 3) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ e >= c /\ a >= b + 2 ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (1, 3) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb2in(b, a, d, c, c) [ b >= a + 1 ] start location: evalNestedMultiplestart leaf cost: 2 By chaining the transition evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ 0 >= f + 1 ] with all transitions in problem 17, the following new transitions are obtained: evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 ] evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e + 1) [ 0 >= f + 1 /\ c >= e + 2 ] We thus obtain the following problem: 18: T: (?, 5) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 ] (?, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e + 1) [ 0 >= f + 1 /\ c >= e + 2 ] (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ f >= 1 ] (6*a + 6*b, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] (6*a + 6*b, 3) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ e >= c /\ a >= b + 2 ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (1, 3) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb2in(b, a, d, c, c) [ b >= a + 1 ] start location: evalNestedMultiplestart leaf cost: 2 A polynomial rank function with Pol(evalNestedMultiplebb3in) = 2*V_3 - 2*V_5 - 1 Pol(evalNestedMultiplebb2in) = 2*V_3 - 2*V_5 - 1 Pol(evalNestedMultiplestart) = -2*V_3 + 2*V_4 - 1 orients all transitions weakly and the transition evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e + 1) [ 0 >= f + 1 /\ c >= e + 2 ] strictly and produces the following problem: 19: T: (?, 5) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 ] (2*c + 2*d + 1, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e + 1) [ 0 >= f + 1 /\ c >= e + 2 ] (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ f >= 1 ] (6*a + 6*b, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] (6*a + 6*b, 3) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ e >= c /\ a >= b + 2 ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (1, 3) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb2in(b, a, d, c, c) [ b >= a + 1 ] start location: evalNestedMultiplestart leaf cost: 2 A polynomial rank function with Pol(evalNestedMultiplebb3in) = V_1 - V_2 - 1 Pol(evalNestedMultiplebb2in) = V_1 - V_2 - 1 Pol(evalNestedMultiplestart) = -V_1 + V_2 - 1 orients all transitions weakly and the transition evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 ] strictly and produces the following problem: 20: T: (a + b + 1, 5) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 ] (2*c + 2*d + 1, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e + 1) [ 0 >= f + 1 /\ c >= e + 2 ] (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ f >= 1 ] (6*a + 6*b, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] (6*a + 6*b, 3) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ e >= c /\ a >= b + 2 ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (1, 3) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb2in(b, a, d, c, c) [ b >= a + 1 ] start location: evalNestedMultiplestart leaf cost: 2 By chaining the transition evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 ] with all transitions in problem 20, the following new transition is obtained: evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 2, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 /\ a >= b + 3 ] We thus obtain the following problem: 21: T: (a + b + 1, 8) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 2, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 /\ a >= b + 3 ] (2*c + 2*d + 1, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e + 1) [ 0 >= f + 1 /\ c >= e + 2 ] (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ f >= 1 ] (6*a + 6*b, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] (6*a + 6*b, 3) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ e >= c /\ a >= b + 2 ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (1, 3) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb2in(b, a, d, c, c) [ b >= a + 1 ] start location: evalNestedMultiplestart leaf cost: 2 By chaining the transition evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 2, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 /\ a >= b + 3 ] with all transitions in problem 21, the following new transition is obtained: evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 3, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 /\ a >= b + 3 /\ a >= b + 4 ] We thus obtain the following problem: 22: T: (a + b + 1, 11) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 3, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 /\ a >= b + 3 /\ a >= b + 4 ] (2*c + 2*d + 1, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e + 1) [ 0 >= f + 1 /\ c >= e + 2 ] (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ f >= 1 ] (6*a + 6*b, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] (6*a + 6*b, 3) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ e >= c /\ a >= b + 2 ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (1, 3) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb2in(b, a, d, c, c) [ b >= a + 1 ] start location: evalNestedMultiplestart leaf cost: 2 By chaining the transition evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 3, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 /\ a >= b + 3 /\ a >= b + 4 ] with all transitions in problem 22, the following new transition is obtained: evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 4, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 /\ a >= b + 3 /\ a >= b + 4 /\ a >= b + 5 ] We thus obtain the following problem: 23: T: (a + b + 1, 14) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 4, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 /\ a >= b + 3 /\ a >= b + 4 /\ a >= b + 5 ] (2*c + 2*d + 1, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e + 1) [ 0 >= f + 1 /\ c >= e + 2 ] (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ f >= 1 ] (6*a + 6*b, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] (6*a + 6*b, 3) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ e >= c /\ a >= b + 2 ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (1, 3) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb2in(b, a, d, c, c) [ b >= a + 1 ] start location: evalNestedMultiplestart leaf cost: 2 By chaining the transition evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 4, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 /\ a >= b + 3 /\ a >= b + 4 /\ a >= b + 5 ] with all transitions in problem 23, the following new transition is obtained: evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 5, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 /\ a >= b + 3 /\ a >= b + 4 /\ a >= b + 5 /\ a >= b + 6 ] We thus obtain the following problem: 24: T: (a + b + 1, 17) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 5, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 /\ a >= b + 3 /\ a >= b + 4 /\ a >= b + 5 /\ a >= b + 6 ] (2*c + 2*d + 1, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e + 1) [ 0 >= f + 1 /\ c >= e + 2 ] (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ f >= 1 ] (6*a + 6*b, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] (6*a + 6*b, 3) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ e >= c /\ a >= b + 2 ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (1, 3) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb2in(b, a, d, c, c) [ b >= a + 1 ] start location: evalNestedMultiplestart leaf cost: 2 By chaining the transition evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 5, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 /\ a >= b + 3 /\ a >= b + 4 /\ a >= b + 5 /\ a >= b + 6 ] with all transitions in problem 24, the following new transition is obtained: evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 6, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 /\ a >= b + 3 /\ a >= b + 4 /\ a >= b + 5 /\ a >= b + 6 /\ a >= b + 7 ] We thus obtain the following problem: 25: T: (a + b + 1, 20) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 6, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 /\ a >= b + 3 /\ a >= b + 4 /\ a >= b + 5 /\ a >= b + 6 /\ a >= b + 7 ] (2*c + 2*d + 1, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e + 1) [ 0 >= f + 1 /\ c >= e + 2 ] (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ f >= 1 ] (6*a + 6*b, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] (6*a + 6*b, 3) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ e >= c /\ a >= b + 2 ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (1, 3) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb2in(b, a, d, c, c) [ b >= a + 1 ] start location: evalNestedMultiplestart leaf cost: 2 By chaining the transition evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 6, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 /\ a >= b + 3 /\ a >= b + 4 /\ a >= b + 5 /\ a >= b + 6 /\ a >= b + 7 ] with all transitions in problem 25, the following new transition is obtained: evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 7, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 /\ a >= b + 3 /\ a >= b + 4 /\ a >= b + 5 /\ a >= b + 6 /\ a >= b + 7 /\ a >= b + 8 ] We thus obtain the following problem: 26: T: (a + b + 1, 23) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 7, c, e + 1, e + 1) [ 0 >= f + 1 /\ e + 1 >= c /\ a >= b + 2 /\ a >= b + 3 /\ a >= b + 4 /\ a >= b + 5 /\ a >= b + 6 /\ a >= b + 7 /\ a >= b + 8 ] (2*c + 2*d + 1, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e + 1) [ 0 >= f + 1 /\ c >= e + 2 ] (?, 2) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b, c, d, e + 1) [ f >= 1 ] (6*a + 6*b, 3) evalNestedMultiplebb3in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ a >= b + 2 ] (6*a + 6*b, 3) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb2in(a, b + 1, c, e, e) [ e >= c /\ a >= b + 2 ] (?, 1) evalNestedMultiplebb2in(a, b, c, d, e) -> evalNestedMultiplebb3in(a, b, c, d, e) [ c >= e + 1 ] (1, 3) evalNestedMultiplestart(a, b, c, d, e) -> evalNestedMultiplebb2in(b, a, d, c, c) [ b >= a + 1 ] start location: evalNestedMultiplestart leaf cost: 2 Complexity upper bound ? Time: 3.550 sec (SMT: 3.299 sec)