MAYBE Initial complexity problem: 1: T: (?, 1) f2(a, b, c, d, e, f) -> f2(a + 1, g, g, d, e, f) [ g >= 1 /\ a >= 1 ] (?, 1) f2(a, b, c, d, e, f) -> f2(a + 1, g, g, d, e, f) [ 0 >= g + 1 /\ a >= 1 ] (?, 1) f2(a, b, c, d, e, f) -> f0(a, 0, 0, g, e, f) (?, 1) f3(a, b, c, d, e, f) -> f2(a + 1, g, g, d, e, f) [ g >= 1 /\ a >= 1 ] (?, 1) f3(a, b, c, d, e, f) -> f2(a + 1, g, g, d, e, f) [ 0 >= g + 1 /\ a >= 1 ] (?, 1) f3(a, b, c, d, e, f) -> f0(a, 0, 0, g, e, f) (1, 1) f4(a, b, c, d, e, f) -> f2(h + 1, g, g, d, h, h) [ g >= 1 /\ h >= 1 ] (1, 1) f4(a, b, c, d, e, f) -> f2(h + 1, g, g, d, h, h) [ 0 >= g + 1 /\ h >= 1 ] (1, 1) f4(a, b, c, d, e, f) -> f0(g, 0, 0, h, g, g) start location: f4 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a]. We thus obtain the following problem: 2: T: (1, 1) f4(a) -> f0(g) (1, 1) f4(a) -> f2(h + 1) [ 0 >= g + 1 /\ h >= 1 ] (1, 1) f4(a) -> f2(h + 1) [ g >= 1 /\ h >= 1 ] (?, 1) f3(a) -> f0(a) (?, 1) f3(a) -> f2(a + 1) [ 0 >= g + 1 /\ a >= 1 ] (?, 1) f3(a) -> f2(a + 1) [ g >= 1 /\ a >= 1 ] (?, 1) f2(a) -> f0(a) (?, 1) f2(a) -> f2(a + 1) [ 0 >= g + 1 /\ a >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ g >= 1 /\ a >= 1 ] start location: f4 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (1, 1) f4(a) -> f2(h + 1) [ 0 >= g + 1 /\ h >= 1 ] (1, 1) f4(a) -> f2(h + 1) [ g >= 1 /\ h >= 1 ] (?, 1) f3(a) -> f2(a + 1) [ 0 >= g + 1 /\ a >= 1 ] (?, 1) f3(a) -> f2(a + 1) [ g >= 1 /\ a >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ 0 >= g + 1 /\ a >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ g >= 1 /\ a >= 1 ] start location: f4 leaf cost: 3 Testing for reachability in the complexity graph removes the following transitions from problem 3: f3(a) -> f2(a + 1) [ 0 >= g + 1 /\ a >= 1 ] f3(a) -> f2(a + 1) [ g >= 1 /\ a >= 1 ] We thus obtain the following problem: 4: T: (?, 1) f2(a) -> f2(a + 1) [ g >= 1 /\ a >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ 0 >= g + 1 /\ a >= 1 ] (1, 1) f4(a) -> f2(h + 1) [ g >= 1 /\ h >= 1 ] (1, 1) f4(a) -> f2(h + 1) [ 0 >= g + 1 /\ h >= 1 ] start location: f4 leaf cost: 3 Applied AI with 'oct' on problem 4 to obtain the following invariants: For symbol f2: X_1 - 2 >= 0 This yielded the following problem: 5: T: (1, 1) f4(a) -> f2(h + 1) [ 0 >= g + 1 /\ h >= 1 ] (1, 1) f4(a) -> f2(h + 1) [ g >= 1 /\ h >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ 0 >= g + 1 /\ a >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ g >= 1 /\ a >= 1 ] start location: f4 leaf cost: 3 By chaining the transition f4(a) -> f2(h + 1) [ 0 >= g + 1 /\ h >= 1 ] with all transitions in problem 5, the following new transitions are obtained: f4(a) -> f2(h + 2) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 ] f4(a) -> f2(h + 2) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ 0 >= g' + 1 /\ h + 1 >= 1 ] We thus obtain the following problem: 6: T: (1, 2) f4(a) -> f2(h + 2) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 ] (1, 2) f4(a) -> f2(h + 2) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ 0 >= g' + 1 /\ h + 1 >= 1 ] (1, 1) f4(a) -> f2(h + 1) [ g >= 1 /\ h >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ 0 >= g + 1 /\ a >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ g >= 1 /\ a >= 1 ] start location: f4 leaf cost: 3 By chaining the transition f4(a) -> f2(h + 2) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 ] with all transitions in problem 6, the following new transitions are obtained: f4(a) -> f2(h + 3) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 ] f4(a) -> f2(h + 3) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ 0 >= g'' + 1 /\ h + 2 >= 1 ] We thus obtain the following problem: 7: T: (1, 3) f4(a) -> f2(h + 3) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 ] (1, 3) f4(a) -> f2(h + 3) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ 0 >= g'' + 1 /\ h + 2 >= 1 ] (1, 2) f4(a) -> f2(h + 2) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ 0 >= g' + 1 /\ h + 1 >= 1 ] (1, 1) f4(a) -> f2(h + 1) [ g >= 1 /\ h >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ 0 >= g + 1 /\ a >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ g >= 1 /\ a >= 1 ] start location: f4 leaf cost: 3 By chaining the transition f4(a) -> f2(h + 3) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 ] with all transitions in problem 7, the following new transitions are obtained: f4(a) -> f2(h + 4) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 ] f4(a) -> f2(h + 4) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ 0 >= g''' + 1 /\ h + 3 >= 1 ] We thus obtain the following problem: 8: T: (1, 4) f4(a) -> f2(h + 4) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 ] (1, 4) f4(a) -> f2(h + 4) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ 0 >= g''' + 1 /\ h + 3 >= 1 ] (1, 3) f4(a) -> f2(h + 3) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ 0 >= g'' + 1 /\ h + 2 >= 1 ] (1, 2) f4(a) -> f2(h + 2) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ 0 >= g' + 1 /\ h + 1 >= 1 ] (1, 1) f4(a) -> f2(h + 1) [ g >= 1 /\ h >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ 0 >= g + 1 /\ a >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ g >= 1 /\ a >= 1 ] start location: f4 leaf cost: 3 By chaining the transition f4(a) -> f2(h + 4) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 ] with all transitions in problem 8, the following new transitions are obtained: f4(a) -> f2(h + 5) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 ] f4(a) -> f2(h + 5) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ 0 >= g'''' + 1 /\ h + 4 >= 1 ] We thus obtain the following problem: 9: T: (1, 5) f4(a) -> f2(h + 5) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 ] (1, 5) f4(a) -> f2(h + 5) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ 0 >= g'''' + 1 /\ h + 4 >= 1 ] (1, 4) f4(a) -> f2(h + 4) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ 0 >= g''' + 1 /\ h + 3 >= 1 ] (1, 3) f4(a) -> f2(h + 3) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ 0 >= g'' + 1 /\ h + 2 >= 1 ] (1, 2) f4(a) -> f2(h + 2) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ 0 >= g' + 1 /\ h + 1 >= 1 ] (1, 1) f4(a) -> f2(h + 1) [ g >= 1 /\ h >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ 0 >= g + 1 /\ a >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ g >= 1 /\ a >= 1 ] start location: f4 leaf cost: 3 By chaining the transition f4(a) -> f2(h + 5) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 ] with all transitions in problem 9, the following new transitions are obtained: f4(a) -> f2(h + 6) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 ] f4(a) -> f2(h + 6) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ 0 >= g''''' + 1 /\ h + 5 >= 1 ] We thus obtain the following problem: 10: T: (1, 6) f4(a) -> f2(h + 6) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 ] (1, 6) f4(a) -> f2(h + 6) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ 0 >= g''''' + 1 /\ h + 5 >= 1 ] (1, 5) f4(a) -> f2(h + 5) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ 0 >= g'''' + 1 /\ h + 4 >= 1 ] (1, 4) f4(a) -> f2(h + 4) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ 0 >= g''' + 1 /\ h + 3 >= 1 ] (1, 3) f4(a) -> f2(h + 3) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ 0 >= g'' + 1 /\ h + 2 >= 1 ] (1, 2) f4(a) -> f2(h + 2) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ 0 >= g' + 1 /\ h + 1 >= 1 ] (1, 1) f4(a) -> f2(h + 1) [ g >= 1 /\ h >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ 0 >= g + 1 /\ a >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ g >= 1 /\ a >= 1 ] start location: f4 leaf cost: 3 By chaining the transition f4(a) -> f2(h + 6) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 ] with all transitions in problem 10, the following new transitions are obtained: f4(a) -> f2(h + 7) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 ] f4(a) -> f2(h + 7) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ 0 >= g'''''' + 1 /\ h + 6 >= 1 ] We thus obtain the following problem: 11: T: (1, 7) f4(a) -> f2(h + 7) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 ] (1, 7) f4(a) -> f2(h + 7) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ 0 >= g'''''' + 1 /\ h + 6 >= 1 ] (1, 6) f4(a) -> f2(h + 6) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ 0 >= g''''' + 1 /\ h + 5 >= 1 ] (1, 5) f4(a) -> f2(h + 5) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ 0 >= g'''' + 1 /\ h + 4 >= 1 ] (1, 4) f4(a) -> f2(h + 4) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ 0 >= g''' + 1 /\ h + 3 >= 1 ] (1, 3) f4(a) -> f2(h + 3) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ 0 >= g'' + 1 /\ h + 2 >= 1 ] (1, 2) f4(a) -> f2(h + 2) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ 0 >= g' + 1 /\ h + 1 >= 1 ] (1, 1) f4(a) -> f2(h + 1) [ g >= 1 /\ h >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ 0 >= g + 1 /\ a >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ g >= 1 /\ a >= 1 ] start location: f4 leaf cost: 3 By chaining the transition f4(a) -> f2(h + 7) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 ] with all transitions in problem 11, the following new transitions are obtained: f4(a) -> f2(h + 8) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 ] f4(a) -> f2(h + 8) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ 0 >= g''''''' + 1 /\ h + 7 >= 1 ] We thus obtain the following problem: 12: T: (1, 8) f4(a) -> f2(h + 8) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 ] (1, 8) f4(a) -> f2(h + 8) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ 0 >= g''''''' + 1 /\ h + 7 >= 1 ] (1, 7) f4(a) -> f2(h + 7) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ 0 >= g'''''' + 1 /\ h + 6 >= 1 ] (1, 6) f4(a) -> f2(h + 6) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ 0 >= g''''' + 1 /\ h + 5 >= 1 ] (1, 5) f4(a) -> f2(h + 5) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ 0 >= g'''' + 1 /\ h + 4 >= 1 ] (1, 4) f4(a) -> f2(h + 4) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ 0 >= g''' + 1 /\ h + 3 >= 1 ] (1, 3) f4(a) -> f2(h + 3) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ 0 >= g'' + 1 /\ h + 2 >= 1 ] (1, 2) f4(a) -> f2(h + 2) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ 0 >= g' + 1 /\ h + 1 >= 1 ] (1, 1) f4(a) -> f2(h + 1) [ g >= 1 /\ h >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ 0 >= g + 1 /\ a >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ g >= 1 /\ a >= 1 ] start location: f4 leaf cost: 3 By chaining the transition f4(a) -> f2(h + 8) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 ] with all transitions in problem 12, the following new transitions are obtained: f4(a) -> f2(h + 9) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 ] f4(a) -> f2(h + 9) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ 0 >= g'''''''' + 1 /\ h + 8 >= 1 ] We thus obtain the following problem: 13: T: (1, 9) f4(a) -> f2(h + 9) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 ] (1, 9) f4(a) -> f2(h + 9) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ 0 >= g'''''''' + 1 /\ h + 8 >= 1 ] (1, 8) f4(a) -> f2(h + 8) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ 0 >= g''''''' + 1 /\ h + 7 >= 1 ] (1, 7) f4(a) -> f2(h + 7) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ 0 >= g'''''' + 1 /\ h + 6 >= 1 ] (1, 6) f4(a) -> f2(h + 6) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ 0 >= g''''' + 1 /\ h + 5 >= 1 ] (1, 5) f4(a) -> f2(h + 5) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ 0 >= g'''' + 1 /\ h + 4 >= 1 ] (1, 4) f4(a) -> f2(h + 4) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ 0 >= g''' + 1 /\ h + 3 >= 1 ] (1, 3) f4(a) -> f2(h + 3) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ 0 >= g'' + 1 /\ h + 2 >= 1 ] (1, 2) f4(a) -> f2(h + 2) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ 0 >= g' + 1 /\ h + 1 >= 1 ] (1, 1) f4(a) -> f2(h + 1) [ g >= 1 /\ h >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ 0 >= g + 1 /\ a >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ g >= 1 /\ a >= 1 ] start location: f4 leaf cost: 3 By chaining the transition f4(a) -> f2(h + 9) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 ] with all transitions in problem 13, the following new transitions are obtained: f4(a) -> f2(h + 10) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 ] f4(a) -> f2(h + 10) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ 0 >= g''''''''' + 1 /\ h + 9 >= 1 ] We thus obtain the following problem: 14: T: (1, 10) f4(a) -> f2(h + 10) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 ] (1, 10) f4(a) -> f2(h + 10) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ 0 >= g''''''''' + 1 /\ h + 9 >= 1 ] (1, 9) f4(a) -> f2(h + 9) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ 0 >= g'''''''' + 1 /\ h + 8 >= 1 ] (1, 8) f4(a) -> f2(h + 8) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ 0 >= g''''''' + 1 /\ h + 7 >= 1 ] (1, 7) f4(a) -> f2(h + 7) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ 0 >= g'''''' + 1 /\ h + 6 >= 1 ] (1, 6) f4(a) -> f2(h + 6) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ 0 >= g''''' + 1 /\ h + 5 >= 1 ] (1, 5) f4(a) -> f2(h + 5) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ 0 >= g'''' + 1 /\ h + 4 >= 1 ] (1, 4) f4(a) -> f2(h + 4) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ 0 >= g''' + 1 /\ h + 3 >= 1 ] (1, 3) f4(a) -> f2(h + 3) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ 0 >= g'' + 1 /\ h + 2 >= 1 ] (1, 2) f4(a) -> f2(h + 2) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ 0 >= g' + 1 /\ h + 1 >= 1 ] (1, 1) f4(a) -> f2(h + 1) [ g >= 1 /\ h >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ 0 >= g + 1 /\ a >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ g >= 1 /\ a >= 1 ] start location: f4 leaf cost: 3 By chaining the transition f4(a) -> f2(h + 10) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 ] with all transitions in problem 14, the following new transitions are obtained: f4(a) -> f2(h + 11) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 ] f4(a) -> f2(h + 11) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ 0 >= g'''''''''' + 1 /\ h + 10 >= 1 ] We thus obtain the following problem: 15: T: (1, 11) f4(a) -> f2(h + 11) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 ] (1, 11) f4(a) -> f2(h + 11) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ 0 >= g'''''''''' + 1 /\ h + 10 >= 1 ] (1, 10) f4(a) -> f2(h + 10) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ 0 >= g''''''''' + 1 /\ h + 9 >= 1 ] (1, 9) f4(a) -> f2(h + 9) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ 0 >= g'''''''' + 1 /\ h + 8 >= 1 ] (1, 8) f4(a) -> f2(h + 8) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ 0 >= g''''''' + 1 /\ h + 7 >= 1 ] (1, 7) f4(a) -> f2(h + 7) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ 0 >= g'''''' + 1 /\ h + 6 >= 1 ] (1, 6) f4(a) -> f2(h + 6) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ 0 >= g''''' + 1 /\ h + 5 >= 1 ] (1, 5) f4(a) -> f2(h + 5) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ 0 >= g'''' + 1 /\ h + 4 >= 1 ] (1, 4) f4(a) -> f2(h + 4) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ 0 >= g''' + 1 /\ h + 3 >= 1 ] (1, 3) f4(a) -> f2(h + 3) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ 0 >= g'' + 1 /\ h + 2 >= 1 ] (1, 2) f4(a) -> f2(h + 2) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ 0 >= g' + 1 /\ h + 1 >= 1 ] (1, 1) f4(a) -> f2(h + 1) [ g >= 1 /\ h >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ 0 >= g + 1 /\ a >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ g >= 1 /\ a >= 1 ] start location: f4 leaf cost: 3 By chaining the transition f4(a) -> f2(h + 11) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 ] with all transitions in problem 15, the following new transitions are obtained: f4(a) -> f2(h + 12) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 ] f4(a) -> f2(h + 12) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ 0 >= g''''''''''' + 1 /\ h + 11 >= 1 ] We thus obtain the following problem: 16: T: (1, 12) f4(a) -> f2(h + 12) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 ] (1, 12) f4(a) -> f2(h + 12) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ 0 >= g''''''''''' + 1 /\ h + 11 >= 1 ] (1, 11) f4(a) -> f2(h + 11) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ 0 >= g'''''''''' + 1 /\ h + 10 >= 1 ] (1, 10) f4(a) -> f2(h + 10) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ 0 >= g''''''''' + 1 /\ h + 9 >= 1 ] (1, 9) f4(a) -> f2(h + 9) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ 0 >= g'''''''' + 1 /\ h + 8 >= 1 ] (1, 8) f4(a) -> f2(h + 8) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ 0 >= g''''''' + 1 /\ h + 7 >= 1 ] (1, 7) f4(a) -> f2(h + 7) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ 0 >= g'''''' + 1 /\ h + 6 >= 1 ] (1, 6) f4(a) -> f2(h + 6) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ 0 >= g''''' + 1 /\ h + 5 >= 1 ] (1, 5) f4(a) -> f2(h + 5) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ 0 >= g'''' + 1 /\ h + 4 >= 1 ] (1, 4) f4(a) -> f2(h + 4) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ 0 >= g''' + 1 /\ h + 3 >= 1 ] (1, 3) f4(a) -> f2(h + 3) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ 0 >= g'' + 1 /\ h + 2 >= 1 ] (1, 2) f4(a) -> f2(h + 2) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ 0 >= g' + 1 /\ h + 1 >= 1 ] (1, 1) f4(a) -> f2(h + 1) [ g >= 1 /\ h >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ 0 >= g + 1 /\ a >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ g >= 1 /\ a >= 1 ] start location: f4 leaf cost: 3 By chaining the transition f4(a) -> f2(h + 12) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 ] with all transitions in problem 16, the following new transitions are obtained: f4(a) -> f2(h + 13) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ g'''''''''''' >= 1 /\ h + 12 >= 1 ] f4(a) -> f2(h + 13) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ 0 >= g'''''''''''' + 1 /\ h + 12 >= 1 ] We thus obtain the following problem: 17: T: (1, 13) f4(a) -> f2(h + 13) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ g'''''''''''' >= 1 /\ h + 12 >= 1 ] (1, 13) f4(a) -> f2(h + 13) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ 0 >= g'''''''''''' + 1 /\ h + 12 >= 1 ] (1, 12) f4(a) -> f2(h + 12) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ 0 >= g''''''''''' + 1 /\ h + 11 >= 1 ] (1, 11) f4(a) -> f2(h + 11) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ 0 >= g'''''''''' + 1 /\ h + 10 >= 1 ] (1, 10) f4(a) -> f2(h + 10) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ 0 >= g''''''''' + 1 /\ h + 9 >= 1 ] (1, 9) f4(a) -> f2(h + 9) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ 0 >= g'''''''' + 1 /\ h + 8 >= 1 ] (1, 8) f4(a) -> f2(h + 8) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ 0 >= g''''''' + 1 /\ h + 7 >= 1 ] (1, 7) f4(a) -> f2(h + 7) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ 0 >= g'''''' + 1 /\ h + 6 >= 1 ] (1, 6) f4(a) -> f2(h + 6) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ 0 >= g''''' + 1 /\ h + 5 >= 1 ] (1, 5) f4(a) -> f2(h + 5) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ 0 >= g'''' + 1 /\ h + 4 >= 1 ] (1, 4) f4(a) -> f2(h + 4) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ 0 >= g''' + 1 /\ h + 3 >= 1 ] (1, 3) f4(a) -> f2(h + 3) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ 0 >= g'' + 1 /\ h + 2 >= 1 ] (1, 2) f4(a) -> f2(h + 2) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ 0 >= g' + 1 /\ h + 1 >= 1 ] (1, 1) f4(a) -> f2(h + 1) [ g >= 1 /\ h >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ 0 >= g + 1 /\ a >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ g >= 1 /\ a >= 1 ] start location: f4 leaf cost: 3 By chaining the transition f4(a) -> f2(h + 13) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ g'''''''''''' >= 1 /\ h + 12 >= 1 ] with all transitions in problem 17, the following new transitions are obtained: f4(a) -> f2(h + 14) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ g'''''''''''' >= 1 /\ h + 12 >= 1 /\ h + 11 >= 0 /\ g''''''''''''' >= 1 /\ h + 13 >= 1 ] f4(a) -> f2(h + 14) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ g'''''''''''' >= 1 /\ h + 12 >= 1 /\ h + 11 >= 0 /\ 0 >= g''''''''''''' + 1 /\ h + 13 >= 1 ] We thus obtain the following problem: 18: T: (1, 14) f4(a) -> f2(h + 14) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ g'''''''''''' >= 1 /\ h + 12 >= 1 /\ h + 11 >= 0 /\ g''''''''''''' >= 1 /\ h + 13 >= 1 ] (1, 14) f4(a) -> f2(h + 14) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ g'''''''''''' >= 1 /\ h + 12 >= 1 /\ h + 11 >= 0 /\ 0 >= g''''''''''''' + 1 /\ h + 13 >= 1 ] (1, 13) f4(a) -> f2(h + 13) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ 0 >= g'''''''''''' + 1 /\ h + 12 >= 1 ] (1, 12) f4(a) -> f2(h + 12) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ 0 >= g''''''''''' + 1 /\ h + 11 >= 1 ] (1, 11) f4(a) -> f2(h + 11) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ 0 >= g'''''''''' + 1 /\ h + 10 >= 1 ] (1, 10) f4(a) -> f2(h + 10) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ 0 >= g''''''''' + 1 /\ h + 9 >= 1 ] (1, 9) f4(a) -> f2(h + 9) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ 0 >= g'''''''' + 1 /\ h + 8 >= 1 ] (1, 8) f4(a) -> f2(h + 8) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ 0 >= g''''''' + 1 /\ h + 7 >= 1 ] (1, 7) f4(a) -> f2(h + 7) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ 0 >= g'''''' + 1 /\ h + 6 >= 1 ] (1, 6) f4(a) -> f2(h + 6) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ 0 >= g''''' + 1 /\ h + 5 >= 1 ] (1, 5) f4(a) -> f2(h + 5) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ 0 >= g'''' + 1 /\ h + 4 >= 1 ] (1, 4) f4(a) -> f2(h + 4) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ 0 >= g''' + 1 /\ h + 3 >= 1 ] (1, 3) f4(a) -> f2(h + 3) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ 0 >= g'' + 1 /\ h + 2 >= 1 ] (1, 2) f4(a) -> f2(h + 2) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ 0 >= g' + 1 /\ h + 1 >= 1 ] (1, 1) f4(a) -> f2(h + 1) [ g >= 1 /\ h >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ 0 >= g + 1 /\ a >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ g >= 1 /\ a >= 1 ] start location: f4 leaf cost: 3 By chaining the transition f4(a) -> f2(h + 14) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ g'''''''''''' >= 1 /\ h + 12 >= 1 /\ h + 11 >= 0 /\ g''''''''''''' >= 1 /\ h + 13 >= 1 ] with all transitions in problem 18, the following new transitions are obtained: f4(a) -> f2(h + 15) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ g'''''''''''' >= 1 /\ h + 12 >= 1 /\ h + 11 >= 0 /\ g''''''''''''' >= 1 /\ h + 13 >= 1 /\ h + 12 >= 0 /\ g'''''''''''''' >= 1 /\ h + 14 >= 1 ] f4(a) -> f2(h + 15) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ g'''''''''''' >= 1 /\ h + 12 >= 1 /\ h + 11 >= 0 /\ g''''''''''''' >= 1 /\ h + 13 >= 1 /\ h + 12 >= 0 /\ 0 >= g'''''''''''''' + 1 /\ h + 14 >= 1 ] We thus obtain the following problem: 19: T: (1, 15) f4(a) -> f2(h + 15) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ g'''''''''''' >= 1 /\ h + 12 >= 1 /\ h + 11 >= 0 /\ g''''''''''''' >= 1 /\ h + 13 >= 1 /\ h + 12 >= 0 /\ g'''''''''''''' >= 1 /\ h + 14 >= 1 ] (1, 15) f4(a) -> f2(h + 15) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ g'''''''''''' >= 1 /\ h + 12 >= 1 /\ h + 11 >= 0 /\ g''''''''''''' >= 1 /\ h + 13 >= 1 /\ h + 12 >= 0 /\ 0 >= g'''''''''''''' + 1 /\ h + 14 >= 1 ] (1, 14) f4(a) -> f2(h + 14) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ g'''''''''''' >= 1 /\ h + 12 >= 1 /\ h + 11 >= 0 /\ 0 >= g''''''''''''' + 1 /\ h + 13 >= 1 ] (1, 13) f4(a) -> f2(h + 13) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ 0 >= g'''''''''''' + 1 /\ h + 12 >= 1 ] (1, 12) f4(a) -> f2(h + 12) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ 0 >= g''''''''''' + 1 /\ h + 11 >= 1 ] (1, 11) f4(a) -> f2(h + 11) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ 0 >= g'''''''''' + 1 /\ h + 10 >= 1 ] (1, 10) f4(a) -> f2(h + 10) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ 0 >= g''''''''' + 1 /\ h + 9 >= 1 ] (1, 9) f4(a) -> f2(h + 9) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ 0 >= g'''''''' + 1 /\ h + 8 >= 1 ] (1, 8) f4(a) -> f2(h + 8) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ 0 >= g''''''' + 1 /\ h + 7 >= 1 ] (1, 7) f4(a) -> f2(h + 7) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ 0 >= g'''''' + 1 /\ h + 6 >= 1 ] (1, 6) f4(a) -> f2(h + 6) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ 0 >= g''''' + 1 /\ h + 5 >= 1 ] (1, 5) f4(a) -> f2(h + 5) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ 0 >= g'''' + 1 /\ h + 4 >= 1 ] (1, 4) f4(a) -> f2(h + 4) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ 0 >= g''' + 1 /\ h + 3 >= 1 ] (1, 3) f4(a) -> f2(h + 3) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ 0 >= g'' + 1 /\ h + 2 >= 1 ] (1, 2) f4(a) -> f2(h + 2) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ 0 >= g' + 1 /\ h + 1 >= 1 ] (1, 1) f4(a) -> f2(h + 1) [ g >= 1 /\ h >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ 0 >= g + 1 /\ a >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ g >= 1 /\ a >= 1 ] start location: f4 leaf cost: 3 By chaining the transition f4(a) -> f2(h + 15) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ g'''''''''''' >= 1 /\ h + 12 >= 1 /\ h + 11 >= 0 /\ g''''''''''''' >= 1 /\ h + 13 >= 1 /\ h + 12 >= 0 /\ g'''''''''''''' >= 1 /\ h + 14 >= 1 ] with all transitions in problem 19, the following new transitions are obtained: f4(a) -> f2(h + 16) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ g'''''''''''' >= 1 /\ h + 12 >= 1 /\ h + 11 >= 0 /\ g''''''''''''' >= 1 /\ h + 13 >= 1 /\ h + 12 >= 0 /\ g'''''''''''''' >= 1 /\ h + 14 >= 1 /\ h + 13 >= 0 /\ g''''''''''''''' >= 1 /\ h + 15 >= 1 ] f4(a) -> f2(h + 16) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ g'''''''''''' >= 1 /\ h + 12 >= 1 /\ h + 11 >= 0 /\ g''''''''''''' >= 1 /\ h + 13 >= 1 /\ h + 12 >= 0 /\ g'''''''''''''' >= 1 /\ h + 14 >= 1 /\ h + 13 >= 0 /\ 0 >= g''''''''''''''' + 1 /\ h + 15 >= 1 ] We thus obtain the following problem: 20: T: (1, 16) f4(a) -> f2(h + 16) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ g'''''''''''' >= 1 /\ h + 12 >= 1 /\ h + 11 >= 0 /\ g''''''''''''' >= 1 /\ h + 13 >= 1 /\ h + 12 >= 0 /\ g'''''''''''''' >= 1 /\ h + 14 >= 1 /\ h + 13 >= 0 /\ g''''''''''''''' >= 1 /\ h + 15 >= 1 ] (1, 16) f4(a) -> f2(h + 16) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ g'''''''''''' >= 1 /\ h + 12 >= 1 /\ h + 11 >= 0 /\ g''''''''''''' >= 1 /\ h + 13 >= 1 /\ h + 12 >= 0 /\ g'''''''''''''' >= 1 /\ h + 14 >= 1 /\ h + 13 >= 0 /\ 0 >= g''''''''''''''' + 1 /\ h + 15 >= 1 ] (1, 15) f4(a) -> f2(h + 15) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ g'''''''''''' >= 1 /\ h + 12 >= 1 /\ h + 11 >= 0 /\ g''''''''''''' >= 1 /\ h + 13 >= 1 /\ h + 12 >= 0 /\ 0 >= g'''''''''''''' + 1 /\ h + 14 >= 1 ] (1, 14) f4(a) -> f2(h + 14) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ g'''''''''''' >= 1 /\ h + 12 >= 1 /\ h + 11 >= 0 /\ 0 >= g''''''''''''' + 1 /\ h + 13 >= 1 ] (1, 13) f4(a) -> f2(h + 13) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ g''''''''''' >= 1 /\ h + 11 >= 1 /\ h + 10 >= 0 /\ 0 >= g'''''''''''' + 1 /\ h + 12 >= 1 ] (1, 12) f4(a) -> f2(h + 12) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ g'''''''''' >= 1 /\ h + 10 >= 1 /\ h + 9 >= 0 /\ 0 >= g''''''''''' + 1 /\ h + 11 >= 1 ] (1, 11) f4(a) -> f2(h + 11) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ g''''''''' >= 1 /\ h + 9 >= 1 /\ h + 8 >= 0 /\ 0 >= g'''''''''' + 1 /\ h + 10 >= 1 ] (1, 10) f4(a) -> f2(h + 10) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ g'''''''' >= 1 /\ h + 8 >= 1 /\ h + 7 >= 0 /\ 0 >= g''''''''' + 1 /\ h + 9 >= 1 ] (1, 9) f4(a) -> f2(h + 9) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ g''''''' >= 1 /\ h + 7 >= 1 /\ h + 6 >= 0 /\ 0 >= g'''''''' + 1 /\ h + 8 >= 1 ] (1, 8) f4(a) -> f2(h + 8) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ g'''''' >= 1 /\ h + 6 >= 1 /\ h + 5 >= 0 /\ 0 >= g''''''' + 1 /\ h + 7 >= 1 ] (1, 7) f4(a) -> f2(h + 7) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ g''''' >= 1 /\ h + 5 >= 1 /\ h + 4 >= 0 /\ 0 >= g'''''' + 1 /\ h + 6 >= 1 ] (1, 6) f4(a) -> f2(h + 6) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ g'''' >= 1 /\ h + 4 >= 1 /\ h + 3 >= 0 /\ 0 >= g''''' + 1 /\ h + 5 >= 1 ] (1, 5) f4(a) -> f2(h + 5) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ g''' >= 1 /\ h + 3 >= 1 /\ h + 2 >= 0 /\ 0 >= g'''' + 1 /\ h + 4 >= 1 ] (1, 4) f4(a) -> f2(h + 4) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ g'' >= 1 /\ h + 2 >= 1 /\ h + 1 >= 0 /\ 0 >= g''' + 1 /\ h + 3 >= 1 ] (1, 3) f4(a) -> f2(h + 3) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ g' >= 1 /\ h + 1 >= 1 /\ h >= 0 /\ 0 >= g'' + 1 /\ h + 2 >= 1 ] (1, 2) f4(a) -> f2(h + 2) [ 0 >= g + 1 /\ h >= 1 /\ h - 1 >= 0 /\ 0 >= g' + 1 /\ h + 1 >= 1 ] (1, 1) f4(a) -> f2(h + 1) [ g >= 1 /\ h >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ 0 >= g + 1 /\ a >= 1 ] (?, 1) f2(a) -> f2(a + 1) [ a - 2 >= 0 /\ g >= 1 /\ a >= 1 ] start location: f4 leaf cost: 3 Complexity upper bound ? Time: 1.326 sec (SMT: 1.089 sec)