YES(?, 301) Initial complexity problem: 1: T: (1, 1) f0(a) -> f1(300) (?, 1) f1(a) -> f1(a - 1) [ a >= 102 ] (?, 1) f1(a) -> f1(a - 1) [ 100 >= a ] start location: f0 leaf cost: 0 Testing for reachability in the complexity graph removes the following transition from problem 1: f1(a) -> f1(a - 1) [ 100 >= a ] We thus obtain the following problem: 2: T: (?, 1) f1(a) -> f1(a - 1) [ a >= 102 ] (1, 1) f0(a) -> f1(300) start location: f0 leaf cost: 0 A polynomial rank function with Pol(f1) = V_1 Pol(f0) = 300 orients all transitions weakly and the transition f1(a) -> f1(a - 1) [ a >= 102 ] strictly and produces the following problem: 3: T: (300, 1) f1(a) -> f1(a - 1) [ a >= 102 ] (1, 1) f0(a) -> f1(300) start location: f0 leaf cost: 0 Complexity upper bound 301 Time: 0.076 sec (SMT: 0.073 sec)