LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
0 54 0: − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − s_ab_post + s_ab_post ≤ 0 ∧ s_ab_post − s_ab_post ≤ 0 ∧ − s_ab_0 + s_ab_0 ≤ 0 ∧ s_ab_0 − s_ab_0 ≤ 0 ∧ − rrep_post + rrep_post ≤ 0 ∧ rrep_post − rrep_post ≤ 0 ∧ − rrep_0 + rrep_0 ≤ 0 ∧ rrep_0 − rrep_0 ≤ 0 ∧ − recv_post + recv_post ≤ 0 ∧ recv_post − recv_post ≤ 0 ∧ − recv_0 + recv_0 ≤ 0 ∧ recv_0 − recv_0 ≤ 0 ∧ − r_ab_post + r_ab_post ≤ 0 ∧ r_ab_post − r_ab_post ≤ 0 ∧ − r_ab_0 + r_ab_0 ≤ 0 ∧ r_ab_0 − r_ab_0 ≤ 0 ∧ − pos_post + pos_post ≤ 0 ∧ pos_post − pos_post ≤ 0 ∧ − pos_0 + pos_0 ≤ 0 ∧ pos_0 − pos_0 ≤ 0 ∧ − next_post + next_post ≤ 0 ∧ next_post − next_post ≤ 0 ∧ − next_0 + next_0 ≤ 0 ∧ next_0 − next_0 ≤ 0 ∧ − ls_post + ls_post ≤ 0 ∧ ls_post − ls_post ≤ 0 ∧ − ls_0 + ls_0 ≤ 0 ∧ ls_0 − ls_0 ≤ 0 ∧ − lr_post + lr_post ≤ 0 ∧ lr_post − lr_post ≤ 0 ∧ − lr_0 + lr_0 ≤ 0 ∧ lr_0 − lr_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − fs_post + fs_post ≤ 0 ∧ fs_post − fs_post ≤ 0 ∧ − fs_0 + fs_0 ≤ 0 ∧ fs_0 − fs_0 ≤ 0 ∧ − fr_post + fr_post ≤ 0 ∧ fr_post − fr_post ≤ 0 ∧ − fr_0 + fr_0 ≤ 0 ∧ fr_0 − fr_0 ≤ 0 ∧ − c2_0 + c2_0 ≤ 0 ∧ c2_0 − c2_0 ≤ 0 ∧ − c1_0 + c1_0 ≤ 0 ∧ c1_0 − c1_0 ≤ 0 ∧ − bs_post + bs_post ≤ 0 ∧ bs_post − bs_post ≤ 0 ∧ − bs_0 + bs_0 ≤ 0 ∧ bs_0 − bs_0 ≤ 0 ∧ − br_post + br_post ≤ 0 ∧ br_post − br_post ≤ 0 ∧ − br_0 + br_0 ≤ 0 ∧ br_0 − br_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0
3 61 3: − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − s_ab_post + s_ab_post ≤ 0 ∧ s_ab_post − s_ab_post ≤ 0 ∧ − s_ab_0 + s_ab_0 ≤ 0 ∧ s_ab_0 − s_ab_0 ≤ 0 ∧ − rrep_post + rrep_post ≤ 0 ∧ rrep_post − rrep_post ≤ 0 ∧ − rrep_0 + rrep_0 ≤ 0 ∧ rrep_0 − rrep_0 ≤ 0 ∧ − recv_post + recv_post ≤ 0 ∧ recv_post − recv_post ≤ 0 ∧ − recv_0 + recv_0 ≤ 0 ∧ recv_0 − recv_0 ≤ 0 ∧ − r_ab_post + r_ab_post ≤ 0 ∧ r_ab_post − r_ab_post ≤ 0 ∧ − r_ab_0 + r_ab_0 ≤ 0 ∧ r_ab_0 − r_ab_0 ≤ 0 ∧ − pos_post + pos_post ≤ 0 ∧ pos_post − pos_post ≤ 0 ∧ − pos_0 + pos_0 ≤ 0 ∧ pos_0 − pos_0 ≤ 0 ∧ − next_post + next_post ≤ 0 ∧ next_post − next_post ≤ 0 ∧ − next_0 + next_0 ≤ 0 ∧ next_0 − next_0 ≤ 0 ∧ − ls_post + ls_post ≤ 0 ∧ ls_post − ls_post ≤ 0 ∧ − ls_0 + ls_0 ≤ 0 ∧ ls_0 − ls_0 ≤ 0 ∧ − lr_post + lr_post ≤ 0 ∧ lr_post − lr_post ≤ 0 ∧ − lr_0 + lr_0 ≤ 0 ∧ lr_0 − lr_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − fs_post + fs_post ≤ 0 ∧ fs_post − fs_post ≤ 0 ∧ − fs_0 + fs_0 ≤ 0 ∧ fs_0 − fs_0 ≤ 0 ∧ − fr_post + fr_post ≤ 0 ∧ fr_post − fr_post ≤ 0 ∧ − fr_0 + fr_0 ≤ 0 ∧ fr_0 − fr_0 ≤ 0 ∧ − c2_0 + c2_0 ≤ 0 ∧ c2_0 − c2_0 ≤ 0 ∧ − c1_0 + c1_0 ≤ 0 ∧ c1_0 − c1_0 ≤ 0 ∧ − bs_post + bs_post ≤ 0 ∧ bs_post − bs_post ≤ 0 ∧ − bs_0 + bs_0 ≤ 0 ∧ bs_0 − bs_0 ≤ 0 ∧ − br_post + br_post ≤ 0 ∧ br_post − br_post ≤ 0 ∧ − br_0 + br_0 ≤ 0 ∧ br_0 − br_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0
and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 44, 51, 53 using the following ranking functions, which are bounded by −15.

