YES(?, a + 1) Initial complexity problem: 1: T: (1, 1) f0(a) -> f1(a) (?, 1) f1(a) -> f1(a - 1) [ a >= 202 ] start location: f0 leaf cost: 0 A polynomial rank function with Pol(f0) = V_1 Pol(f1) = V_1 orients all transitions weakly and the transition f1(a) -> f1(a - 1) [ a >= 202 ] strictly and produces the following problem: 2: T: (1, 1) f0(a) -> f1(a) (a, 1) f1(a) -> f1(a - 1) [ a >= 202 ] start location: f0 leaf cost: 0 Complexity upper bound a + 1 Time: 0.065 sec (SMT: 0.062 sec)