YES(?, 2*a + 2*b + 3) Initial complexity problem: 1: T: (?, 1) merge(a, b) -> merge(a - 1, b) [ a >= 1 /\ b >= 1 ] (?, 1) merge(a, b) -> merge(a, b - 1) [ a >= 1 /\ b >= 1 ] (1, 1) start(a, b) -> merge(a, b) start location: start leaf cost: 0 A polynomial rank function with Pol(merge) = V_1 + V_2 - 1 Pol(start) = V_1 + V_2 - 1 orients all transitions weakly and the transitions merge(a, b) -> merge(a, b - 1) [ a >= 1 /\ b >= 1 ] merge(a, b) -> merge(a - 1, b) [ a >= 1 /\ b >= 1 ] strictly and produces the following problem: 2: T: (a + b + 1, 1) merge(a, b) -> merge(a - 1, b) [ a >= 1 /\ b >= 1 ] (a + b + 1, 1) merge(a, b) -> merge(a, b - 1) [ a >= 1 /\ b >= 1 ] (1, 1) start(a, b) -> merge(a, b) start location: start leaf cost: 0 Complexity upper bound 2*a + 2*b + 3 Time: 0.127 sec (SMT: 0.122 sec)