30: 0
25: 0
0: 0
1: 0
2: 0
3: 0
4: 0
5: 0
6: 0
7: 0
8: 0
9: 0
10: 0
11: 0
12: 0
13: 0
14: 0
15: 0
16: 0
17: 0
18: 0
19: 0
20: 0
21: 0
22: 0
23: 0
24: 0
26: 0
27: 0
28: 0
29: 0
30: −5
25: −6
0: −7
1: −7
2: −7
3: −7
4: −7
5: −7
6: −7
7: −7
8: −7
9: −7
10: −7
11: −7
12: −7
13: −7
14: −7
15: −7
16: −7
17: −7
18: −7
19: −7
20: −7
21: −7
22: −7
23: −7
24: −7
26: −7
27: −7
28: −7
0_var_snapshot: −7
0*: −7
3_var_snapshot: −7
3*: −7
29: −10

3 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

0* 57 0: − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − s_ab_post + s_ab_post ≤ 0 ∧ s_ab_post − s_ab_post ≤ 0 ∧ − s_ab_0 + s_ab_0 ≤ 0 ∧ s_ab_0 − s_ab_0 ≤ 0 ∧ − rrep_post + rrep_post ≤ 0 ∧ rrep_post − rrep_post ≤ 0 ∧ − rrep_0 + rrep_0 ≤ 0 ∧ rrep_0 − rrep_0 ≤ 0 ∧ − recv_post + recv_post ≤ 0 ∧ recv_post − recv_post ≤ 0 ∧ − recv_0 + recv_0 ≤ 0 ∧ recv_0 − recv_0 ≤ 0 ∧ − r_ab_post + r_ab_post ≤ 0 ∧ r_ab_post − r_ab_post ≤ 0 ∧ − r_ab_0 + r_ab_0 ≤ 0 ∧ r_ab_0 − r_ab_0 ≤ 0 ∧ − pos_post + pos_post ≤ 0 ∧ pos_post − pos_post ≤ 0 ∧ − pos_0 + pos_0 ≤ 0 ∧ pos_0 − pos_0 ≤ 0 ∧ − next_post + next_post ≤ 0 ∧ next_post − next_post ≤ 0 ∧ − next_0 + next_0 ≤ 0 ∧ next_0 − next_0 ≤ 0 ∧ − ls_post + ls_post ≤ 0 ∧ ls_post − ls_post ≤ 0 ∧ − ls_0 + ls_0 ≤ 0 ∧ ls_0 − ls_0 ≤ 0 ∧ − lr_post + lr_post ≤ 0 ∧ lr_post − lr_post ≤ 0 ∧ − lr_0 + lr_0 ≤ 0 ∧ lr_0 − lr_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − fs_post + fs_post ≤ 0 ∧ fs_post − fs_post ≤ 0 ∧ − fs_0 + fs_0 ≤ 0 ∧ fs_0 − fs_0 ≤ 0 ∧ − fr_post + fr_post ≤ 0 ∧ fr_post − fr_post ≤ 0 ∧ − fr_0 + fr_0 ≤ 0 ∧ fr_0 − fr_0 ≤ 0 ∧ − c2_0 + c2_0 ≤ 0 ∧ c2_0 − c2_0 ≤ 0 ∧ − c1_0 + c1_0 ≤ 0 ∧ c1_0 − c1_0 ≤ 0 ∧ − bs_post + bs_post ≤ 0 ∧ bs_post − bs_post ≤ 0 ∧ − bs_0 + bs_0 ≤ 0 ∧ bs_0 − bs_0 ≤ 0 ∧ − br_post + br_post ≤ 0 ∧ br_post − br_post ≤ 0 ∧ − br_0 + br_0 ≤ 0 ∧ br_0 − br_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0

