YES(?, b + 2) Initial complexity problem: 1: T: (1, 1) l0(a, b) -> l1(0, b) (?, 1) l1(a, b) -> l1(a + 1, b - 1) [ b >= 1 ] (?, 1) l1(a, b) -> l2(a, b) [ 0 >= b ] start location: l0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem: 2: T: (1, 1) l0(a, b) -> l1(0, b) (?, 1) l1(a, b) -> l1(a + 1, b - 1) [ b >= 1 ] start location: l0 leaf cost: 1 A polynomial rank function with Pol(l0) = V_2 Pol(l1) = V_2 orients all transitions weakly and the transition l1(a, b) -> l1(a + 1, b - 1) [ b >= 1 ] strictly and produces the following problem: 3: T: (1, 1) l0(a, b) -> l1(0, b) (b, 1) l1(a, b) -> l1(a + 1, b - 1) [ b >= 1 ] start location: l0 leaf cost: 1 Complexity upper bound b + 2 Time: 0.084 sec (SMT: 0.081 sec)