MAYBE Initial complexity problem: 1: T: (?, 1) f1(a, b) -> f2(a - 1, b) [ a >= 1 ] (?, 1) f2(a, b) -> f2(a - 1, b + 1) [ a >= 1 ] (1, 1) f999(a, b) -> f1(1, b - 1) [ b >= 1 /\ a = 0 ] (?, 1) f1(a, b) -> f1(a + 1, b - 1) [ b >= 1 ] (?, 1) f2(a, b) -> f1(a + 1, b - 1) [ b >= 1 ] start location: f999 leaf cost: 0 Applied AI with 'oct' on problem 1 to obtain the following invariants: For symbol f1: X_2 >= 0 /\ X_1 + X_2 - 1 >= 0 /\ X_1 - 1 >= 0 For symbol f2: X_2 >= 0 /\ X_1 + X_2 >= 0 /\ X_1 >= 0 This yielded the following problem: 2: T: (?, 1) f2(a, b) -> f1(a + 1, b - 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 ] (?, 1) f1(a, b) -> f1(a + 1, b - 1) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= 1 ] (1, 1) f999(a, b) -> f1(1, b - 1) [ b >= 1 /\ a = 0 ] (?, 1) f2(a, b) -> f2(a - 1, b + 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= 1 ] (?, 1) f1(a, b) -> f2(a - 1, b) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ a >= 1 ] start location: f999 leaf cost: 0 A polynomial rank function with Pol(f2) = 2*V_1 + 2*V_2 + 1 Pol(f1) = 2*V_1 + 2*V_2 Pol(f999) = 2*V_2 orients all transitions weakly and the transitions f2(a, b) -> f1(a + 1, b - 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 ] f1(a, b) -> f2(a - 1, b) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ a >= 1 ] strictly and produces the following problem: 3: T: (2*b, 1) f2(a, b) -> f1(a + 1, b - 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 ] (?, 1) f1(a, b) -> f1(a + 1, b - 1) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= 1 ] (1, 1) f999(a, b) -> f1(1, b - 1) [ b >= 1 /\ a = 0 ] (?, 1) f2(a, b) -> f2(a - 1, b + 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= 1 ] (2*b, 1) f1(a, b) -> f2(a - 1, b) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ a >= 1 ] start location: f999 leaf cost: 0 By chaining the transition f2(a, b) -> f1(a + 1, b - 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 ] with all transitions in problem 3, the following new transitions are obtained: f2(a, b) -> f2(a, b - 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ a + 1 >= 1 ] f2(a, b) -> f1(a + 2, b - 2) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 ] We thus obtain the following problem: 4: T: (2*b, 2) f2(a, b) -> f2(a, b - 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ a + 1 >= 1 ] (2*b, 2) f2(a, b) -> f1(a + 2, b - 2) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 ] (?, 1) f1(a, b) -> f1(a + 1, b - 1) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= 1 ] (1, 1) f999(a, b) -> f1(1, b - 1) [ b >= 1 /\ a = 0 ] (?, 1) f2(a, b) -> f2(a - 1, b + 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= 1 ] (2*b, 1) f1(a, b) -> f2(a - 1, b) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ a >= 1 ] start location: f999 leaf cost: 0 By chaining the transition f2(a, b) -> f1(a + 2, b - 2) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 ] with all transitions in problem 4, the following new transitions are obtained: f2(a, b) -> f2(a + 1, b - 2) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ a + 2 >= 1 ] f2(a, b) -> f1(a + 3, b - 3) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 ] We thus obtain the following problem: 5: T: (2*b, 3) f2(a, b) -> f2(a + 1, b - 2) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ a + 2 >= 1 ] (2*b, 3) f2(a, b) -> f1(a + 3, b - 3) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 ] (2*b, 2) f2(a, b) -> f2(a, b - 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ a + 1 >= 1 ] (?, 1) f1(a, b) -> f1(a + 1, b - 1) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= 1 ] (1, 1) f999(a, b) -> f1(1, b - 1) [ b >= 1 /\ a = 0 ] (?, 1) f2(a, b) -> f2(a - 1, b + 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= 1 ] (2*b, 1) f1(a, b) -> f2(a - 1, b) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ a >= 1 ] start location: f999 leaf cost: 0 By chaining the transition f2(a, b) -> f1(a + 3, b - 3) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 ] with all transitions in problem 5, the following new transitions are obtained: f2(a, b) -> f2(a + 2, b - 3) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ a + 3 >= 1 ] f2(a, b) -> f1(a + 4, b - 4) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 ] We thus obtain the following problem: 6: T: (2*b, 4) f2(a, b) -> f2(a + 2, b - 3) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ a + 3 >= 1 ] (2*b, 4) f2(a, b) -> f1(a + 4, b - 4) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 ] (2*b, 3) f2(a, b) -> f2(a + 1, b - 2) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ a + 2 >= 1 ] (2*b, 2) f2(a, b) -> f2(a, b - 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ a + 1 >= 1 ] (?, 1) f1(a, b) -> f1(a + 1, b - 1) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= 1 ] (1, 1) f999(a, b) -> f1(1, b - 1) [ b >= 1 /\ a = 0 ] (?, 1) f2(a, b) -> f2(a - 1, b + 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= 1 ] (2*b, 1) f1(a, b) -> f2(a - 1, b) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ a >= 1 ] start location: f999 leaf cost: 0 By chaining the transition f2(a, b) -> f1(a + 4, b - 4) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 ] with all transitions in problem 6, the following new transitions are obtained: f2(a, b) -> f2(a + 3, b - 4) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ a + 4 >= 1 ] f2(a, b) -> f1(a + 5, b - 5) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 ] We thus obtain the following problem: 7: T: (2*b, 5) f2(a, b) -> f2(a + 3, b - 4) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ a + 4 >= 1 ] (2*b, 5) f2(a, b) -> f1(a + 5, b - 5) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 ] (2*b, 4) f2(a, b) -> f2(a + 2, b - 3) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ a + 3 >= 1 ] (2*b, 3) f2(a, b) -> f2(a + 1, b - 2) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ a + 2 >= 1 ] (2*b, 2) f2(a, b) -> f2(a, b - 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ a + 1 >= 1 ] (?, 1) f1(a, b) -> f1(a + 1, b - 1) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= 1 ] (1, 1) f999(a, b) -> f1(1, b - 1) [ b >= 1 /\ a = 0 ] (?, 1) f2(a, b) -> f2(a - 1, b + 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= 1 ] (2*b, 1) f1(a, b) -> f2(a - 1, b) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ a >= 1 ] start location: f999 leaf cost: 0 By chaining the transition f2(a, b) -> f1(a + 5, b - 5) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 ] with all transitions in problem 7, the following new transitions are obtained: f2(a, b) -> f2(a + 4, b - 5) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ a + 5 >= 1 ] f2(a, b) -> f1(a + 6, b - 6) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 ] We thus obtain the following problem: 8: T: (2*b, 6) f2(a, b) -> f2(a + 4, b - 5) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ a + 5 >= 1 ] (2*b, 6) f2(a, b) -> f1(a + 6, b - 6) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 ] (2*b, 5) f2(a, b) -> f2(a + 3, b - 4) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ a + 4 >= 1 ] (2*b, 4) f2(a, b) -> f2(a + 2, b - 3) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ a + 3 >= 1 ] (2*b, 3) f2(a, b) -> f2(a + 1, b - 2) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ a + 2 >= 1 ] (2*b, 2) f2(a, b) -> f2(a, b - 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ a + 1 >= 1 ] (?, 1) f1(a, b) -> f1(a + 1, b - 1) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= 1 ] (1, 1) f999(a, b) -> f1(1, b - 1) [ b >= 1 /\ a = 0 ] (?, 1) f2(a, b) -> f2(a - 1, b + 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= 1 ] (2*b, 1) f1(a, b) -> f2(a - 1, b) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ a >= 1 ] start location: f999 leaf cost: 0 By chaining the transition f2(a, b) -> f1(a + 6, b - 6) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 ] with all transitions in problem 8, the following new transitions are obtained: f2(a, b) -> f2(a + 5, b - 6) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ a + 6 >= 1 ] f2(a, b) -> f1(a + 7, b - 7) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 ] We thus obtain the following problem: 9: T: (2*b, 7) f2(a, b) -> f2(a + 5, b - 6) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ a + 6 >= 1 ] (2*b, 7) f2(a, b) -> f1(a + 7, b - 7) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 ] (2*b, 6) f2(a, b) -> f2(a + 4, b - 5) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ a + 5 >= 1 ] (2*b, 5) f2(a, b) -> f2(a + 3, b - 4) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ a + 4 >= 1 ] (2*b, 4) f2(a, b) -> f2(a + 2, b - 3) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ a + 3 >= 1 ] (2*b, 3) f2(a, b) -> f2(a + 1, b - 2) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ a + 2 >= 1 ] (2*b, 2) f2(a, b) -> f2(a, b - 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ a + 1 >= 1 ] (?, 1) f1(a, b) -> f1(a + 1, b - 1) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= 1 ] (1, 1) f999(a, b) -> f1(1, b - 1) [ b >= 1 /\ a = 0 ] (?, 1) f2(a, b) -> f2(a - 1, b + 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= 1 ] (2*b, 1) f1(a, b) -> f2(a - 1, b) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ a >= 1 ] start location: f999 leaf cost: 0 By chaining the transition f2(a, b) -> f1(a + 7, b - 7) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 ] with all transitions in problem 9, the following new transitions are obtained: f2(a, b) -> f2(a + 6, b - 7) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ a + 7 >= 1 ] f2(a, b) -> f1(a + 8, b - 8) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 ] We thus obtain the following problem: 10: T: (2*b, 8) f2(a, b) -> f2(a + 6, b - 7) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ a + 7 >= 1 ] (2*b, 8) f2(a, b) -> f1(a + 8, b - 8) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 ] (2*b, 7) f2(a, b) -> f2(a + 5, b - 6) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ a + 6 >= 1 ] (2*b, 6) f2(a, b) -> f2(a + 4, b - 5) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ a + 5 >= 1 ] (2*b, 5) f2(a, b) -> f2(a + 3, b - 4) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ a + 4 >= 1 ] (2*b, 4) f2(a, b) -> f2(a + 2, b - 3) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ a + 3 >= 1 ] (2*b, 3) f2(a, b) -> f2(a + 1, b - 2) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ a + 2 >= 1 ] (2*b, 2) f2(a, b) -> f2(a, b - 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ a + 1 >= 1 ] (?, 1) f1(a, b) -> f1(a + 1, b - 1) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= 1 ] (1, 1) f999(a, b) -> f1(1, b - 1) [ b >= 1 /\ a = 0 ] (?, 1) f2(a, b) -> f2(a - 1, b + 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= 1 ] (2*b, 1) f1(a, b) -> f2(a - 1, b) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ a >= 1 ] start location: f999 leaf cost: 0 By chaining the transition f2(a, b) -> f1(a + 8, b - 8) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 ] with all transitions in problem 10, the following new transitions are obtained: f2(a, b) -> f2(a + 7, b - 8) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ a + 8 >= 1 ] f2(a, b) -> f1(a + 9, b - 9) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 ] We thus obtain the following problem: 11: T: (2*b, 9) f2(a, b) -> f2(a + 7, b - 8) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ a + 8 >= 1 ] (2*b, 9) f2(a, b) -> f1(a + 9, b - 9) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 ] (2*b, 8) f2(a, b) -> f2(a + 6, b - 7) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ a + 7 >= 1 ] (2*b, 7) f2(a, b) -> f2(a + 5, b - 6) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ a + 6 >= 1 ] (2*b, 6) f2(a, b) -> f2(a + 4, b - 5) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ a + 5 >= 1 ] (2*b, 5) f2(a, b) -> f2(a + 3, b - 4) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ a + 4 >= 1 ] (2*b, 4) f2(a, b) -> f2(a + 2, b - 3) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ a + 3 >= 1 ] (2*b, 3) f2(a, b) -> f2(a + 1, b - 2) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ a + 2 >= 1 ] (2*b, 2) f2(a, b) -> f2(a, b - 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ a + 1 >= 1 ] (?, 1) f1(a, b) -> f1(a + 1, b - 1) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= 1 ] (1, 1) f999(a, b) -> f1(1, b - 1) [ b >= 1 /\ a = 0 ] (?, 1) f2(a, b) -> f2(a - 1, b + 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= 1 ] (2*b, 1) f1(a, b) -> f2(a - 1, b) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ a >= 1 ] start location: f999 leaf cost: 0 By chaining the transition f2(a, b) -> f1(a + 9, b - 9) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 ] with all transitions in problem 11, the following new transitions are obtained: f2(a, b) -> f2(a + 8, b - 9) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ a + 9 >= 1 ] f2(a, b) -> f1(a + 10, b - 10) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 ] We thus obtain the following problem: 12: T: (2*b, 10) f2(a, b) -> f2(a + 8, b - 9) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ a + 9 >= 1 ] (2*b, 10) f2(a, b) -> f1(a + 10, b - 10) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 ] (2*b, 9) f2(a, b) -> f2(a + 7, b - 8) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ a + 8 >= 1 ] (2*b, 8) f2(a, b) -> f2(a + 6, b - 7) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ a + 7 >= 1 ] (2*b, 7) f2(a, b) -> f2(a + 5, b - 6) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ a + 6 >= 1 ] (2*b, 6) f2(a, b) -> f2(a + 4, b - 5) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ a + 5 >= 1 ] (2*b, 5) f2(a, b) -> f2(a + 3, b - 4) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ a + 4 >= 1 ] (2*b, 4) f2(a, b) -> f2(a + 2, b - 3) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ a + 3 >= 1 ] (2*b, 3) f2(a, b) -> f2(a + 1, b - 2) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ a + 2 >= 1 ] (2*b, 2) f2(a, b) -> f2(a, b - 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ a + 1 >= 1 ] (?, 1) f1(a, b) -> f1(a + 1, b - 1) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= 1 ] (1, 1) f999(a, b) -> f1(1, b - 1) [ b >= 1 /\ a = 0 ] (?, 1) f2(a, b) -> f2(a - 1, b + 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= 1 ] (2*b, 1) f1(a, b) -> f2(a - 1, b) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ a >= 1 ] start location: f999 leaf cost: 0 By chaining the transition f2(a, b) -> f1(a + 10, b - 10) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 ] with all transitions in problem 12, the following new transitions are obtained: f2(a, b) -> f2(a + 9, b - 10) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ a + 10 >= 1 ] f2(a, b) -> f1(a + 11, b - 11) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 ] We thus obtain the following problem: 13: T: (2*b, 11) f2(a, b) -> f2(a + 9, b - 10) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ a + 10 >= 1 ] (2*b, 11) f2(a, b) -> f1(a + 11, b - 11) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 ] (2*b, 10) f2(a, b) -> f2(a + 8, b - 9) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ a + 9 >= 1 ] (2*b, 9) f2(a, b) -> f2(a + 7, b - 8) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ a + 8 >= 1 ] (2*b, 8) f2(a, b) -> f2(a + 6, b - 7) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ a + 7 >= 1 ] (2*b, 7) f2(a, b) -> f2(a + 5, b - 6) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ a + 6 >= 1 ] (2*b, 6) f2(a, b) -> f2(a + 4, b - 5) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ a + 5 >= 1 ] (2*b, 5) f2(a, b) -> f2(a + 3, b - 4) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ a + 4 >= 1 ] (2*b, 4) f2(a, b) -> f2(a + 2, b - 3) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ a + 3 >= 1 ] (2*b, 3) f2(a, b) -> f2(a + 1, b - 2) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ a + 2 >= 1 ] (2*b, 2) f2(a, b) -> f2(a, b - 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ a + 1 >= 1 ] (?, 1) f1(a, b) -> f1(a + 1, b - 1) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= 1 ] (1, 1) f999(a, b) -> f1(1, b - 1) [ b >= 1 /\ a = 0 ] (?, 1) f2(a, b) -> f2(a - 1, b + 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= 1 ] (2*b, 1) f1(a, b) -> f2(a - 1, b) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ a >= 1 ] start location: f999 leaf cost: 0 By chaining the transition f2(a, b) -> f1(a + 11, b - 11) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 ] with all transitions in problem 13, the following new transitions are obtained: f2(a, b) -> f2(a + 10, b - 11) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ a + 11 >= 1 ] f2(a, b) -> f1(a + 12, b - 12) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 ] We thus obtain the following problem: 14: T: (2*b, 12) f2(a, b) -> f2(a + 10, b - 11) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ a + 11 >= 1 ] (2*b, 12) f2(a, b) -> f1(a + 12, b - 12) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 ] (2*b, 11) f2(a, b) -> f2(a + 9, b - 10) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ a + 10 >= 1 ] (2*b, 10) f2(a, b) -> f2(a + 8, b - 9) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ a + 9 >= 1 ] (2*b, 9) f2(a, b) -> f2(a + 7, b - 8) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ a + 8 >= 1 ] (2*b, 8) f2(a, b) -> f2(a + 6, b - 7) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ a + 7 >= 1 ] (2*b, 7) f2(a, b) -> f2(a + 5, b - 6) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ a + 6 >= 1 ] (2*b, 6) f2(a, b) -> f2(a + 4, b - 5) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ a + 5 >= 1 ] (2*b, 5) f2(a, b) -> f2(a + 3, b - 4) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ a + 4 >= 1 ] (2*b, 4) f2(a, b) -> f2(a + 2, b - 3) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ a + 3 >= 1 ] (2*b, 3) f2(a, b) -> f2(a + 1, b - 2) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ a + 2 >= 1 ] (2*b, 2) f2(a, b) -> f2(a, b - 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ a + 1 >= 1 ] (?, 1) f1(a, b) -> f1(a + 1, b - 1) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= 1 ] (1, 1) f999(a, b) -> f1(1, b - 1) [ b >= 1 /\ a = 0 ] (?, 1) f2(a, b) -> f2(a - 1, b + 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= 1 ] (2*b, 1) f1(a, b) -> f2(a - 1, b) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ a >= 1 ] start location: f999 leaf cost: 0 By chaining the transition f2(a, b) -> f1(a + 12, b - 12) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 ] with all transitions in problem 14, the following new transitions are obtained: f2(a, b) -> f2(a + 11, b - 12) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ a + 12 >= 1 ] f2(a, b) -> f1(a + 13, b - 13) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ b - 12 >= 1 ] We thus obtain the following problem: 15: T: (2*b, 13) f2(a, b) -> f2(a + 11, b - 12) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ a + 12 >= 1 ] (2*b, 13) f2(a, b) -> f1(a + 13, b - 13) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ b - 12 >= 1 ] (2*b, 12) f2(a, b) -> f2(a + 10, b - 11) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ a + 11 >= 1 ] (2*b, 11) f2(a, b) -> f2(a + 9, b - 10) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ a + 10 >= 1 ] (2*b, 10) f2(a, b) -> f2(a + 8, b - 9) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ a + 9 >= 1 ] (2*b, 9) f2(a, b) -> f2(a + 7, b - 8) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ a + 8 >= 1 ] (2*b, 8) f2(a, b) -> f2(a + 6, b - 7) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ a + 7 >= 1 ] (2*b, 7) f2(a, b) -> f2(a + 5, b - 6) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ a + 6 >= 1 ] (2*b, 6) f2(a, b) -> f2(a + 4, b - 5) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ a + 5 >= 1 ] (2*b, 5) f2(a, b) -> f2(a + 3, b - 4) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ a + 4 >= 1 ] (2*b, 4) f2(a, b) -> f2(a + 2, b - 3) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ a + 3 >= 1 ] (2*b, 3) f2(a, b) -> f2(a + 1, b - 2) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ a + 2 >= 1 ] (2*b, 2) f2(a, b) -> f2(a, b - 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ a + 1 >= 1 ] (?, 1) f1(a, b) -> f1(a + 1, b - 1) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= 1 ] (1, 1) f999(a, b) -> f1(1, b - 1) [ b >= 1 /\ a = 0 ] (?, 1) f2(a, b) -> f2(a - 1, b + 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= 1 ] (2*b, 1) f1(a, b) -> f2(a - 1, b) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ a >= 1 ] start location: f999 leaf cost: 0 By chaining the transition f2(a, b) -> f1(a + 13, b - 13) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ b - 12 >= 1 ] with all transitions in problem 15, the following new transitions are obtained: f2(a, b) -> f2(a + 12, b - 13) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ b - 12 >= 1 /\ b - 13 >= 0 /\ a + 12 >= 0 /\ a + 13 >= 1 ] f2(a, b) -> f1(a + 14, b - 14) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ b - 12 >= 1 /\ b - 13 >= 0 /\ a + 12 >= 0 /\ b - 13 >= 1 ] We thus obtain the following problem: 16: T: (2*b, 14) f2(a, b) -> f2(a + 12, b - 13) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ b - 12 >= 1 /\ b - 13 >= 0 /\ a + 12 >= 0 /\ a + 13 >= 1 ] (2*b, 14) f2(a, b) -> f1(a + 14, b - 14) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ b - 12 >= 1 /\ b - 13 >= 0 /\ a + 12 >= 0 /\ b - 13 >= 1 ] (2*b, 13) f2(a, b) -> f2(a + 11, b - 12) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ a + 12 >= 1 ] (2*b, 12) f2(a, b) -> f2(a + 10, b - 11) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ a + 11 >= 1 ] (2*b, 11) f2(a, b) -> f2(a + 9, b - 10) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ a + 10 >= 1 ] (2*b, 10) f2(a, b) -> f2(a + 8, b - 9) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ a + 9 >= 1 ] (2*b, 9) f2(a, b) -> f2(a + 7, b - 8) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ a + 8 >= 1 ] (2*b, 8) f2(a, b) -> f2(a + 6, b - 7) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ a + 7 >= 1 ] (2*b, 7) f2(a, b) -> f2(a + 5, b - 6) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ a + 6 >= 1 ] (2*b, 6) f2(a, b) -> f2(a + 4, b - 5) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ a + 5 >= 1 ] (2*b, 5) f2(a, b) -> f2(a + 3, b - 4) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ a + 4 >= 1 ] (2*b, 4) f2(a, b) -> f2(a + 2, b - 3) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ a + 3 >= 1 ] (2*b, 3) f2(a, b) -> f2(a + 1, b - 2) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ a + 2 >= 1 ] (2*b, 2) f2(a, b) -> f2(a, b - 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ a + 1 >= 1 ] (?, 1) f1(a, b) -> f1(a + 1, b - 1) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= 1 ] (1, 1) f999(a, b) -> f1(1, b - 1) [ b >= 1 /\ a = 0 ] (?, 1) f2(a, b) -> f2(a - 1, b + 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= 1 ] (2*b, 1) f1(a, b) -> f2(a - 1, b) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ a >= 1 ] start location: f999 leaf cost: 0 By chaining the transition f2(a, b) -> f1(a + 14, b - 14) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ b - 12 >= 1 /\ b - 13 >= 0 /\ a + 12 >= 0 /\ b - 13 >= 1 ] with all transitions in problem 16, the following new transitions are obtained: f2(a, b) -> f2(a + 13, b - 14) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ b - 12 >= 1 /\ b - 13 >= 0 /\ a + 12 >= 0 /\ b - 13 >= 1 /\ b - 14 >= 0 /\ a + 13 >= 0 /\ a + 14 >= 1 ] f2(a, b) -> f1(a + 15, b - 15) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ b - 12 >= 1 /\ b - 13 >= 0 /\ a + 12 >= 0 /\ b - 13 >= 1 /\ b - 14 >= 0 /\ a + 13 >= 0 /\ b - 14 >= 1 ] We thus obtain the following problem: 17: T: (2*b, 15) f2(a, b) -> f2(a + 13, b - 14) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ b - 12 >= 1 /\ b - 13 >= 0 /\ a + 12 >= 0 /\ b - 13 >= 1 /\ b - 14 >= 0 /\ a + 13 >= 0 /\ a + 14 >= 1 ] (2*b, 15) f2(a, b) -> f1(a + 15, b - 15) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ b - 12 >= 1 /\ b - 13 >= 0 /\ a + 12 >= 0 /\ b - 13 >= 1 /\ b - 14 >= 0 /\ a + 13 >= 0 /\ b - 14 >= 1 ] (2*b, 14) f2(a, b) -> f2(a + 12, b - 13) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ b - 12 >= 1 /\ b - 13 >= 0 /\ a + 12 >= 0 /\ a + 13 >= 1 ] (2*b, 13) f2(a, b) -> f2(a + 11, b - 12) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ a + 12 >= 1 ] (2*b, 12) f2(a, b) -> f2(a + 10, b - 11) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ a + 11 >= 1 ] (2*b, 11) f2(a, b) -> f2(a + 9, b - 10) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ a + 10 >= 1 ] (2*b, 10) f2(a, b) -> f2(a + 8, b - 9) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ a + 9 >= 1 ] (2*b, 9) f2(a, b) -> f2(a + 7, b - 8) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ a + 8 >= 1 ] (2*b, 8) f2(a, b) -> f2(a + 6, b - 7) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ a + 7 >= 1 ] (2*b, 7) f2(a, b) -> f2(a + 5, b - 6) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ a + 6 >= 1 ] (2*b, 6) f2(a, b) -> f2(a + 4, b - 5) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ a + 5 >= 1 ] (2*b, 5) f2(a, b) -> f2(a + 3, b - 4) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ a + 4 >= 1 ] (2*b, 4) f2(a, b) -> f2(a + 2, b - 3) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ a + 3 >= 1 ] (2*b, 3) f2(a, b) -> f2(a + 1, b - 2) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ a + 2 >= 1 ] (2*b, 2) f2(a, b) -> f2(a, b - 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ a + 1 >= 1 ] (?, 1) f1(a, b) -> f1(a + 1, b - 1) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= 1 ] (1, 1) f999(a, b) -> f1(1, b - 1) [ b >= 1 /\ a = 0 ] (?, 1) f2(a, b) -> f2(a - 1, b + 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= 1 ] (2*b, 1) f1(a, b) -> f2(a - 1, b) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ a >= 1 ] start location: f999 leaf cost: 0 By chaining the transition f2(a, b) -> f1(a + 15, b - 15) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ b - 12 >= 1 /\ b - 13 >= 0 /\ a + 12 >= 0 /\ b - 13 >= 1 /\ b - 14 >= 0 /\ a + 13 >= 0 /\ b - 14 >= 1 ] with all transitions in problem 17, the following new transitions are obtained: f2(a, b) -> f2(a + 14, b - 15) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ b - 12 >= 1 /\ b - 13 >= 0 /\ a + 12 >= 0 /\ b - 13 >= 1 /\ b - 14 >= 0 /\ a + 13 >= 0 /\ b - 14 >= 1 /\ b - 15 >= 0 /\ a + 14 >= 0 /\ a + 15 >= 1 ] f2(a, b) -> f1(a + 16, b - 16) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ b - 12 >= 1 /\ b - 13 >= 0 /\ a + 12 >= 0 /\ b - 13 >= 1 /\ b - 14 >= 0 /\ a + 13 >= 0 /\ b - 14 >= 1 /\ b - 15 >= 0 /\ a + 14 >= 0 /\ b - 15 >= 1 ] We thus obtain the following problem: 18: T: (2*b, 16) f2(a, b) -> f2(a + 14, b - 15) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ b - 12 >= 1 /\ b - 13 >= 0 /\ a + 12 >= 0 /\ b - 13 >= 1 /\ b - 14 >= 0 /\ a + 13 >= 0 /\ b - 14 >= 1 /\ b - 15 >= 0 /\ a + 14 >= 0 /\ a + 15 >= 1 ] (2*b, 16) f2(a, b) -> f1(a + 16, b - 16) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ b - 12 >= 1 /\ b - 13 >= 0 /\ a + 12 >= 0 /\ b - 13 >= 1 /\ b - 14 >= 0 /\ a + 13 >= 0 /\ b - 14 >= 1 /\ b - 15 >= 0 /\ a + 14 >= 0 /\ b - 15 >= 1 ] (2*b, 15) f2(a, b) -> f2(a + 13, b - 14) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ b - 12 >= 1 /\ b - 13 >= 0 /\ a + 12 >= 0 /\ b - 13 >= 1 /\ b - 14 >= 0 /\ a + 13 >= 0 /\ a + 14 >= 1 ] (2*b, 14) f2(a, b) -> f2(a + 12, b - 13) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ b - 12 >= 1 /\ b - 13 >= 0 /\ a + 12 >= 0 /\ a + 13 >= 1 ] (2*b, 13) f2(a, b) -> f2(a + 11, b - 12) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ b - 11 >= 1 /\ b - 12 >= 0 /\ a + 11 >= 0 /\ a + 12 >= 1 ] (2*b, 12) f2(a, b) -> f2(a + 10, b - 11) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ b - 10 >= 1 /\ b - 11 >= 0 /\ a + 10 >= 0 /\ a + 11 >= 1 ] (2*b, 11) f2(a, b) -> f2(a + 9, b - 10) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ b - 9 >= 1 /\ b - 10 >= 0 /\ a + 9 >= 0 /\ a + 10 >= 1 ] (2*b, 10) f2(a, b) -> f2(a + 8, b - 9) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ b - 8 >= 1 /\ b - 9 >= 0 /\ a + 8 >= 0 /\ a + 9 >= 1 ] (2*b, 9) f2(a, b) -> f2(a + 7, b - 8) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ b - 7 >= 1 /\ b - 8 >= 0 /\ a + 7 >= 0 /\ a + 8 >= 1 ] (2*b, 8) f2(a, b) -> f2(a + 6, b - 7) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ b - 6 >= 1 /\ b - 7 >= 0 /\ a + 6 >= 0 /\ a + 7 >= 1 ] (2*b, 7) f2(a, b) -> f2(a + 5, b - 6) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ b - 5 >= 1 /\ b - 6 >= 0 /\ a + 5 >= 0 /\ a + 6 >= 1 ] (2*b, 6) f2(a, b) -> f2(a + 4, b - 5) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ b - 4 >= 1 /\ b - 5 >= 0 /\ a + 4 >= 0 /\ a + 5 >= 1 ] (2*b, 5) f2(a, b) -> f2(a + 3, b - 4) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ b - 3 >= 1 /\ b - 4 >= 0 /\ a + 3 >= 0 /\ a + 4 >= 1 ] (2*b, 4) f2(a, b) -> f2(a + 2, b - 3) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ b - 2 >= 1 /\ b - 3 >= 0 /\ a + 2 >= 0 /\ a + 3 >= 1 ] (2*b, 3) f2(a, b) -> f2(a + 1, b - 2) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ b - 1 >= 1 /\ b - 2 >= 0 /\ a + 1 >= 0 /\ a + 2 >= 1 ] (2*b, 2) f2(a, b) -> f2(a, b - 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= 1 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ a + 1 >= 1 ] (?, 1) f1(a, b) -> f1(a + 1, b - 1) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= 1 ] (1, 1) f999(a, b) -> f1(1, b - 1) [ b >= 1 /\ a = 0 ] (?, 1) f2(a, b) -> f2(a - 1, b + 1) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= 1 ] (2*b, 1) f1(a, b) -> f2(a - 1, b) [ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ a >= 1 ] start location: f999 leaf cost: 0 Complexity upper bound ? Time: 8.470 sec (SMT: 7.614 sec)