4 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

0 55 0_var_snapshot: − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − s_ab_post + s_ab_post ≤ 0 ∧ s_ab_post − s_ab_post ≤ 0 ∧ − s_ab_0 + s_ab_0 ≤ 0 ∧ s_ab_0 − s_ab_0 ≤ 0 ∧ − rrep_post + rrep_post ≤ 0 ∧ rrep_post − rrep_post ≤ 0 ∧ − rrep_0 + rrep_0 ≤ 0 ∧ rrep_0 − rrep_0 ≤ 0 ∧ − recv_post + recv_post ≤ 0 ∧ recv_post − recv_post ≤ 0 ∧ − recv_0 + recv_0 ≤ 0 ∧ recv_0 − recv_0 ≤ 0 ∧ − r_ab_post + r_ab_post ≤ 0 ∧ r_ab_post − r_ab_post ≤ 0 ∧ − r_ab_0 + r_ab_0 ≤ 0 ∧ r_ab_0 − r_ab_0 ≤ 0 ∧ − pos_post + pos_post ≤ 0 ∧ pos_post − pos_post ≤ 0 ∧ − pos_0 + pos_0 ≤ 0 ∧ pos_0 − pos_0 ≤ 0 ∧ − next_post + next_post ≤ 0 ∧ next_post − next_post ≤ 0 ∧ − next_0 + next_0 ≤ 0 ∧ next_0 − next_0 ≤ 0 ∧ − ls_post + ls_post ≤ 0 ∧ ls_post − ls_post ≤ 0 ∧ − ls_0 + ls_0 ≤ 0 ∧ ls_0 − ls_0 ≤ 0 ∧ − lr_post + lr_post ≤ 0 ∧ lr_post − lr_post ≤ 0 ∧ − lr_0 + lr_0 ≤ 0 ∧ lr_0 − lr_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − fs_post + fs_post ≤ 0 ∧ fs_post − fs_post ≤ 0 ∧ − fs_0 + fs_0 ≤ 0 ∧ fs_0 − fs_0 ≤ 0 ∧ − fr_post + fr_post ≤ 0 ∧ fr_post − fr_post ≤ 0 ∧ − fr_0 + fr_0 ≤ 0 ∧ fr_0 − fr_0 ≤ 0 ∧ − c2_0 + c2_0 ≤ 0 ∧ c2_0 − c2_0 ≤ 0 ∧ − c1_0 + c1_0 ≤ 0 ∧ c1_0 − c1_0 ≤ 0 ∧ − bs_post + bs_post ≤ 0 ∧ bs_post − bs_post ≤ 0 ∧ − bs_0 + bs_0 ≤ 0 ∧ bs_0 − bs_0 ≤ 0 ∧ − br_post + br_post ≤ 0 ∧ br_post − br_post ≤ 0 ∧ − br_0 + br_0 ≤ 0 ∧ br_0 − br_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0

5 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

