(r_init s_init , not expab and not ab,
z >= 2 * t1 + t1 * n26 + synch and x >= synch and x - z <= - 2 * t1 - t1 * n26, rc = 1 + n25, (eps),(eps), - t1 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n25 = -1 and
- t2 <= 0 and
- n25 <= 0 and
- n25 + n26 = 0 and
- n26 <= 0 ->
z >= synch and x >= synch and x - z <= 0, rc = 1 + n3, (eps),(eps), - t1 = 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n3 = -1 and
- t2 <= 0 and
- n3 <= 0 and
- n3 + n4 = 0 and
- n4 <= 0 ->
z >= 0 and x >= 0 and z - x <= 0 and x - z <= 0, rc = 0, (eps),(eps), - t1 <= 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- t2 <= 0
)
(r_init s_init , expab and not ab,
z >= synch + t2 and x >= synch and z - x < t1 + t2 and x - z <= - t2, rc = 2, (eps),(eps), - 5 * t1 - t1 * n7 + t2 < 0 and
- t1 < 0 and
- t1 - synch < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= t2 and x > - t1 + t2 and z - x < t1 and x - z <= 0, rc = 0, (eps),(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= t2 and x > - 2 * t1 + t2 and z - x < 2 * t1 and x - z <= 0, rc = 1, (eps),(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= 2 * t1 + t1 * n10 + synch and x >= synch and z - x <= 3 * t1 + t1 * n10 and x - z <= - 2 * t1 - t1 * n10, rc = 2 + n9, (eps),(eps), - 3 * t1 - t1 * n10 - synch + t2 < 0 and
- 2 * t1 - t1 * n10 - synch + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 = -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 ->
z >= t2 and x > - t1 + t2 and z - x < t1 and x - z <= 0, rc = 1 + n14, (eps),(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 ->
z >= 2 * t1 + t1 * n21 + synch and x >= synch and z - x <= t2 and x - z <= - 2 * t1 - t1 * n21, rc = 1 + n20, (eps),(eps), - 2 * t1 - t1 * n21 - synch + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 + t1 * n21 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 + t1 * n21 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
t1 * n21 - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- max + n20 = -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 and
- n20 <= 0 and
- n20 + n21 = 0 and
- n21 <= 0 ->
z >= synch + t2 and x >= synch and z - x <= t1 + t2 and x - z <= - t2, rc = 1 + n20, (eps),(eps), - t1 < 0 and
- t1 - synch < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 + t1 * n21 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 + t1 * n21 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
t1 * n21 - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- max + n20 = -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 and
- n20 <= 0 and
- n20 + n21 = 0 and
- n21 <= 0 ->
z >= t1 + synch + t2 and x >= synch and z - x <= 2 * t1 + t2 and x - z <= - t1 - t2, rc = 2 + n20, (eps),(eps), - t1 < 0 and
- t1 - synch < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 + t1 * n21 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 + t1 * n21 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
t1 * n21 - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- max + n20 = -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 and
- n20 <= 0 and
- n20 + n21 = 0 and
- n21 <= 0 ->
z >= 2 * t1 + t1 * n19 + synch + t2 and x >= synch and z - x <= 3 * t1 + t1 * n19 + t2 and x - z <= - 2 * t1 - t1 * n19 - t2, rc = 2 + n18, (eps),(eps), - t1 < 0 and
- t1 - synch < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- max + n18 = -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 and
- n18 <= 0 and
- n18 + n19 = 0 and
- n19 <= 0 ->
z >= t2 and x > - 2 * t1 + t2 and z - x < 2 * t1 and x - z <= 0, rc = 2 + n14, (eps),(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 ->
z >= t2 and x > - 3 * t1 - t1 * n10 + t2 and z - x < 3 * t1 + t1 * n10 and x - z <= - t1 - t1 * n10, rc = 2 + n9, (eps),(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 ->
z >= synch and x >= synch and z - x <= t1 and x - z <= 0, rc = 1 + n0, (eps),(eps), - t1 = 0 and
- t1 - synch + t2 < 0 and
t1 - t2 < 0 and
2 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n0 = -1 and
- t2 < 0 and
- n0 <= 0
)
(r_init s_fst , not expab and not ab,
z >= t1 + t1 * n26 and x >= 0 and x <= t1 and x - z <= - t1 - t1 * n26, rc = 1 + n25, (fst0)*,(eps), - t1 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n25 <= -1 and
- t2 <= 0 and
- n25 <= 0 and
- n25 + n26 = 0 and
- n26 <= 0 ->
z >= 0 and x >= 0 and x <= t1 and x - z <= 0, rc = 0, (fst0+eps),(eps), - t1 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- t2 <= 0 ->
z >= 0 and x >= 0 and x <= t1 and x - z <= 0, rc = 1 + n3, (fst0)*,(eps), - t1 = 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n3 <= -1 and
- t2 <= 0 and
- n3 <= 0 and
- n3 + n4 = 0 and
- n4 <= 0 ->
z >= 0 and x >= 0 and x <= t1 and x - z <= 0, rc = 0, (fst0+eps),(eps), - t1 = 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- t2 <= 0
)
(r_init s_fst , expab and not ab,
z >= t2 and x >= 0 and z <= 2 * t1 + t2 and z - x <= t1 + t2 and x <= t1 and x - z <= - t2, rc = 2 + n20, (fst0+eps),(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 + t1 * n21 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 + t1 * n21 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
t1 * n21 - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- max + n20 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 and
- n20 <= 0 and
- n20 + n21 = 0 and
- n21 <= 0 ->
z >= t2 and x >= 0 and z <= t1 + t2 and z - x <= t2 and x <= t1 and x - z <= t1 - t2, rc = 1 + n20, (eps),(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 + t1 * n21 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 + t1 * n21 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
t1 * n21 - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- max + n20 <= -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 and
- n20 <= 0 and
- n20 + n21 = 0 and
- n21 <= 0 ->
z >= t1 + t1 * n19 + t2 and x >= 0 and z <= 3 * t1 + t1 * n19 + t2 and z - x <= 2 * t1 + t1 * n19 + t2 and x <= t1 and x - z <= - t1 - t1 * n19 - t2, rc = 2 + n18, (fst0)*,(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- max + n18 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 and
- n18 <= 0 and
- n18 + n19 = 0 and
- n19 <= 0 ->
z >= t2 and x >= 0 and z <= 2 * t1 + t2 and z - x <= t1 + t2 and x <= t1 and x - z <= - t2, rc = 1, (fst0+eps),(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 ->
z >= t2 and x >= 0 and z <= t1 + t2 and z - x <= t2 and x <= t1 and x - z <= t1 - t2, rc = 0, (eps),(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 ->
z >= t1 + t1 * n12 + t2 and x >= 0 and x <= t1 and x - z <= - t1 - t1 * n12 - t2, rc = 1 + n11, (fst0)*,(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 ->
z >= t2 and x >= 0 and x <= t1 and x - z <= - t2, rc = 0, (fst0+eps),(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 ->
z >= synch and x >= 0 and x <= t1 and x - z <= - synch, rc = 1 + n1, (fst0)*,(eps), - t1 = 0 and
- t1 - synch + t2 < 0 and
t1 - t2 < 0 and
2 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n0 = -1 and
- max + n1 <= -1 and
- t2 < 0 and
- n0 <= 0 and
- n1 <= 0 and
- n1 + n2 = 0 and
- n2 <= 0 ->
z >= synch and x >= 0 and x <= t1 and x - z <= - synch, rc = 0, (fst0+eps),(eps), - t1 = 0 and
- t1 - synch + t2 < 0 and
t1 - t2 < 0 and
2 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n0 = -1 and
- t2 < 0 and
- n0 <= 0
)
(r_init s_success , expab and ab,
z >= t2 and x > 0 and z < t1 + t2 and z - x < t2 and x <= t1 and x - z <= t1 - t2, rc = 2, (eps),(eps), - 5 * t1 - t1 * n7 + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= t2 and x >= 0 and z < 6 * t1 + t1 * n7 and z - x < 5 * t1 + t1 * n7 and x <= t1 and x - z <= - t2, rc = 2, (last1+eps),(eps), - 5 * t1 - t1 * n7 + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= t2 and x > - 4 * t1 - t1 * n7 + t2 and z < 5 * t1 + t1 * n7 and z - x < 4 * t1 + t1 * n7 and x <= t1 and x - z <= t1 - t2, rc = 1, (eps),(eps), - 5 * t1 - t1 * n7 + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= t2 and x > - 5 * t1 - t1 * n7 + t2 and z < 6 * t1 + t1 * n7 and z - x < 5 * t1 + t1 * n7 and x <= t1 and x - z <= t1 - t2, rc = 2, (eps),(eps), - 6 * t1 - t1 * n7 + t2 < 0 and
- 5 * t1 - t1 * n7 + t2 = 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= t2 and x >= 0 and z <= t1 + t2 and z - x <= t2 and x <= t1 and x - z <= t1 - t2, rc = 2, (eps),(eps), - 5 * t1 - t1 * n7 + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0
)
(r_init s_error , not expab and not ab,
z >= 2 * t1 + t1 * n26 and x >= 0 and x <= synch and x - z <= - 2 * t1 - t1 * n26, rc = 1 + n25, (eps),(eps), - t1 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n25 = -1 and
- t2 <= 0 and
- n25 <= 0 and
- n25 + n26 = 0 and
- n26 <= 0 ->
z >= 0 and x >= 0 and x <= synch and x - z <= 0, rc = 1 + n3, (eps),(eps), - t1 = 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n3 = -1 and
- t2 <= 0 and
- n3 <= 0 and
- n3 + n4 = 0 and
- n4 <= 0
)
(r_init s_error , expab and not ab,
z >= t2 and x >= - 3 * t1 - t1 * n7 + t2 and z <= 3 * t1 + t1 * n7 + synch and z - x <= 3 * t1 + t1 * n7 and x <= synch and x - z <= - 2 * t1 - t1 * n7, rc = 2 + n6, (eps),(eps), - 3 * t1 - t1 * n7 - synch + t2 < 0 and
- 2 * t1 - t1 * n7 - synch + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 = -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= t2 and x >= - t1 + t2 and z <= t1 + synch and z - x <= t1 and x <= synch and x - z <= 0, rc = 1 + n11, (eps),(eps), - t1 < 0 and
- t1 - synch + t2 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 = -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 ->
z >= t2 and x >= - 2 * t1 + t2 and z <= 2 * t1 + synch and z - x <= 2 * t1 and x <= synch and x - z <= - t1, rc = 2 + n11, (eps),(eps), - 2 * t1 - synch + t2 < 0 and
- t1 < 0 and
- t1 - synch + t2 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 = -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 ->
z >= t2 and x >= 0 and z <= synch + t2 and z - x <= t2 and x <= synch and x - z <= - 2 * t1 - t1 * n21, rc = 1 + n20, (eps),(eps), - 2 * t1 - t1 * n21 - synch + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 + t1 * n21 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 + t1 * n21 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
t1 * n21 - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- max + n20 = -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 and
- n20 <= 0 and
- n20 + n21 = 0 and
- n21 <= 0 ->
z >= t2 and x >= 0 and z <= t1 + synch + t2 and z - x <= t1 + t2 and x <= synch and x - z <= - t2, rc = 1 + n20, (eps),(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 + t1 * n21 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 + t1 * n21 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
t1 * n21 - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- max + n20 = -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 and
- n20 <= 0 and
- n20 + n21 = 0 and
- n21 <= 0 ->
z >= t1 + t2 and x >= 0 and z <= 2 * t1 + synch + t2 and z - x <= 2 * t1 + t2 and x <= synch and x - z <= - t1 - t2, rc = 2 + n20, (eps),(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 + t1 * n21 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 + t1 * n21 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
t1 * n21 - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- max + n20 = -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 and
- n20 <= 0 and
- n20 + n21 = 0 and
- n21 <= 0 ->
z >= 2 * t1 + t1 * n19 + t2 and x >= 0 and z <= 3 * t1 + t1 * n19 + synch + t2 and z - x <= 3 * t1 + t1 * n19 + t2 and x <= synch and x - z <= - 2 * t1 - t1 * n19 - t2, rc = 2 + n18, (eps),(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- max + n18 = -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 and
- n18 <= 0 and
- n18 + n19 = 0 and
- n19 <= 0 ->
z >= synch and x >= 0 and x <= synch and x - z <= - synch, rc = 1 + n1, (eps),(eps), - t1 = 0 and
- t1 - synch + t2 < 0 and
t1 - t2 < 0 and
2 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n0 = -1 and
- max + n1 = -1 and
- t2 < 0 and
- n0 <= 0 and
- n1 <= 0 and
- n1 + n2 = 0 and
- n2 <= 0 ->
z >= t2 and x >= - t1 + t2 and z <= t1 + synch and z - x <= t1 and x <= synch and x - z <= 0, rc = 1 + n0, (eps),(eps), - t1 = 0 and
- t1 - synch + t2 < 0 and
t1 - t2 < 0 and
2 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n0 = -1 and
- t2 < 0 and
- n0 <= 0
)
(r_init s_error , expab and ab,
z >= t2 and x >= - t1 + t2 and z <= t1 + synch and z - x <= t1 and x <= synch and x - z <= 0, rc = 2, (eps),(eps), - 5 * t1 - t1 * n7 + t2 < 0 and
- t1 < 0 and
- t1 - synch + t2 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= t2 and x >= 0 and z < t1 + synch + t2 and z - x < t1 + t2 and x <= synch and x - z <= - t2, rc = 2, (eps),(eps), - 5 * t1 - t1 * n7 + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= t1 + t2 and x >= 0 and z < 6 * t1 + t1 * n7 + synch and z - x < 6 * t1 + t1 * n7 and x <= synch and x - z <= - t1 - t2, rc = 2, (eps),(eps), - 6 * t1 - t1 * n7 + t2 < 0 and
- 5 * t1 - t1 * n7 + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= t2 and x >= 0 and z <= synch + t2 and z - x <= t2 and x <= synch and x - z <= - 4 * t1 - t1 * n7, rc = 2, (eps),(eps), - 6 * t1 - t1 * n7 + t2 < 0 and
- 5 * t1 - t1 * n7 + t2 = 0 and
- 4 * t1 - t1 * n7 - synch + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= t2 and x >= 0 and z < 6 * t1 + t1 * n7 + synch and z - x < 6 * t1 + t1 * n7 and x <= synch and x - z <= - t2, rc = 2, (eps),(eps), - 6 * t1 - t1 * n7 + t2 < 0 and
- 5 * t1 - t1 * n7 + t2 = 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= t2 and x >= - 3 * t1 - t1 * n10 + t2 and z <= 3 * t1 + t1 * n10 + synch and z - x <= 3 * t1 + t1 * n10 and x <= synch and x - z <= - 2 * t1 - t1 * n10, rc = 2 + n9, (eps),(eps), - 3 * t1 - t1 * n10 - synch + t2 < 0 and
- 2 * t1 - t1 * n10 - synch + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 = -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 ->
z >= t2 and x >= 0 and z <= synch + t2 and z - x <= t2 and x <= synch and x - z <= - 2 * t1 - t1 * n15, rc = 1 + n14, (eps),(eps), - 4 * t1 - t1 * n15 + t2 < 0 and
- 2 * t1 - t1 * n15 - synch + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 ->
z >= t2 and x >= 0 and z <= t1 + synch + t2 and z - x <= t1 + t2 and x <= synch and x - z <= - t2, rc = 2, (eps),(eps), - 5 * t1 - t1 * n7 + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= t2 and x > - 4 * t1 - t1 * n15 + t2 and z < 4 * t1 + t1 * n15 + synch and z - x < 4 * t1 + t1 * n15 and x <= synch and x - z <= - 2 * t1 - t1 * n15, rc = 1 + n14, (eps),(eps), - 4 * t1 - t1 * n15 - synch + t2 < 0 and
- 2 * t1 - t1 * n15 - synch + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 = -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 ->
z >= t2 and x > - 5 * t1 - t1 * n15 + t2 and z < 5 * t1 + t1 * n15 + synch and z - x < 5 * t1 + t1 * n15 and x <= synch and x - z <= - 3 * t1 - t1 * n15, rc = 2 + n14, (eps),(eps), - 5 * t1 - t1 * n15 - synch + t2 < 0 and
- 5 * t1 - t1 * n15 + t2 = 0 and
- 3 * t1 - t1 * n15 - synch + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 ->
z >= t2 and x >= - t1 + t2 and z <= t1 + synch and z - x <= t1 and x <= synch and x - z <= 0, rc = 2 + n14, (eps),(eps), - t1 < 0 and
- t1 - synch + t2 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
5 * t1 + t1 * n15 - t2 = 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 ->
z >= t2 and x >= - t1 + t2 and z <= t1 + synch and z - x <= t1 and x <= synch and x - z <= 0, rc = 1 + n14, (eps),(eps), - t1 < 0 and
- t1 - synch + t2 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 = -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 ->
z >= t2 and x >= - 2 * t1 + t2 and z <= 2 * t1 + synch and z - x <= 2 * t1 and x <= synch and x - z <= - t1, rc = 2 + n14, (eps),(eps), - 2 * t1 - synch + t2 < 0 and
- t1 < 0 and
- t1 - synch + t2 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 = -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0
)
(r_wait_next s_fst , expab and not ab,
z >= 0 and x >= 0 and z <= 2 * t1 and z - x <= t1 and x <= t1 and x - z <= 0, rc = 2 + n11, (fst0)*,(ack0)*, - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 ->
z >= 0 and x >= 0 and z <= t1 and z - x <= 0 and x <= t1 and x - z <= t1, rc = 1 + n11, (fst0)*,(ack0)*, - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 ->
z >= t1 + t1 * n7 and x >= 0 and z <= 3 * t1 + t1 * n7 and z - x <= 2 * t1 + t1 * n7 and x <= t1 and x - z <= - t1 - t1 * n7, rc = 2 + n6, (fst0)*,(ack0)*, - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= 0 and x >= 0 and z <= 2 * t1 and z - x <= t1 and x <= t1 and x - z <= 0, rc = 1, (eps),(ack0+eps)(ack0+eps), - t1 < 0 and
t1 - t2 < 0 and
2 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- t2 < 0 ->
z >= 0 and x >= 0 and z <= 2 * t1 and z - x <= t1 and x <= t1 and x - z <= 0, rc = 1, (fst0+eps),(ack0+eps), - t1 < 0 and
t1 - t2 < 0 and
2 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- t2 < 0 ->
z >= 0 and x >= 0 and z <= t1 and z - x <= 0 and x <= t1 and x - z <= t1, rc = 0, (eps),(ack0+eps), - t1 < 0 and
t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- t2 < 0 ->
z >= 0 and x >= 0 and z <= t1 and z - x <= 0 and x <= t1 and x - z <= t1, rc = 1 + n0, (fst0)*,(ack0)*, - t1 = 0 and
t1 - t2 < 0 and
2 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n0 <= -1 and
- t2 < 0 and
- n0 <= 0 ->
z >= 0 and x >= 0 and z <= t1 and z - x <= 0 and x <= t1 and x - z <= t1, rc = 0, (eps),(ack0+eps), - t1 = 0 and
t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- t2 < 0
)
(r_wait_next s_success , expab and ab,
z >= 3 * t1 + t1 * n7 and x >= 0 and z <= t2 and z - x < t2 and x <= t1 and x - z <= - 3 * t1 - t1 * n7, rc = 2, (fst0)*(last1+eps)(last1+eps)(last1+eps),(ack0)*, - 5 * t1 - t1 * n7 + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= 3 * t1 + t1 * n7 and x >= 0 and z <= t2 and z - x <= t2 and x <= t1 and x - z <= - 3 * t1 - t1 * n7, rc = 2, (fst0)*(last1+eps)(last1+eps)(last1+eps),(ack0)*, - 5 * t1 - t1 * n7 + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= 2 * t1 + t1 * n7 and x >= 0 and z <= t2 and z - x < 4 * t1 + t1 * n7 and x <= t1 and x - z <= - 2 * t1 - t1 * n7, rc = 1, (fst0)*(last1+eps)(last1+eps),(ack0)*, - 5 * t1 - t1 * n7 + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= 3 * t1 + t1 * n7 and x >= 0 and z <= t2 and z - x < 5 * t1 + t1 * n7 and x <= t1 and x - z <= - 3 * t1 - t1 * n7, rc = 2, (fst0)*(last1+eps)(last1+eps)(last1+eps),(ack0)*, - 6 * t1 - t1 * n7 + t2 < 0 and
- 5 * t1 - t1 * n7 + t2 = 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= 2 * t1 + t1 * n7 and x >= 0 and z < 5 * t1 + t1 * n7 and z - x < 4 * t1 + t1 * n7 and x <= t1 and x - z <= - 2 * t1 - t1 * n7, rc = 1, (fst0)*(last1+eps)(last1+eps),(ack0)*, - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
5 * t1 + t1 * n7 - t2 = 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= 2 * t1 + t1 * n15 and x >= 0 and z < 5 * t1 + t1 * n15 and z - x < 4 * t1 + t1 * n15 and x <= t1 and x - z <= - 2 * t1 - t1 * n15, rc = 2 + n14, (fst0)*(last1)*,(ack0)*, - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
5 * t1 + t1 * n15 - t2 = 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 ->
z >= t1 + t1 * n15 and x >= 0 and z <= t2 and z - x < 3 * t1 + t1 * n15 and x <= t1 and x - z <= - t1 - t1 * n15, rc = 1 + n14, (fst0)*(last1)*,(ack0)*, - 4 * t1 - t1 * n15 + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 ->
z >= t1 + t1 * n15 and x >= 0 and z < 4 * t1 + t1 * n15 and z - x < 3 * t1 + t1 * n15 and x <= t1 and x - z <= - t1 - t1 * n15, rc = 1 + n14, (fst0)*(last1)*,(ack0)*, - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 ->
z >= 0 and x >= 0 and z < 3 * t1 and z - x < 2 * t1 and x <= t1 and x - z <= 0, rc = 0, (fst0)*(last1+eps),(ack0)*, - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 ->
z >= t1 + t1 * n7 and x >= 0 and z < 4 * t1 + t1 * n7 and z - x < 3 * t1 + t1 * n7 and x <= t1 and x - z <= - t1 - t1 * n7, rc = 0, (fst0)*(last1+eps),(ack0)*, - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0
)
(r_wait_next s_error , expab and not ab,
z >= 2 * t1 + t1 * n7 and x >= 0 and z <= t2 and z - x <= 3 * t1 + t1 * n7 and x <= - 2 * t1 - t1 * n7 + t2 and x - z <= - 2 * t1 - t1 * n7, rc = 2 + n6, (eps),(eps), - 2 * t1 - t1 * n7 - synch + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 = -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= 0 and x >= 0 and z <= t2 and z - x <= t1 and x <= t2 and x - z <= 0, rc = 1 + n11, (eps),(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 = -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 ->
z >= t1 and x >= 0 and z <= t2 and z - x <= 2 * t1 and x <= - t1 + t2 and x - z <= - t1, rc = 2 + n11, (eps),(eps), - t1 < 0 and
- t1 - synch + t2 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 = -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 ->
z >= 0 and x >= 0 and z <= t2 and z - x <= t1 and x <= t2 and x - z <= 0, rc = 1 + n0, (eps),(eps), - t1 = 0 and
t1 - t2 < 0 and
2 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n0 = -1 and
- t2 < 0 and
- n0 <= 0
)
(r_wait_next s_error , expab and ab,
z >= 4 * t1 + t1 * n7 and x >= 0 and z <= t2 and z - x <= t2 and x <= - 4 * t1 - t1 * n7 + t2 and x - z <= - 4 * t1 - t1 * n7, rc = 2, (eps),(ack0)*, - 6 * t1 - t1 * n7 + t2 < 0 and
- 5 * t1 - t1 * n7 + t2 = 0 and
- 4 * t1 - t1 * n7 - synch + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= 2 * t1 + t1 * n15 and x >= 0 and z <= t2 and z - x <= t2 and x <= - 2 * t1 - t1 * n15 + t2 and x - z <= - 2 * t1 - t1 * n15, rc = 1 + n14, (eps),(ack0)*, - 4 * t1 - t1 * n15 + t2 < 0 and
- 2 * t1 - t1 * n15 - synch + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 ->
z >= 2 * t1 + t1 * n15 and x >= 0 and z <= t2 and z - x < 4 * t1 + t1 * n15 and x <= - 2 * t1 - t1 * n15 + t2 and x - z <= - 2 * t1 - t1 * n15, rc = 1 + n14, (eps),(ack0)*, - 2 * t1 - t1 * n15 - synch + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 = -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 ->
z >= 3 * t1 + t1 * n15 and x >= 0 and z <= t2 and z - x < 5 * t1 + t1 * n15 and x <= - 3 * t1 - t1 * n15 + t2 and x - z <= - 3 * t1 - t1 * n15, rc = 2 + n14, (eps),(ack0)*, - 5 * t1 - t1 * n15 + t2 = 0 and
- 3 * t1 - t1 * n15 - synch + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0
)
(r_ok s_init , expab and not ab,
z >= 0 and x >= 0 and z <= t2 and z - x < t1 and x <= t2 and x - z <= 0, rc = 0, (eps),(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= 0 and x >= 0 and z <= t2 and z - x < 2 * t1 and x <= t2 and x - z <= 0, rc = 1, (eps),(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= 0 and x >= 0 and z <= t2 and z - x < t1 and x <= t2 and x - z <= 0, rc = 1 + n14, (eps),(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 ->
z >= 0 and x >= 0 and z <= t2 and z - x < 2 * t1 and x <= t2 and x - z <= 0, rc = 2 + n14, (eps),(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 ->
z >= t1 + t1 * n10 and x >= 0 and z <= t2 and z - x < 3 * t1 + t1 * n10 and x <= - t1 - t1 * n10 + t2 and x - z <= - t1 - t1 * n10, rc = 2 + n9, (eps),(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0
)
(r_ok s_fst , expab and not ab,
z >= t1 + t1 * n21 and x >= 0 and z <= t2 and z - x <= t2 and x <= t1 and x - z <= - t1 - t1 * n21, rc = 1 + n20, (fst0)*,(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 + t1 * n21 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 + t1 * n21 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
t1 * n21 - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- max + n20 <= -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 and
- n20 <= 0 and
- n20 + n21 = 0 and
- n21 <= 0 ->
z >= 0 and x >= 0 and z <= t2 and z - x <= t2 and x <= t1 and x - z <= 0, rc = 0, (fst0+eps),(eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0
)
(r_ok s_success , expab and ab,
z >= 0 and x >= 0 and z <= t1 and z - x <= 0 and x <= t1 and x - z <= t1, rc = 2, (eps),(ack0)*(ack1+eps)(ack1+eps)(ack1+eps), - 5 * t1 - t1 * n7 + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= 0 and x >= 0 and z <= t1 and z - x <= 0 and x <= t1 and x - z <= t1, rc = 2, (last1+eps),(ack0)*(ack1+eps)(ack1+eps), - 5 * t1 - t1 * n7 + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= 0 and x >= 0 and z <= t1 and z - x <= 0 and x <= t1 and x - z <= t1, rc = 2, (last1+eps)(last1+eps),(ack0)*(ack1+eps), - 5 * t1 - t1 * n7 + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= 0 and x >= 0 and z <= t1 and z - x <= 0 and x <= t1 and x - z <= t1, rc = 2 + n14, (last1)*,(ack0)*(ack1)*, - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
5 * t1 + t1 * n15 - t2 = 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 ->
z >= 0 and x >= 0 and z <= 2 * t1 and z - x <= t1 and x <= t1 and x - z <= 0, rc = 2 + n14, (last1)*,(ack0)*(ack1)*, - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 ->
z >= 0 and x >= 0 and z <= t1 and z - x <= 0 and x <= t1 and x - z <= t1, rc = 1 + n14, (last1)*,(ack0)*(ack1)*, - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 ->
z >= t1 + t1 * n10 and x >= 0 and z <= 3 * t1 + t1 * n10 and z - x <= 2 * t1 + t1 * n10 and x <= t1 and x - z <= - t1 - t1 * n10, rc = 2 + n9, (last1)*,(ack0)*(ack1)*, - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 ->
z >= 0 and x >= 0 and z <= 2 * t1 and z - x <= t1 and x <= t1 and x - z <= 0, rc = 1, (eps),(ack0)*(ack1+eps)(ack1+eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= 0 and x >= 0 and z <= 2 * t1 and z - x <= t1 and x <= t1 and x - z <= 0, rc = 1, (last1+eps),(ack0)*(ack1+eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= 0 and x >= 0 and z <= t1 and z - x <= 0 and x <= t1 and x - z <= t1, rc = 0, (eps),(ack0)*(ack1+eps), - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0
)
(r_ok s_error , expab and not ab,
z >= 2 * t1 + t1 * n21 and x >= 0 and z <= t2 and z - x <= t2 and x <= - 2 * t1 - t1 * n21 + t2 and x - z <= - 2 * t1 - t1 * n21, rc = 1 + n20, (eps),(eps), - 2 * t1 - t1 * n21 - synch + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 + t1 * n21 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 + t1 * n21 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
t1 * n21 - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- max + n20 = -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 and
- n20 <= 0 and
- n20 + n21 = 0 and
- n21 <= 0
)
(r_ok s_error , expab and ab,
z >= 0 and x >= 0 and z <= t2 and z - x <= t1 and x <= t2 and x - z <= 0, rc = 2, (eps),(ack0)*(ack1+eps)(ack1+eps)(ack1+eps), - 5 * t1 - t1 * n7 + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 ->
z >= 2 * t1 + t1 * n10 and x >= 0 and z <= t2 and z - x <= 3 * t1 + t1 * n10 and x <= - 2 * t1 - t1 * n10 + t2 and x - z <= - 2 * t1 - t1 * n10, rc = 2 + n9, (eps),(ack0)*(ack1)*, - 2 * t1 - t1 * n10 - synch + t2 < 0 and
- t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 = -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 ->
z >= 0 and x >= 0 and z <= t2 and z - x <= t1 and x <= t2 and x - z <= 0, rc = 2 + n14, (eps),(ack0)*(ack1)*, - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
5 * t1 + t1 * n15 - t2 = 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 <= -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 ->
z >= 0 and x >= 0 and z <= t2 and z - x <= t1 and x <= t2 and x - z <= 0, rc = 1 + n14, (eps),(ack0)*(ack1)*, - t1 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 = -1 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0 ->
z >= t1 and x >= 0 and z <= t2 and z - x <= 2 * t1 and x <= - t1 + t2 and x - z <= - t1, rc = 2 + n14, (eps),(ack0)*(ack1)*, - t1 < 0 and
- t1 - synch + t2 < 0 and
t1 + t1 * n7 - t2 < 0 and
t1 + t1 * n10 - t2 < 0 and
t1 + t1 * n15 - t2 < 0 and
t1 - t2 < 0 and
2 * t1 + t1 * n7 - t2 < 0 and
2 * t1 + t1 * n10 - t2 < 0 and
2 * t1 + t1 * n15 - t2 < 0 and
2 * t1 - t2 < 0 and
3 * t1 + t1 * n7 - t2 < 0 and
3 * t1 + t1 * n10 - t2 < 0 and
3 * t1 + t1 * n15 - t2 < 0 and
3 * t1 - t2 < 0 and
4 * t1 + t1 * n7 - t2 < 0 and
4 * t1 + t1 * n15 - t2 < 0 and
4 * t1 - t2 < 0 and
2 * t1 * max - t2 < 0 and
- synch < 0 and
- synch + t2 < 0 and
- max <= -2 and
- max + n6 <= -2 and
- max + n9 <= -2 and
- max + n11 <= -2 and
- max + n14 = -2 and
- t2 < 0 and
- n6 <= 0 and
- n6 + n7 = 0 and
- n7 <= 0 and
- n9 <= 0 and
- n9 + n10 = 0 and
- n10 <= 0 and
- n11 <= 0 and
- n11 + n12 = 0 and
- n12 <= 0 and
- n14 <= 0 and
- n14 + n15 = 0 and
- n15 <= 0
)
Temps d'execution : 5026.78 s.
corespondance avec le graphe :
[ 0 -- ( r_init s_init , not expab and not ab, 0)]
[ 1 -- ( r_init s_fst , not expab and not ab, 0)]
[ 2 -- ( r_wait_next s_fst , expab and not ab, 0)]
[ 3 -- ( r_wait_next s_error , expab and not ab, 0)]
[ 4 -- ( r_init s_error , expab and not ab, 0)]
[ 5 -- ( r_init s_init , expab and not ab, 0)]
[ 6 -- ( r_init s_fst , expab and not ab, 0)]
[ 7 -- ( r_init s_error , not expab and not ab, 0)]
[ 8 -- ( r_wait_next s_success , expab and ab, 0)]
[ 9 -- ( r_ok s_success , expab and ab, 0)]
[ 10 -- ( r_ok s_init , expab and not ab, 0)]
[ 11 -- ( r_ok s_error , expab and ab, 0)]
[ 12 -- ( r_ok s_fst , expab and not ab, 0)]
[ 13 -- ( r_wait_next s_error , expab and ab, 0)]
[ 14 -- ( r_ok s_error , expab and not ab, 0)]
[ 15 -- ( r_init s_error , expab and ab, 0)]
[ 16 -- ( r_init s_success , expab and ab, 0)]
child : 534.06
self : 5029.33
---------------
total : 5563.39
Memoire : 85080 80240