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