3* 64 3: − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − s_ab_post + s_ab_post ≤ 0 ∧ s_ab_post − s_ab_post ≤ 0 ∧ − s_ab_0 + s_ab_0 ≤ 0 ∧ s_ab_0 − s_ab_0 ≤ 0 ∧ − rrep_post + rrep_post ≤ 0 ∧ rrep_post − rrep_post ≤ 0 ∧ − rrep_0 + rrep_0 ≤ 0 ∧ rrep_0 − rrep_0 ≤ 0 ∧ − recv_post + recv_post ≤ 0 ∧ recv_post − recv_post ≤ 0 ∧ − recv_0 + recv_0 ≤ 0 ∧ recv_0 − recv_0 ≤ 0 ∧ − r_ab_post + r_ab_post ≤ 0 ∧ r_ab_post − r_ab_post ≤ 0 ∧ − r_ab_0 + r_ab_0 ≤ 0 ∧ r_ab_0 − r_ab_0 ≤ 0 ∧ − pos_post + pos_post ≤ 0 ∧ pos_post − pos_post ≤ 0 ∧ − pos_0 + pos_0 ≤ 0 ∧ pos_0 − pos_0 ≤ 0 ∧ − next_post + next_post ≤ 0 ∧ next_post − next_post ≤ 0 ∧ − next_0 + next_0 ≤ 0 ∧ next_0 − next_0 ≤ 0 ∧ − ls_post + ls_post ≤ 0 ∧ ls_post − ls_post ≤ 0 ∧ − ls_0 + ls_0 ≤ 0 ∧ ls_0 − ls_0 ≤ 0 ∧ − lr_post + lr_post ≤ 0 ∧ lr_post − lr_post ≤ 0 ∧ − lr_0 + lr_0 ≤ 0 ∧ lr_0 − lr_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − fs_post + fs_post ≤ 0 ∧ fs_post − fs_post ≤ 0 ∧ − fs_0 + fs_0 ≤ 0 ∧ fs_0 − fs_0 ≤ 0 ∧ − fr_post + fr_post ≤ 0 ∧ fr_post − fr_post ≤ 0 ∧ − fr_0 + fr_0 ≤ 0 ∧ fr_0 − fr_0 ≤ 0 ∧ − c2_0 + c2_0 ≤ 0 ∧ c2_0 − c2_0 ≤ 0 ∧ − c1_0 + c1_0 ≤ 0 ∧ c1_0 − c1_0 ≤ 0 ∧ − bs_post + bs_post ≤ 0 ∧ bs_post − bs_post ≤ 0 ∧ − bs_0 + bs_0 ≤ 0 ∧ bs_0 − bs_0 ≤ 0 ∧ − br_post + br_post ≤ 0 ∧ br_post − br_post ≤ 0 ∧ − br_0 + br_0 ≤ 0 ∧ br_0 − br_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0

6 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

3 62 3_var_snapshot: − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − s_ab_post + s_ab_post ≤ 0 ∧ s_ab_post − s_ab_post ≤ 0 ∧ − s_ab_0 + s_ab_0 ≤ 0 ∧ s_ab_0 − s_ab_0 ≤ 0 ∧ − rrep_post + rrep_post ≤ 0 ∧ rrep_post − rrep_post ≤ 0 ∧ − rrep_0 + rrep_0 ≤ 0 ∧ rrep_0 − rrep_0 ≤ 0 ∧ − recv_post + recv_post ≤ 0 ∧ recv_post − recv_post ≤ 0 ∧ − recv_0 + recv_0 ≤ 0 ∧ recv_0 − recv_0 ≤ 0 ∧ − r_ab_post + r_ab_post ≤ 0 ∧ r_ab_post − r_ab_post ≤ 0 ∧ − r_ab_0 + r_ab_0 ≤ 0 ∧ r_ab_0 − r_ab_0 ≤ 0 ∧ − pos_post + pos_post ≤ 0 ∧ pos_post − pos_post ≤ 0 ∧ − pos_0 + pos_0 ≤ 0 ∧ pos_0 − pos_0 ≤ 0 ∧ − next_post + next_post ≤ 0 ∧ next_post − next_post ≤ 0 ∧ − next_0 + next_0 ≤ 0 ∧ next_0 − next_0 ≤ 0 ∧ − ls_post + ls_post ≤ 0 ∧ ls_post − ls_post ≤ 0 ∧ − ls_0 + ls_0 ≤ 0 ∧ ls_0 − ls_0 ≤ 0 ∧ − lr_post + lr_post ≤ 0 ∧ lr_post − lr_post ≤ 0 ∧ − lr_0 + lr_0 ≤ 0 ∧ lr_0 − lr_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − fs_post + fs_post ≤ 0 ∧ fs_post − fs_post ≤ 0 ∧ − fs_0 + fs_0 ≤ 0 ∧ fs_0 − fs_0 ≤ 0 ∧ − fr_post + fr_post ≤ 0 ∧ fr_post − fr_post ≤ 0 ∧ − fr_0 + fr_0 ≤ 0 ∧ fr_0 − fr_0 ≤ 0 ∧ − c2_0 + c2_0 ≤ 0 ∧ c2_0 − c2_0 ≤ 0 ∧ − c1_0 + c1_0 ≤ 0 ∧ c1_0 − c1_0 ≤ 0 ∧ − bs_post + bs_post ≤ 0 ∧ bs_post − bs_post ≤ 0 ∧ − bs_0 + bs_0 ≤ 0 ∧ bs_0 − bs_0 ≤ 0 ∧ − br_post + br_post ≤ 0 ∧ br_post − br_post ≤ 0 ∧ − br_0 + br_0 ≤ 0 ∧ br_0 − br_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0

7 SCC Decomposition

We consider subproblems for each of the 1 SCC(s) of the program graph.

