MAYBE Initial complexity problem: 1: T: (1, 1) f0(a, b) -> f4(c, 0) (?, 1) f4(a, b) -> f4(a, b + 1) [ 0 >= c + 1 ] (?, 1) f4(a, b) -> f4(a, b + 1) (?, 1) f4(a, b) -> f14(a, b) [ a >= 0 /\ b >= a + 1 ] (?, 1) f4(a, b) -> f14(a, b) [ 0 >= a + 1 ] (?, 1) f4(a, b) -> f14(a, b) [ a >= 0 /\ a >= b ] (?, 1) f4(a, b) -> f14(a, b) [ 0 >= c + 1 /\ a >= 0 /\ b >= a + 1 ] start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem: 2: T: (1, 1) f0(a, b) -> f4(c, 0) (?, 1) f4(a, b) -> f4(a, b + 1) [ 0 >= c + 1 ] (?, 1) f4(a, b) -> f4(a, b + 1) start location: f0 leaf cost: 4 Applied AI with 'oct' on problem 2 to obtain the following invariants: For symbol f4: X_2 >= 0 This yielded the following problem: 3: T: (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 /\ 0 >= c + 1 ] (1, 1) f0(a, b) -> f4(c, 0) start location: f0 leaf cost: 4 By chaining the transition f0(a, b) -> f4(c, 0) with all transitions in problem 3, the following new transitions are obtained: f0(a, b) -> f4(c, 1) [ 0 >= 0 /\ 0 >= c' + 1 ] f0(a, b) -> f4(c, 1) [ 0 >= 0 ] We thus obtain the following problem: 4: T: (1, 2) f0(a, b) -> f4(c, 1) [ 0 >= 0 /\ 0 >= c' + 1 ] (1, 2) f0(a, b) -> f4(c, 1) [ 0 >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 /\ 0 >= c + 1 ] start location: f0 leaf cost: 4 By chaining the transition f0(a, b) -> f4(c, 1) [ 0 >= 0 /\ 0 >= c' + 1 ] with all transitions in problem 4, the following new transitions are obtained: f0(a, b) -> f4(c, 2) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 ] f0(a, b) -> f4(c, 2) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 ] We thus obtain the following problem: 5: T: (1, 3) f0(a, b) -> f4(c, 2) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 ] (1, 3) f0(a, b) -> f4(c, 2) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 ] (1, 2) f0(a, b) -> f4(c, 1) [ 0 >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 /\ 0 >= c + 1 ] start location: f0 leaf cost: 4 By chaining the transition f0(a, b) -> f4(c, 2) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 ] with all transitions in problem 5, the following new transitions are obtained: f0(a, b) -> f4(c, 3) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 ] f0(a, b) -> f4(c, 3) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 ] We thus obtain the following problem: 6: T: (1, 4) f0(a, b) -> f4(c, 3) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 ] (1, 4) f0(a, b) -> f4(c, 3) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 ] (1, 3) f0(a, b) -> f4(c, 2) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 ] (1, 2) f0(a, b) -> f4(c, 1) [ 0 >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 /\ 0 >= c + 1 ] start location: f0 leaf cost: 4 By chaining the transition f0(a, b) -> f4(c, 3) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 ] with all transitions in problem 6, the following new transitions are obtained: f0(a, b) -> f4(c, 4) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 ] f0(a, b) -> f4(c, 4) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 ] We thus obtain the following problem: 7: T: (1, 5) f0(a, b) -> f4(c, 4) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 ] (1, 5) f0(a, b) -> f4(c, 4) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 ] (1, 4) f0(a, b) -> f4(c, 3) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 ] (1, 3) f0(a, b) -> f4(c, 2) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 ] (1, 2) f0(a, b) -> f4(c, 1) [ 0 >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 /\ 0 >= c + 1 ] start location: f0 leaf cost: 4 By chaining the transition f0(a, b) -> f4(c, 4) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 ] with all transitions in problem 7, the following new transitions are obtained: f0(a, b) -> f4(c, 5) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 ] f0(a, b) -> f4(c, 5) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 ] We thus obtain the following problem: 8: T: (1, 6) f0(a, b) -> f4(c, 5) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 ] (1, 6) f0(a, b) -> f4(c, 5) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 ] (1, 5) f0(a, b) -> f4(c, 4) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 ] (1, 4) f0(a, b) -> f4(c, 3) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 ] (1, 3) f0(a, b) -> f4(c, 2) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 ] (1, 2) f0(a, b) -> f4(c, 1) [ 0 >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 /\ 0 >= c + 1 ] start location: f0 leaf cost: 4 By chaining the transition f0(a, b) -> f4(c, 5) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 ] with all transitions in problem 8, the following new transitions are obtained: f0(a, b) -> f4(c, 6) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 ] f0(a, b) -> f4(c, 6) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 ] We thus obtain the following problem: 9: T: (1, 7) f0(a, b) -> f4(c, 6) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 ] (1, 7) f0(a, b) -> f4(c, 6) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 ] (1, 6) f0(a, b) -> f4(c, 5) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 ] (1, 5) f0(a, b) -> f4(c, 4) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 ] (1, 4) f0(a, b) -> f4(c, 3) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 ] (1, 3) f0(a, b) -> f4(c, 2) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 ] (1, 2) f0(a, b) -> f4(c, 1) [ 0 >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 /\ 0 >= c + 1 ] start location: f0 leaf cost: 4 By chaining the transition f0(a, b) -> f4(c, 6) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 ] with all transitions in problem 9, the following new transitions are obtained: f0(a, b) -> f4(c, 7) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 ] f0(a, b) -> f4(c, 7) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 ] We thus obtain the following problem: 10: T: (1, 8) f0(a, b) -> f4(c, 7) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 ] (1, 8) f0(a, b) -> f4(c, 7) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 ] (1, 7) f0(a, b) -> f4(c, 6) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 ] (1, 6) f0(a, b) -> f4(c, 5) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 ] (1, 5) f0(a, b) -> f4(c, 4) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 ] (1, 4) f0(a, b) -> f4(c, 3) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 ] (1, 3) f0(a, b) -> f4(c, 2) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 ] (1, 2) f0(a, b) -> f4(c, 1) [ 0 >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 /\ 0 >= c + 1 ] start location: f0 leaf cost: 4 By chaining the transition f0(a, b) -> f4(c, 7) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 ] with all transitions in problem 10, the following new transitions are obtained: f0(a, b) -> f4(c, 8) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 ] f0(a, b) -> f4(c, 8) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 ] We thus obtain the following problem: 11: T: (1, 9) f0(a, b) -> f4(c, 8) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 ] (1, 9) f0(a, b) -> f4(c, 8) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 ] (1, 8) f0(a, b) -> f4(c, 7) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 ] (1, 7) f0(a, b) -> f4(c, 6) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 ] (1, 6) f0(a, b) -> f4(c, 5) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 ] (1, 5) f0(a, b) -> f4(c, 4) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 ] (1, 4) f0(a, b) -> f4(c, 3) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 ] (1, 3) f0(a, b) -> f4(c, 2) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 ] (1, 2) f0(a, b) -> f4(c, 1) [ 0 >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 /\ 0 >= c + 1 ] start location: f0 leaf cost: 4 By chaining the transition f0(a, b) -> f4(c, 8) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 ] with all transitions in problem 11, the following new transitions are obtained: f0(a, b) -> f4(c, 9) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 ] f0(a, b) -> f4(c, 9) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 ] We thus obtain the following problem: 12: T: (1, 10) f0(a, b) -> f4(c, 9) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 ] (1, 10) f0(a, b) -> f4(c, 9) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 ] (1, 9) f0(a, b) -> f4(c, 8) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 ] (1, 8) f0(a, b) -> f4(c, 7) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 ] (1, 7) f0(a, b) -> f4(c, 6) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 ] (1, 6) f0(a, b) -> f4(c, 5) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 ] (1, 5) f0(a, b) -> f4(c, 4) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 ] (1, 4) f0(a, b) -> f4(c, 3) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 ] (1, 3) f0(a, b) -> f4(c, 2) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 ] (1, 2) f0(a, b) -> f4(c, 1) [ 0 >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 /\ 0 >= c + 1 ] start location: f0 leaf cost: 4 By chaining the transition f0(a, b) -> f4(c, 9) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 ] with all transitions in problem 12, the following new transitions are obtained: f0(a, b) -> f4(c, 10) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 ] f0(a, b) -> f4(c, 10) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 ] We thus obtain the following problem: 13: T: (1, 11) f0(a, b) -> f4(c, 10) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 ] (1, 11) f0(a, b) -> f4(c, 10) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 ] (1, 10) f0(a, b) -> f4(c, 9) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 ] (1, 9) f0(a, b) -> f4(c, 8) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 ] (1, 8) f0(a, b) -> f4(c, 7) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 ] (1, 7) f0(a, b) -> f4(c, 6) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 ] (1, 6) f0(a, b) -> f4(c, 5) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 ] (1, 5) f0(a, b) -> f4(c, 4) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 ] (1, 4) f0(a, b) -> f4(c, 3) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 ] (1, 3) f0(a, b) -> f4(c, 2) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 ] (1, 2) f0(a, b) -> f4(c, 1) [ 0 >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 /\ 0 >= c + 1 ] start location: f0 leaf cost: 4 By chaining the transition f0(a, b) -> f4(c, 10) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 ] with all transitions in problem 13, the following new transitions are obtained: f0(a, b) -> f4(c, 11) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 ] f0(a, b) -> f4(c, 11) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 ] We thus obtain the following problem: 14: T: (1, 12) f0(a, b) -> f4(c, 11) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 ] (1, 12) f0(a, b) -> f4(c, 11) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 ] (1, 11) f0(a, b) -> f4(c, 10) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 ] (1, 10) f0(a, b) -> f4(c, 9) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 ] (1, 9) f0(a, b) -> f4(c, 8) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 ] (1, 8) f0(a, b) -> f4(c, 7) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 ] (1, 7) f0(a, b) -> f4(c, 6) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 ] (1, 6) f0(a, b) -> f4(c, 5) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 ] (1, 5) f0(a, b) -> f4(c, 4) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 ] (1, 4) f0(a, b) -> f4(c, 3) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 ] (1, 3) f0(a, b) -> f4(c, 2) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 ] (1, 2) f0(a, b) -> f4(c, 1) [ 0 >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 /\ 0 >= c + 1 ] start location: f0 leaf cost: 4 By chaining the transition f0(a, b) -> f4(c, 11) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 ] with all transitions in problem 14, the following new transitions are obtained: f0(a, b) -> f4(c, 12) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 /\ 0 >= c'''''''''''' + 1 ] f0(a, b) -> f4(c, 12) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 ] We thus obtain the following problem: 15: T: (1, 13) f0(a, b) -> f4(c, 12) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 /\ 0 >= c'''''''''''' + 1 ] (1, 13) f0(a, b) -> f4(c, 12) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 ] (1, 12) f0(a, b) -> f4(c, 11) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 ] (1, 11) f0(a, b) -> f4(c, 10) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 ] (1, 10) f0(a, b) -> f4(c, 9) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 ] (1, 9) f0(a, b) -> f4(c, 8) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 ] (1, 8) f0(a, b) -> f4(c, 7) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 ] (1, 7) f0(a, b) -> f4(c, 6) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 ] (1, 6) f0(a, b) -> f4(c, 5) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 ] (1, 5) f0(a, b) -> f4(c, 4) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 ] (1, 4) f0(a, b) -> f4(c, 3) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 ] (1, 3) f0(a, b) -> f4(c, 2) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 ] (1, 2) f0(a, b) -> f4(c, 1) [ 0 >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 /\ 0 >= c + 1 ] start location: f0 leaf cost: 4 By chaining the transition f0(a, b) -> f4(c, 12) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 /\ 0 >= c'''''''''''' + 1 ] with all transitions in problem 15, the following new transitions are obtained: f0(a, b) -> f4(c, 13) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 /\ 0 >= c'''''''''''' + 1 /\ 12 >= 0 /\ 0 >= c''''''''''''' + 1 ] f0(a, b) -> f4(c, 13) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 /\ 0 >= c'''''''''''' + 1 /\ 12 >= 0 ] We thus obtain the following problem: 16: T: (1, 14) f0(a, b) -> f4(c, 13) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 /\ 0 >= c'''''''''''' + 1 /\ 12 >= 0 /\ 0 >= c''''''''''''' + 1 ] (1, 14) f0(a, b) -> f4(c, 13) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 /\ 0 >= c'''''''''''' + 1 /\ 12 >= 0 ] (1, 13) f0(a, b) -> f4(c, 12) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 ] (1, 12) f0(a, b) -> f4(c, 11) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 ] (1, 11) f0(a, b) -> f4(c, 10) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 ] (1, 10) f0(a, b) -> f4(c, 9) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 ] (1, 9) f0(a, b) -> f4(c, 8) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 ] (1, 8) f0(a, b) -> f4(c, 7) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 ] (1, 7) f0(a, b) -> f4(c, 6) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 ] (1, 6) f0(a, b) -> f4(c, 5) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 ] (1, 5) f0(a, b) -> f4(c, 4) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 ] (1, 4) f0(a, b) -> f4(c, 3) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 ] (1, 3) f0(a, b) -> f4(c, 2) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 ] (1, 2) f0(a, b) -> f4(c, 1) [ 0 >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 /\ 0 >= c + 1 ] start location: f0 leaf cost: 4 By chaining the transition f0(a, b) -> f4(c, 13) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 /\ 0 >= c'''''''''''' + 1 /\ 12 >= 0 /\ 0 >= c''''''''''''' + 1 ] with all transitions in problem 16, the following new transitions are obtained: f0(a, b) -> f4(c, 14) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 /\ 0 >= c'''''''''''' + 1 /\ 12 >= 0 /\ 0 >= c''''''''''''' + 1 /\ 13 >= 0 /\ 0 >= c'''''''''''''' + 1 ] f0(a, b) -> f4(c, 14) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 /\ 0 >= c'''''''''''' + 1 /\ 12 >= 0 /\ 0 >= c''''''''''''' + 1 /\ 13 >= 0 ] We thus obtain the following problem: 17: T: (1, 15) f0(a, b) -> f4(c, 14) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 /\ 0 >= c'''''''''''' + 1 /\ 12 >= 0 /\ 0 >= c''''''''''''' + 1 /\ 13 >= 0 /\ 0 >= c'''''''''''''' + 1 ] (1, 15) f0(a, b) -> f4(c, 14) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 /\ 0 >= c'''''''''''' + 1 /\ 12 >= 0 /\ 0 >= c''''''''''''' + 1 /\ 13 >= 0 ] (1, 14) f0(a, b) -> f4(c, 13) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 /\ 0 >= c'''''''''''' + 1 /\ 12 >= 0 ] (1, 13) f0(a, b) -> f4(c, 12) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 ] (1, 12) f0(a, b) -> f4(c, 11) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 ] (1, 11) f0(a, b) -> f4(c, 10) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 ] (1, 10) f0(a, b) -> f4(c, 9) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 ] (1, 9) f0(a, b) -> f4(c, 8) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 ] (1, 8) f0(a, b) -> f4(c, 7) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 ] (1, 7) f0(a, b) -> f4(c, 6) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 ] (1, 6) f0(a, b) -> f4(c, 5) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 ] (1, 5) f0(a, b) -> f4(c, 4) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 ] (1, 4) f0(a, b) -> f4(c, 3) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 ] (1, 3) f0(a, b) -> f4(c, 2) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 ] (1, 2) f0(a, b) -> f4(c, 1) [ 0 >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 /\ 0 >= c + 1 ] start location: f0 leaf cost: 4 By chaining the transition f0(a, b) -> f4(c, 14) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 /\ 0 >= c'''''''''''' + 1 /\ 12 >= 0 /\ 0 >= c''''''''''''' + 1 /\ 13 >= 0 /\ 0 >= c'''''''''''''' + 1 ] with all transitions in problem 17, the following new transitions are obtained: f0(a, b) -> f4(c, 15) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 /\ 0 >= c'''''''''''' + 1 /\ 12 >= 0 /\ 0 >= c''''''''''''' + 1 /\ 13 >= 0 /\ 0 >= c'''''''''''''' + 1 /\ 14 >= 0 /\ 0 >= c''''''''''''''' + 1 ] f0(a, b) -> f4(c, 15) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 /\ 0 >= c'''''''''''' + 1 /\ 12 >= 0 /\ 0 >= c''''''''''''' + 1 /\ 13 >= 0 /\ 0 >= c'''''''''''''' + 1 /\ 14 >= 0 ] We thus obtain the following problem: 18: T: (1, 16) f0(a, b) -> f4(c, 15) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 /\ 0 >= c'''''''''''' + 1 /\ 12 >= 0 /\ 0 >= c''''''''''''' + 1 /\ 13 >= 0 /\ 0 >= c'''''''''''''' + 1 /\ 14 >= 0 /\ 0 >= c''''''''''''''' + 1 ] (1, 16) f0(a, b) -> f4(c, 15) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 /\ 0 >= c'''''''''''' + 1 /\ 12 >= 0 /\ 0 >= c''''''''''''' + 1 /\ 13 >= 0 /\ 0 >= c'''''''''''''' + 1 /\ 14 >= 0 ] (1, 15) f0(a, b) -> f4(c, 14) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 /\ 0 >= c'''''''''''' + 1 /\ 12 >= 0 /\ 0 >= c''''''''''''' + 1 /\ 13 >= 0 ] (1, 14) f0(a, b) -> f4(c, 13) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 /\ 0 >= c'''''''''''' + 1 /\ 12 >= 0 ] (1, 13) f0(a, b) -> f4(c, 12) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 /\ 0 >= c''''''''''' + 1 /\ 11 >= 0 ] (1, 12) f0(a, b) -> f4(c, 11) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 /\ 0 >= c'''''''''' + 1 /\ 10 >= 0 ] (1, 11) f0(a, b) -> f4(c, 10) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 /\ 0 >= c''''''''' + 1 /\ 9 >= 0 ] (1, 10) f0(a, b) -> f4(c, 9) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 /\ 0 >= c'''''''' + 1 /\ 8 >= 0 ] (1, 9) f0(a, b) -> f4(c, 8) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 /\ 0 >= c''''''' + 1 /\ 7 >= 0 ] (1, 8) f0(a, b) -> f4(c, 7) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 /\ 0 >= c'''''' + 1 /\ 6 >= 0 ] (1, 7) f0(a, b) -> f4(c, 6) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 /\ 0 >= c''''' + 1 /\ 5 >= 0 ] (1, 6) f0(a, b) -> f4(c, 5) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 /\ 0 >= c'''' + 1 /\ 4 >= 0 ] (1, 5) f0(a, b) -> f4(c, 4) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 /\ 0 >= c''' + 1 /\ 3 >= 0 ] (1, 4) f0(a, b) -> f4(c, 3) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 /\ 0 >= c'' + 1 /\ 2 >= 0 ] (1, 3) f0(a, b) -> f4(c, 2) [ 0 >= 0 /\ 0 >= c' + 1 /\ 1 >= 0 ] (1, 2) f0(a, b) -> f4(c, 1) [ 0 >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 ] (?, 1) f4(a, b) -> f4(a, b + 1) [ b >= 0 /\ 0 >= c + 1 ] start location: f0 leaf cost: 4 Complexity upper bound ? Time: 1.424 sec (SMT: 1.267 sec)