YES(?, a + 4) Initial complexity problem: 1: T: (?, 1) start(a, b, c, d) -> stop(a, b, c, d) [ 1 >= a /\ b = c /\ d = a ] (?, 1) start(a, b, c, d) -> lbl32(a, b, c, d - 1) [ a >= 2 /\ b = c /\ d = a ] (?, 1) lbl32(a, b, c, d) -> stop(a, b, c, d) [ a >= 2 /\ d = 1 /\ b = c ] (?, 1) lbl32(a, b, c, d) -> lbl32(a, b, c, d - 1) [ d >= 2 /\ d >= 1 /\ a >= d + 1 /\ b = c ] (1, 1) start0(a, b, c, d) -> start(a, c, c, a) start location: start0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem: 2: T: (?, 1) start(a, b, c, d) -> lbl32(a, b, c, d - 1) [ a >= 2 /\ b = c /\ d = a ] (?, 1) lbl32(a, b, c, d) -> lbl32(a, b, c, d - 1) [ d >= 2 /\ d >= 1 /\ a >= d + 1 /\ b = c ] (1, 1) start0(a, b, c, d) -> start(a, c, c, a) start location: start0 leaf cost: 2 Repeatedly propagating knowledge in problem 2 produces the following problem: 3: T: (1, 1) start(a, b, c, d) -> lbl32(a, b, c, d - 1) [ a >= 2 /\ b = c /\ d = a ] (?, 1) lbl32(a, b, c, d) -> lbl32(a, b, c, d - 1) [ d >= 2 /\ d >= 1 /\ a >= d + 1 /\ b = c ] (1, 1) start0(a, b, c, d) -> start(a, c, c, a) start location: start0 leaf cost: 2 A polynomial rank function with Pol(start) = V_4 Pol(lbl32) = V_4 Pol(start0) = V_1 orients all transitions weakly and the transition lbl32(a, b, c, d) -> lbl32(a, b, c, d - 1) [ d >= 2 /\ d >= 1 /\ a >= d + 1 /\ b = c ] strictly and produces the following problem: 4: T: (1, 1) start(a, b, c, d) -> lbl32(a, b, c, d - 1) [ a >= 2 /\ b = c /\ d = a ] (a, 1) lbl32(a, b, c, d) -> lbl32(a, b, c, d - 1) [ d >= 2 /\ d >= 1 /\ a >= d + 1 /\ b = c ] (1, 1) start0(a, b, c, d) -> start(a, c, c, a) start location: start0 leaf cost: 2 Complexity upper bound a + 4 Time: 0.156 sec (SMT: 0.148 sec)