7.1 SCC Subproblem 1/1

Here we consider the SCC { 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 26, 27, 28, 0_var_snapshot, 0*, 3_var_snapshot, 3* }.

7.1.1 Transition Removal

We remove transition 47 using the following ranking functions, which are bounded by 39.

0: 1 + 22⋅N_0 − 22⋅i_0
1: 22⋅N_0 − 22⋅i_0
2: −6 + 22⋅N_0 − 22⋅i_0
3: −6 + 22⋅N_0 − 22⋅i_0
4: −19 + 22⋅N_0 − 22⋅i_0
5: −18 + 22⋅N_0 − 22⋅i_0
6: −6 + 22⋅N_0 − 22⋅i_0
7: −6 + 22⋅N_0 − 22⋅i_0
8: −6 + 22⋅N_0 − 22⋅i_0
9: −6 + 22⋅N_0 − 22⋅i_0
10: −6 + 22⋅N_0 − 22⋅i_0
11: −6 + 22⋅N_0 − 22⋅i_0
12: −6 + 22⋅N_0 − 22⋅i_0
13: −6 + 22⋅N_0 − 22⋅i_0
14: −6 + 22⋅N_0 − 22⋅i_0
15: −6 + 22⋅N_0 − 22⋅i_0
16: −6 + 22⋅N_0 − 22⋅i_0
17: −6 + 22⋅N_0 − 22⋅i_0
18: −6 + 22⋅N_0 − 22⋅i_0
19: −6 + 22⋅N_0 − 22⋅i_0
20: −6 + 22⋅N_0 − 22⋅i_0
21: −6 + 22⋅N_0 − 22⋅i_0
22: −6 + 22⋅N_0 − 22⋅i_0
23: −6 + 22⋅N_0 − 22⋅i_0
24: −6 + 22⋅N_0 − 22⋅i_0
26: −5 + 22⋅N_0 − 22⋅i_0
27: −4 + 22⋅N_0 − 22⋅i_0
28: −3 + 22⋅N_0 − 22⋅i_0
0_var_snapshot: 1 + 22⋅N_0 − 22⋅i_0
0*: 2 + 22⋅N_0 − 22⋅i_0
3_var_snapshot: −6 + 22⋅N_0 − 22⋅i_0
3*: −6 + 22⋅N_0 − 22⋅i_0

7.1.2 Transition Removal

We remove transitions 48, 49, 50, 52 using the following ranking functions, which are bounded by 17.

0: 3 + 22⋅N_0 − 22⋅i_0
1: 22⋅N_0 − 22⋅i_0
2: −15 + 22⋅N_0 − 22⋅i_0
3: −15 + 22⋅N_0 − 22⋅i_0
4: −17 + 22⋅N_0 − 22⋅i_0
5: −16 + 22⋅N_0 − 22⋅i_0
6: −15 + 22⋅N_0 − 22⋅i_0
7: −15 + 22⋅N_0 − 22⋅i_0
8: −15 + 22⋅N_0 − 22⋅i_0
9: −15 + 22⋅N_0 − 22⋅i_0
10: −15 + 22⋅N_0 − 22⋅i_0
11: −15 + 22⋅N_0 − 22⋅i_0
12: −15 + 22⋅N_0 − 22⋅i_0
13: −15 + 22⋅N_0 − 22⋅i_0
14: −15 + 22⋅N_0 − 22⋅i_0
15: −15 + 22⋅N_0 − 22⋅i_0
16: −15 + 22⋅N_0 − 22⋅i_0
17: −15 + 22⋅N_0 − 22⋅i_0
18: −15 + 22⋅N_0 − 22⋅i_0
19: −15 + 22⋅N_0 − 22⋅i_0
20: −15 + 22⋅N_0 − 22⋅i_0
21: −15 + 22⋅N_0 − 22⋅i_0
22: −15 + 22⋅N_0 − 22⋅i_0
23: −15 + 22⋅N_0 − 22⋅i_0
24: −15 + 22⋅N_0 − 22⋅i_0
26: −14 + 22⋅N_0 − 22⋅i_0
27: 18
28: 19
0_var_snapshot: 2 + 22⋅N_0 − 22⋅i_0
0*: 4 + 22⋅N_0 − 22⋅i_0
3_var_snapshot: −15 + 22⋅N_0 − 22⋅i_0
3*: −15 + 22⋅N_0 − 22⋅i_0

7.1.3 Transition Removal

We remove transitions 55, 57, 2 using the following ranking functions, which are bounded by −6.

0: −5
1: −7
2: −1 + 19⋅N_0 − 19⋅next_0
3: −1 + 19⋅N_0 − 19⋅next_0
4: −3 + 19⋅N_0 − 19⋅next_0
5: −2 + 19⋅N_0 − 19⋅next_0
6: −1 + 19⋅N_0 − 19⋅next_0
7: −1 + 19⋅N_0 − 19⋅next_0
8: −1 + 19⋅N_0 − 19⋅next_0
9: −1 + 19⋅N_0 − 19⋅next_0
10: −1 + 19⋅N_0 − 19⋅next_0
11: −1 + 19⋅N_0 − 19⋅next_0
12: −1 + 19⋅N_0 − 19⋅next_0
13: −1 + 19⋅N_0 − 19⋅next_0
14: −1 + 19⋅N_0 − 19⋅next_0
15: −1 + 19⋅N_0 − 19⋅next_0
16: −1 + 19⋅N_0 − 19⋅next_0
17: −1 + 19⋅N_0 − 19⋅next_0
18: −1 + 19⋅N_0 − 19⋅next_0
19: −1 + 19⋅N_0 − 19⋅next_0
20: −1 + 19⋅N_0 − 19⋅next_0
21: −1 + 19⋅N_0 − 19⋅next_0
22: −1 + 19⋅N_0 − 19⋅next_0
23: −1 + 19⋅N_0 − 19⋅next_0
24: −1 + 19⋅N_0 − 19⋅next_0
26: 19⋅N_0 − 19⋅next_0
27: 0
28: 0
0_var_snapshot: −6
0*: −4
3_var_snapshot: −1 + 19⋅N_0 − 19⋅next_0
3*: −1 + 19⋅N_0 − 19⋅next_0

7.1.4 Transition Removal

We remove transition 0 using the following ranking functions, which are bounded by 0.

0: 0
1: 0
2: −19⋅next_0
3: −19⋅next_0
4: −2 − 19⋅next_0
5: −1 − 19⋅next_0
6: −19⋅next_0
7: −19⋅next_0
8: −19⋅next_0
9: −19⋅next_0
10: −19⋅next_0
11: −19⋅next_0
12: −19⋅next_0
13: −19⋅next_0
14: −19⋅next_0
15: −19⋅next_0
16: −19⋅next_0
17: −19⋅next_0
18: −19⋅next_0
19: −19⋅next_0
20: −19⋅next_0
21: −19⋅next_0
22: −19⋅next_0
23: −19⋅next_0
24: −19⋅next_0
26: 1 − 19⋅next_0
27: 0
28: 0
0_var_snapshot: 1
0*: 0
3_var_snapshot: −19⋅next_0
3*: −19⋅next_0

7.1.5 Transition Removal

We remove transitions 4, 46 using the following ranking functions, which are bounded by −3.

0: 0
1: 0
2: −1
3: −1
4: −3 + s_ab_post
5: −2
6: −1
7: −1
8: −1
9: −1
10: −1
11: −1
12: −1
13: −1
14: −1
15: −1
16: −1
17: −1
18: −1
19: −1
20: −1
21: −1
22: −1
23: −1
24: −1
26: 0
27: 0
28: 0
0_var_snapshot: 0
0*: 0
3_var_snapshot: −1
3*: −1

7.1.6 Transition Removal

We remove transitions 3, 9 using the following ranking functions, which are bounded by −2.

0: 0
1: 0
2: 0
3: 0
4: −2
5: −1
6: 0
7: 0
8: 0
9: 0
10: 0
11: 0
12: 0
13: 0
14: 0
15: 0
16: 0
17: 0
18: 0
19: 0
20: 0
21: 0
22: 0
23: 0
24: 0
26: 0
27: 0
28: 0
0_var_snapshot: 0
0*: 0
3_var_snapshot: 0
3*: 0

7.1.7 Transition Removal

We remove transition 42 using the following ranking functions, which are bounded by 6.

0: 0
1: 0
2: 7⋅z_0
3: 7⋅z_0
4: 0
5: 0
6: 7⋅z_0
7: 7⋅z_0
8: 7⋅z_0
9: 7⋅z_0
10: 7⋅z_0
11: 7⋅z_0
12: 7⋅z_0
13: 7⋅z_0
14: 7⋅z_0
15: 7⋅z_0
16: 7⋅z_0
17: 7⋅z_0
18: 7⋅z_0
19: 7⋅z_0
20: 7⋅z_0
21: 7⋅z_0
22: 7⋅z_0
23: 7⋅z_0
24: 7⋅z_0
26: 0
27: 0
28: 0
0_var_snapshot: 0
0*: 0
3_var_snapshot: 7⋅z_0
3*: 7⋅z_0

7.1.8 Transition Removal

We remove transition 12 using the following ranking functions, which are bounded by 11.

0: 0
1: 0
2: 12⋅z_0
3: 12⋅z_0
4: 0
5: 0
6: 12⋅z_0
7: 12⋅z_0
8: 12⋅z_0
9: 12⋅z_0
10: 12⋅z_0
11: 12⋅z_0
12: 12⋅z_0
13: 12⋅z_0
14: 12⋅z_0
15: 12⋅z_0
16: 12⋅z_0
17: 12⋅z_0
18: 12⋅z_0
19: 12⋅z_0
20: 12⋅z_0
21: 12⋅z_0
22: 12⋅z_0
23: 12⋅z_0
24: 12⋅z_0
26: 0
27: 0
28: 0
0_var_snapshot: 0
0*: 0
3_var_snapshot: 12⋅z_0
3*: 12⋅z_0

7.1.9 Splitting Cut-Point Transitions

We consider 2 subproblems corresponding to sets of cut-point transitions as follows.

7.1.9.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 54.

7.1.9.1.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

7.1.9.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 61.

7.1.9.2.1 Invariant Updates

The following invariants are asserted.

0: pos_0 ≤ 0 ∧ − i_0 ≤ 0 ∨ N_0 − i_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − i_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − i_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0
1: pos_0 ≤ 0 ∧ − i_0 ≤ 0 ∨ N_0 − i_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − i_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − i_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0
2: pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ 1 ≤ 0 ∨ ls_0 ≤ 0 ∧ pos_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0
3: pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ pos_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − ls_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0
4: pos_0 ≤ 0 ∧ −1 − i_0 ≤ 0 ∨ −1 + N_0 − i_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ −1 − i_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0
5: pos_0 ≤ 0 ∧ −1 − i_0 ≤ 0 ∨ −1 + N_0 − i_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ −1 − i_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0
6: 1 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ −1 − i_0 ≤ 0 ∧ 1 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ −1 + c2_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ − ls_0 ≤ 0
7: pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ −1 + c2_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∨ 1 ≤ 0 ∨ ls_0 ≤ 0 ∧ pos_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ −1 − i_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0
8: pos_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ pos_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ −1 + c2_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ − ls_0 ≤ 0
9: pos_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ pos_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ − ls_0 ≤ 0
10: 1 ≤ 0 ∨ pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ − ls_0 ≤ 0
11: pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ 1 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ − ls_0 ≤ 0
12: pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ 1 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ − ls_0 ≤ 0
13: pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − lr_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ − ls_0 ≤ 0
14: pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fr_0 ≤ 0 ∧ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fr_0 ≤ 0 ∧ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fr_0 ≤ 0 ∧ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − lr_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ − ls_0 ≤ 0
15: pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ 1 ≤ 0
16: pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − lr_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − lr_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ 1 ≤ 0
17: pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − lr_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − lr_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fr_0 ≤ 0 ∧ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fr_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fr_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − lr_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fr_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0
18: pos_0 ≤ 0 ∧ − br_0 + r_ab_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ br_0 − r_ab_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ − br_0 + r_ab_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ br_0 − r_ab_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ pos_0 ≤ 0 ∧ − br_0 + r_ab_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ br_0 − r_ab_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − lr_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − lr_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ − br_0 + r_ab_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ br_0 − r_ab_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − lr_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − lr_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fr_0 ≤ 0 ∧ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fr_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fr_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − lr_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fr_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0
19: pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ pos_0 ≤ 0 ∧ − br_0 + r_ab_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ br_0 − r_ab_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ − br_0 + r_ab_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ br_0 − r_ab_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − lr_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ pos_0 ≤ 0 ∧ − br_0 + r_ab_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ br_0 − r_ab_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − lr_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − lr_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ − br_0 + r_ab_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ br_0 − r_ab_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − lr_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fr_0 ≤ 0 ∧ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ − fr_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ 1 ≤ 0 ∨ fr_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − lr_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ − fr_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0
20: pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − lr_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − lr_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fr_0 ≤ 0 ∧ lr_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fr_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fr_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − lr_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fr_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0
21: 1 ≤ 0 ∨ fs_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − ls_0 ≤ 0 ∧ 1 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0
22: pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ pos_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ 1 ≤ 0 ∨ fs_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − ls_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0
23: pos_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ pos_0 ≤ 0 ∧ z_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − ls_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0
24: pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ ls_0 ≤ 0 ∧ pos_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − ls_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0
25: TRUE
26: ls_0 ≤ 0 ∧ pos_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − ls_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ ls_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + N_0 − i_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ − ls_0 ≤ 0
27: pos_0 ≤ 0 ∧ − i_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∧ − i_0 ≤ 0 ∨ 1 ≤ 0 ∨ fs_0 ≤ 0 ∧ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∧ − i_0 ≤ 0
28: pos_0 ≤ 0 ∧ − i_0 ≤ 0 ∨ 1 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − i_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∨ z_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − i_0 ≤ 0 ∧ 2 − pos_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − i_0 ≤ 0
29: TRUE
30: TRUE
0: FALSE
1: 1 ≤ 0
2: 1 ≤ 0
3: pos_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − ls_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0
4: 1 ≤ 0
5: 1 ≤ 0
6: −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∨ −1 + c2_0 ≤ 0 ∧ 1 − c2_0 ≤ 0
7: −1 + c2_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∨ 1 ≤ 0
8: −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∨ −1 + c2_0 ≤ 0 ∧ 1 − c2_0 ≤ 0
9: −1 + c2_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∨ −1 + c2_0 ≤ 0 ∧ 1 − c2_0 ≤ 0
10: 1 ≤ 0 ∨ −1 + pos_0 ≤ 0 ∨ −1 + c2_0 ≤ 0 ∧ 1 − c2_0 ≤ 0
11: −1 + pos_0 ≤ 0 ∨ −1 + c2_0 ≤ 0 ∧ 1 − c2_0 ≤ 0
12: −1 + pos_0 ≤ 0 ∨ 1 ≤ 0 ∨ −1 + c2_0 ≤ 0 ∧ 1 − c2_0 ≤ 0
13: −1 + pos_0 ≤ 0 ∨ −1 + c2_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − lr_0 ≤ 0 ∨ −1 + c2_0 ≤ 0 ∧ 1 − c2_0 ≤ 0
14: −1 + pos_0 ≤ 0 ∨ −1 + c2_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − lr_0 ≤ 0 ∨ −1 + c2_0 ≤ 0 ∧ 1 − c2_0 ≤ 0
15: −1 + pos_0 ≤ 0
16: −1 + pos_0 ≤ 0 ∨ 1 ≤ 0
17: −1 + pos_0 ≤ 0 ∨ fr_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − lr_0 ≤ 0 ∧ − fr_0 ≤ 0 ∨ fr_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ − fr_0 ≤ 0
18: −1 + pos_0 ≤ 0 ∧ − br_0 + r_ab_0 ≤ 0 ∧ br_0 − r_ab_0 ≤ 0 ∨ −1 + pos_0 ≤ 0 ∨ fr_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − lr_0 ≤ 0 ∧ − fr_0 ≤ 0 ∨ fr_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ − fr_0 ≤ 0
19: −1 + pos_0 ≤ 0 ∨ −1 + pos_0 ≤ 0 ∧ − br_0 + r_ab_0 ≤ 0 ∧ br_0 − r_ab_0 ≤ 0 ∨ fr_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − lr_0 ≤ 0 ∧ − fr_0 ≤ 0 ∨ 1 ≤ 0 ∨ fr_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ − fr_0 ≤ 0
20: −1 + pos_0 ≤ 0 ∨ fr_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − lr_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fr_0 ≤ 0 ∨ fr_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fr_0 ≤ 0
21: 1 ≤ 0 ∨ fs_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − ls_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0
22: −1 + pos_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − ls_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0
23: pos_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − ls_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0
24: pos_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − ls_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0
26: 1 ≤ 0
27: 1 ≤ 0
28: 1 ≤ 0
0_var_snapshot: 1 ≤ 0
0*: 1 ≤ 0
3_var_snapshot: pos_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − ls_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0 ∨ fs_0 ≤ 0 ∧ −1 + c2_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ 1 − c2_0 ≤ 0 ∧ 1 − recv_0 ≤ 0 ∧ − fs_0 ≤ 0
3*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

7.1.9.2.2 Transition Removal

We remove transition 62 using the following ranking functions, which are bounded by −34.

0: −1
1: −2
3: −3
4: −4
5: −5
26: −6
27: −7
28: −8
0_var_snapshot: −9
0*: −10
3_var_snapshot: −11
24: −12
23: −13
21: −14
22: −15
20: −16
19: −17
18: −18
17: −19
16: −20
15: −21
14: −22
13: −23
11: −24
12: −25
10: −26
9: −27
8: −28
6: −29
7: −30
2: −31
3*: −32

7.1.9.2.3 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

Tool configuration

T2Cert