LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

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

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
0 41 0: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tau_post + tau_post ≤ 0 ∧ tau_post − tau_post ≤ 0 ∧ − tau_0 + tau_0 ≤ 0 ∧ tau_0 − tau_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − sqrarg_post + sqrarg_post ≤ 0 ∧ sqrarg_post − sqrarg_post ≤ 0 ∧ − sqrarg_0 + sqrarg_0 ≤ 0 ∧ sqrarg_0 − sqrarg_0 ≤ 0 ∧ − sigma_post + sigma_post ≤ 0 ∧ sigma_post − sigma_post ≤ 0 ∧ − sigma_0 + sigma_0 ≤ 0 ∧ sigma_0 − sigma_0 ≤ 0 ∧ − scale_post + scale_post ≤ 0 ∧ scale_post − scale_post ≤ 0 ∧ − scale_0 + scale_0 ≤ 0 ∧ scale_0 − scale_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − maxarg2_post + maxarg2_post ≤ 0 ∧ maxarg2_post − maxarg2_post ≤ 0 ∧ − maxarg2_0 + maxarg2_0 ≤ 0 ∧ maxarg2_0 − maxarg2_0 ≤ 0 ∧ − maxarg1_post + maxarg1_post ≤ 0 ∧ maxarg1_post − maxarg1_post ≤ 0 ∧ − maxarg1_0 + maxarg1_0 ≤ 0 ∧ maxarg1_0 − maxarg1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0
5 48 5: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tau_post + tau_post ≤ 0 ∧ tau_post − tau_post ≤ 0 ∧ − tau_0 + tau_0 ≤ 0 ∧ tau_0 − tau_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − sqrarg_post + sqrarg_post ≤ 0 ∧ sqrarg_post − sqrarg_post ≤ 0 ∧ − sqrarg_0 + sqrarg_0 ≤ 0 ∧ sqrarg_0 − sqrarg_0 ≤ 0 ∧ − sigma_post + sigma_post ≤ 0 ∧ sigma_post − sigma_post ≤ 0 ∧ − sigma_0 + sigma_0 ≤ 0 ∧ sigma_0 − sigma_0 ≤ 0 ∧ − scale_post + scale_post ≤ 0 ∧ scale_post − scale_post ≤ 0 ∧ − scale_0 + scale_0 ≤ 0 ∧ scale_0 − scale_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − maxarg2_post + maxarg2_post ≤ 0 ∧ maxarg2_post − maxarg2_post ≤ 0 ∧ − maxarg2_0 + maxarg2_0 ≤ 0 ∧ maxarg2_0 − maxarg2_0 ≤ 0 ∧ − maxarg1_post + maxarg1_post ≤ 0 ∧ maxarg1_post − maxarg1_post ≤ 0 ∧ − maxarg1_0 + maxarg1_0 ≤ 0 ∧ maxarg1_0 − maxarg1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0
8 55 8: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tau_post + tau_post ≤ 0 ∧ tau_post − tau_post ≤ 0 ∧ − tau_0 + tau_0 ≤ 0 ∧ tau_0 − tau_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − sqrarg_post + sqrarg_post ≤ 0 ∧ sqrarg_post − sqrarg_post ≤ 0 ∧ − sqrarg_0 + sqrarg_0 ≤ 0 ∧ sqrarg_0 − sqrarg_0 ≤ 0 ∧ − sigma_post + sigma_post ≤ 0 ∧ sigma_post − sigma_post ≤ 0 ∧ − sigma_0 + sigma_0 ≤ 0 ∧ sigma_0 − sigma_0 ≤ 0 ∧ − scale_post + scale_post ≤ 0 ∧ scale_post − scale_post ≤ 0 ∧ − scale_0 + scale_0 ≤ 0 ∧ scale_0 − scale_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − maxarg2_post + maxarg2_post ≤ 0 ∧ maxarg2_post − maxarg2_post ≤ 0 ∧ − maxarg2_0 + maxarg2_0 ≤ 0 ∧ maxarg2_0 − maxarg2_0 ≤ 0 ∧ − maxarg1_post + maxarg1_post ≤ 0 ∧ maxarg1_post − maxarg1_post ≤ 0 ∧ − maxarg1_0 + maxarg1_0 ≤ 0 ∧ maxarg1_0 − maxarg1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0
9 62 9: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tau_post + tau_post ≤ 0 ∧ tau_post − tau_post ≤ 0 ∧ − tau_0 + tau_0 ≤ 0 ∧ tau_0 − tau_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − sqrarg_post + sqrarg_post ≤ 0 ∧ sqrarg_post − sqrarg_post ≤ 0 ∧ − sqrarg_0 + sqrarg_0 ≤ 0 ∧ sqrarg_0 − sqrarg_0 ≤ 0 ∧ − sigma_post + sigma_post ≤ 0 ∧ sigma_post − sigma_post ≤ 0 ∧ − sigma_0 + sigma_0 ≤ 0 ∧ sigma_0 − sigma_0 ≤ 0 ∧ − scale_post + scale_post ≤ 0 ∧ scale_post − scale_post ≤ 0 ∧ − scale_0 + scale_0 ≤ 0 ∧ scale_0 − scale_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − maxarg2_post + maxarg2_post ≤ 0 ∧ maxarg2_post − maxarg2_post ≤ 0 ∧ − maxarg2_0 + maxarg2_0 ≤ 0 ∧ maxarg2_0 − maxarg2_0 ≤ 0 ∧ − maxarg1_post + maxarg1_post ≤ 0 ∧ maxarg1_post − maxarg1_post ≤ 0 ∧ − maxarg1_0 + maxarg1_0 ≤ 0 ∧ maxarg1_0 − maxarg1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0
10 69 10: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tau_post + tau_post ≤ 0 ∧ tau_post − tau_post ≤ 0 ∧ − tau_0 + tau_0 ≤ 0 ∧ tau_0 − tau_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − sqrarg_post + sqrarg_post ≤ 0 ∧ sqrarg_post − sqrarg_post ≤ 0 ∧ − sqrarg_0 + sqrarg_0 ≤ 0 ∧ sqrarg_0 − sqrarg_0 ≤ 0 ∧ − sigma_post + sigma_post ≤ 0 ∧ sigma_post − sigma_post ≤ 0 ∧ − sigma_0 + sigma_0 ≤ 0 ∧ sigma_0 − sigma_0 ≤ 0 ∧ − scale_post + scale_post ≤ 0 ∧ scale_post − scale_post ≤ 0 ∧ − scale_0 + scale_0 ≤ 0 ∧ scale_0 − scale_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − maxarg2_post + maxarg2_post ≤ 0 ∧ maxarg2_post − maxarg2_post ≤ 0 ∧ − maxarg2_0 + maxarg2_0 ≤ 0 ∧ maxarg2_0 − maxarg2_0 ≤ 0 ∧ − maxarg1_post + maxarg1_post ≤ 0 ∧ maxarg1_post − maxarg1_post ≤ 0 ∧ − maxarg1_0 + maxarg1_0 ≤ 0 ∧ maxarg1_0 − maxarg1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0
13 76 13: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tau_post + tau_post ≤ 0 ∧ tau_post − tau_post ≤ 0 ∧ − tau_0 + tau_0 ≤ 0 ∧ tau_0 − tau_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − sqrarg_post + sqrarg_post ≤ 0 ∧ sqrarg_post − sqrarg_post ≤ 0 ∧ − sqrarg_0 + sqrarg_0 ≤ 0 ∧ sqrarg_0 − sqrarg_0 ≤ 0 ∧ − sigma_post + sigma_post ≤ 0 ∧ sigma_post − sigma_post ≤ 0 ∧ − sigma_0 + sigma_0 ≤ 0 ∧ sigma_0 − sigma_0 ≤ 0 ∧ − scale_post + scale_post ≤ 0 ∧ scale_post − scale_post ≤ 0 ∧ − scale_0 + scale_0 ≤ 0 ∧ scale_0 − scale_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − maxarg2_post + maxarg2_post ≤ 0 ∧ maxarg2_post − maxarg2_post ≤ 0 ∧ − maxarg2_0 + maxarg2_0 ≤ 0 ∧ maxarg2_0 − maxarg2_0 ≤ 0 ∧ − maxarg1_post + maxarg1_post ≤ 0 ∧ maxarg1_post − maxarg1_post ≤ 0 ∧ − maxarg1_0 + maxarg1_0 ≤ 0 ∧ maxarg1_0 − maxarg1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0
16 83 16: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tau_post + tau_post ≤ 0 ∧ tau_post − tau_post ≤ 0 ∧ − tau_0 + tau_0 ≤ 0 ∧ tau_0 − tau_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − sqrarg_post + sqrarg_post ≤ 0 ∧ sqrarg_post − sqrarg_post ≤ 0 ∧ − sqrarg_0 + sqrarg_0 ≤ 0 ∧ sqrarg_0 − sqrarg_0 ≤ 0 ∧ − sigma_post + sigma_post ≤ 0 ∧ sigma_post − sigma_post ≤ 0 ∧ − sigma_0 + sigma_0 ≤ 0 ∧ sigma_0 − sigma_0 ≤ 0 ∧ − scale_post + scale_post ≤ 0 ∧ scale_post − scale_post ≤ 0 ∧ − scale_0 + scale_0 ≤ 0 ∧ scale_0 − scale_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − maxarg2_post + maxarg2_post ≤ 0 ∧ maxarg2_post − maxarg2_post ≤ 0 ∧ − maxarg2_0 + maxarg2_0 ≤ 0 ∧ maxarg2_0 − maxarg2_0 ≤ 0 ∧ − maxarg1_post + maxarg1_post ≤ 0 ∧ maxarg1_post − maxarg1_post ≤ 0 ∧ − maxarg1_0 + maxarg1_0 ≤ 0 ∧ maxarg1_0 − maxarg1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 1, 2, 3, 37, 39, 40 using the following ranking functions, which are bounded by −29.

27: 0
26: 0
0: 0
1: 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
25: 0
4: 0
2: 0
3: 0
27: −7
26: −8
0: −9
1: −9
5: −9
6: −9
7: −9
8: −9
9: −9
10: −9
11: −9
12: −9
13: −9
14: −9
15: −9
16: −9
17: −9
18: −9
19: −9
20: −9
21: −9
22: −9
23: −9
24: −9
25: −9
0_var_snapshot: −9
0*: −9
5_var_snapshot: −9
5*: −9
8_var_snapshot: −9
8*: −9
9_var_snapshot: −9
9*: −9
10_var_snapshot: −9
10*: −9
13_var_snapshot: −9
13*: −9
16_var_snapshot: −9
16*: −9
4: −22
2: −23
3: −24

4 Location Addition

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

0* 44 0: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tau_post + tau_post ≤ 0 ∧ tau_post − tau_post ≤ 0 ∧ − tau_0 + tau_0 ≤ 0 ∧ tau_0 − tau_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − sqrarg_post + sqrarg_post ≤ 0 ∧ sqrarg_post − sqrarg_post ≤ 0 ∧ − sqrarg_0 + sqrarg_0 ≤ 0 ∧ sqrarg_0 − sqrarg_0 ≤ 0 ∧ − sigma_post + sigma_post ≤ 0 ∧ sigma_post − sigma_post ≤ 0 ∧ − sigma_0 + sigma_0 ≤ 0 ∧ sigma_0 − sigma_0 ≤ 0 ∧ − scale_post + scale_post ≤ 0 ∧ scale_post − scale_post ≤ 0 ∧ − scale_0 + scale_0 ≤ 0 ∧ scale_0 − scale_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − maxarg2_post + maxarg2_post ≤ 0 ∧ maxarg2_post − maxarg2_post ≤ 0 ∧ − maxarg2_0 + maxarg2_0 ≤ 0 ∧ maxarg2_0 − maxarg2_0 ≤ 0 ∧ − maxarg1_post + maxarg1_post ≤ 0 ∧ maxarg1_post − maxarg1_post ≤ 0 ∧ − maxarg1_0 + maxarg1_0 ≤ 0 ∧ maxarg1_0 − maxarg1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0

5 Location Addition

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

0 42 0_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tau_post + tau_post ≤ 0 ∧ tau_post − tau_post ≤ 0 ∧ − tau_0 + tau_0 ≤ 0 ∧ tau_0 − tau_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − sqrarg_post + sqrarg_post ≤ 0 ∧ sqrarg_post − sqrarg_post ≤ 0 ∧ − sqrarg_0 + sqrarg_0 ≤ 0 ∧ sqrarg_0 − sqrarg_0 ≤ 0 ∧ − sigma_post + sigma_post ≤ 0 ∧ sigma_post − sigma_post ≤ 0 ∧ − sigma_0 + sigma_0 ≤ 0 ∧ sigma_0 − sigma_0 ≤ 0 ∧ − scale_post + scale_post ≤ 0 ∧ scale_post − scale_post ≤ 0 ∧ − scale_0 + scale_0 ≤ 0 ∧ scale_0 − scale_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − maxarg2_post + maxarg2_post ≤ 0 ∧ maxarg2_post − maxarg2_post ≤ 0 ∧ − maxarg2_0 + maxarg2_0 ≤ 0 ∧ maxarg2_0 − maxarg2_0 ≤ 0 ∧ − maxarg1_post + maxarg1_post ≤ 0 ∧ maxarg1_post − maxarg1_post ≤ 0 ∧ − maxarg1_0 + maxarg1_0 ≤ 0 ∧ maxarg1_0 − maxarg1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0

6 Location Addition

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

5* 51 5: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tau_post + tau_post ≤ 0 ∧ tau_post − tau_post ≤ 0 ∧ − tau_0 + tau_0 ≤ 0 ∧ tau_0 − tau_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − sqrarg_post + sqrarg_post ≤ 0 ∧ sqrarg_post − sqrarg_post ≤ 0 ∧ − sqrarg_0 + sqrarg_0 ≤ 0 ∧ sqrarg_0 − sqrarg_0 ≤ 0 ∧ − sigma_post + sigma_post ≤ 0 ∧ sigma_post − sigma_post ≤ 0 ∧ − sigma_0 + sigma_0 ≤ 0 ∧ sigma_0 − sigma_0 ≤ 0 ∧ − scale_post + scale_post ≤ 0 ∧ scale_post − scale_post ≤ 0 ∧ − scale_0 + scale_0 ≤ 0 ∧ scale_0 − scale_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − maxarg2_post + maxarg2_post ≤ 0 ∧ maxarg2_post − maxarg2_post ≤ 0 ∧ − maxarg2_0 + maxarg2_0 ≤ 0 ∧ maxarg2_0 − maxarg2_0 ≤ 0 ∧ − maxarg1_post + maxarg1_post ≤ 0 ∧ maxarg1_post − maxarg1_post ≤ 0 ∧ − maxarg1_0 + maxarg1_0 ≤ 0 ∧ maxarg1_0 − maxarg1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0

7 Location Addition

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

5 49 5_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tau_post + tau_post ≤ 0 ∧ tau_post − tau_post ≤ 0 ∧ − tau_0 + tau_0 ≤ 0 ∧ tau_0 − tau_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − sqrarg_post + sqrarg_post ≤ 0 ∧ sqrarg_post − sqrarg_post ≤ 0 ∧ − sqrarg_0 + sqrarg_0 ≤ 0 ∧ sqrarg_0 − sqrarg_0 ≤ 0 ∧ − sigma_post + sigma_post ≤ 0 ∧ sigma_post − sigma_post ≤ 0 ∧ − sigma_0 + sigma_0 ≤ 0 ∧ sigma_0 − sigma_0 ≤ 0 ∧ − scale_post + scale_post ≤ 0 ∧ scale_post − scale_post ≤ 0 ∧ − scale_0 + scale_0 ≤ 0 ∧ scale_0 − scale_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − maxarg2_post + maxarg2_post ≤ 0 ∧ maxarg2_post − maxarg2_post ≤ 0 ∧ − maxarg2_0 + maxarg2_0 ≤ 0 ∧ maxarg2_0 − maxarg2_0 ≤ 0 ∧ − maxarg1_post + maxarg1_post ≤ 0 ∧ maxarg1_post − maxarg1_post ≤ 0 ∧ − maxarg1_0 + maxarg1_0 ≤ 0 ∧ maxarg1_0 − maxarg1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0

8 Location Addition

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

8* 58 8: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tau_post + tau_post ≤ 0 ∧ tau_post − tau_post ≤ 0 ∧ − tau_0 + tau_0 ≤ 0 ∧ tau_0 − tau_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − sqrarg_post + sqrarg_post ≤ 0 ∧ sqrarg_post − sqrarg_post ≤ 0 ∧ − sqrarg_0 + sqrarg_0 ≤ 0 ∧ sqrarg_0 − sqrarg_0 ≤ 0 ∧ − sigma_post + sigma_post ≤ 0 ∧ sigma_post − sigma_post ≤ 0 ∧ − sigma_0 + sigma_0 ≤ 0 ∧ sigma_0 − sigma_0 ≤ 0 ∧ − scale_post + scale_post ≤ 0 ∧ scale_post − scale_post ≤ 0 ∧ − scale_0 + scale_0 ≤ 0 ∧ scale_0 − scale_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − maxarg2_post + maxarg2_post ≤ 0 ∧ maxarg2_post − maxarg2_post ≤ 0 ∧ − maxarg2_0 + maxarg2_0 ≤ 0 ∧ maxarg2_0 − maxarg2_0 ≤ 0 ∧ − maxarg1_post + maxarg1_post ≤ 0 ∧ maxarg1_post − maxarg1_post ≤ 0 ∧ − maxarg1_0 + maxarg1_0 ≤ 0 ∧ maxarg1_0 − maxarg1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0

9 Location Addition

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

8 56 8_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tau_post + tau_post ≤ 0 ∧ tau_post − tau_post ≤ 0 ∧ − tau_0 + tau_0 ≤ 0 ∧ tau_0 − tau_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − sqrarg_post + sqrarg_post ≤ 0 ∧ sqrarg_post − sqrarg_post ≤ 0 ∧ − sqrarg_0 + sqrarg_0 ≤ 0 ∧ sqrarg_0 − sqrarg_0 ≤ 0 ∧ − sigma_post + sigma_post ≤ 0 ∧ sigma_post − sigma_post ≤ 0 ∧ − sigma_0 + sigma_0 ≤ 0 ∧ sigma_0 − sigma_0 ≤ 0 ∧ − scale_post + scale_post ≤ 0 ∧ scale_post − scale_post ≤ 0 ∧ − scale_0 + scale_0 ≤ 0 ∧ scale_0 − scale_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − maxarg2_post + maxarg2_post ≤ 0 ∧ maxarg2_post − maxarg2_post ≤ 0 ∧ − maxarg2_0 + maxarg2_0 ≤ 0 ∧ maxarg2_0 − maxarg2_0 ≤ 0 ∧ − maxarg1_post + maxarg1_post ≤ 0 ∧ maxarg1_post − maxarg1_post ≤ 0 ∧ − maxarg1_0 + maxarg1_0 ≤ 0 ∧ maxarg1_0 − maxarg1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0

10 Location Addition

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

9* 65 9: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tau_post + tau_post ≤ 0 ∧ tau_post − tau_post ≤ 0 ∧ − tau_0 + tau_0 ≤ 0 ∧ tau_0 − tau_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − sqrarg_post + sqrarg_post ≤ 0 ∧ sqrarg_post − sqrarg_post ≤ 0 ∧ − sqrarg_0 + sqrarg_0 ≤ 0 ∧ sqrarg_0 − sqrarg_0 ≤ 0 ∧ − sigma_post + sigma_post ≤ 0 ∧ sigma_post − sigma_post ≤ 0 ∧ − sigma_0 + sigma_0 ≤ 0 ∧ sigma_0 − sigma_0 ≤ 0 ∧ − scale_post + scale_post ≤ 0 ∧ scale_post − scale_post ≤ 0 ∧ − scale_0 + scale_0 ≤ 0 ∧ scale_0 − scale_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − maxarg2_post + maxarg2_post ≤ 0 ∧ maxarg2_post − maxarg2_post ≤ 0 ∧ − maxarg2_0 + maxarg2_0 ≤ 0 ∧ maxarg2_0 − maxarg2_0 ≤ 0 ∧ − maxarg1_post + maxarg1_post ≤ 0 ∧ maxarg1_post − maxarg1_post ≤ 0 ∧ − maxarg1_0 + maxarg1_0 ≤ 0 ∧ maxarg1_0 − maxarg1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0

11 Location Addition

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

9 63 9_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tau_post + tau_post ≤ 0 ∧ tau_post − tau_post ≤ 0 ∧ − tau_0 + tau_0 ≤ 0 ∧ tau_0 − tau_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − sqrarg_post + sqrarg_post ≤ 0 ∧ sqrarg_post − sqrarg_post ≤ 0 ∧ − sqrarg_0 + sqrarg_0 ≤ 0 ∧ sqrarg_0 − sqrarg_0 ≤ 0 ∧ − sigma_post + sigma_post ≤ 0 ∧ sigma_post − sigma_post ≤ 0 ∧ − sigma_0 + sigma_0 ≤ 0 ∧ sigma_0 − sigma_0 ≤ 0 ∧ − scale_post + scale_post ≤ 0 ∧ scale_post − scale_post ≤ 0 ∧ − scale_0 + scale_0 ≤ 0 ∧ scale_0 − scale_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − maxarg2_post + maxarg2_post ≤ 0 ∧ maxarg2_post − maxarg2_post ≤ 0 ∧ − maxarg2_0 + maxarg2_0 ≤ 0 ∧ maxarg2_0 − maxarg2_0 ≤ 0 ∧ − maxarg1_post + maxarg1_post ≤ 0 ∧ maxarg1_post − maxarg1_post ≤ 0 ∧ − maxarg1_0 + maxarg1_0 ≤ 0 ∧ maxarg1_0 − maxarg1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0

12 Location Addition

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

10* 72 10: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tau_post + tau_post ≤ 0 ∧ tau_post − tau_post ≤ 0 ∧ − tau_0 + tau_0 ≤ 0 ∧ tau_0 − tau_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − sqrarg_post + sqrarg_post ≤ 0 ∧ sqrarg_post − sqrarg_post ≤ 0 ∧ − sqrarg_0 + sqrarg_0 ≤ 0 ∧ sqrarg_0 − sqrarg_0 ≤ 0 ∧ − sigma_post + sigma_post ≤ 0 ∧ sigma_post − sigma_post ≤ 0 ∧ − sigma_0 + sigma_0 ≤ 0 ∧ sigma_0 − sigma_0 ≤ 0 ∧ − scale_post + scale_post ≤ 0 ∧ scale_post − scale_post ≤ 0 ∧ − scale_0 + scale_0 ≤ 0 ∧ scale_0 − scale_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − maxarg2_post + maxarg2_post ≤ 0 ∧ maxarg2_post − maxarg2_post ≤ 0 ∧ − maxarg2_0 + maxarg2_0 ≤ 0 ∧ maxarg2_0 − maxarg2_0 ≤ 0 ∧ − maxarg1_post + maxarg1_post ≤ 0 ∧ maxarg1_post − maxarg1_post ≤ 0 ∧ − maxarg1_0 + maxarg1_0 ≤ 0 ∧ maxarg1_0 − maxarg1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0

13 Location Addition

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

10 70 10_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tau_post + tau_post ≤ 0 ∧ tau_post − tau_post ≤ 0 ∧ − tau_0 + tau_0 ≤ 0 ∧ tau_0 − tau_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − sqrarg_post + sqrarg_post ≤ 0 ∧ sqrarg_post − sqrarg_post ≤ 0 ∧ − sqrarg_0 + sqrarg_0 ≤ 0 ∧ sqrarg_0 − sqrarg_0 ≤ 0 ∧ − sigma_post + sigma_post ≤ 0 ∧ sigma_post − sigma_post ≤ 0 ∧ − sigma_0 + sigma_0 ≤ 0 ∧ sigma_0 − sigma_0 ≤ 0 ∧ − scale_post + scale_post ≤ 0 ∧ scale_post − scale_post ≤ 0 ∧ − scale_0 + scale_0 ≤ 0 ∧ scale_0 − scale_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − maxarg2_post + maxarg2_post ≤ 0 ∧ maxarg2_post − maxarg2_post ≤ 0 ∧ − maxarg2_0 + maxarg2_0 ≤ 0 ∧ maxarg2_0 − maxarg2_0 ≤ 0 ∧ − maxarg1_post + maxarg1_post ≤ 0 ∧ maxarg1_post − maxarg1_post ≤ 0 ∧ − maxarg1_0 + maxarg1_0 ≤ 0 ∧ maxarg1_0 − maxarg1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0

14 Location Addition

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

13* 79 13: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tau_post + tau_post ≤ 0 ∧ tau_post − tau_post ≤ 0 ∧ − tau_0 + tau_0 ≤ 0 ∧ tau_0 − tau_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − sqrarg_post + sqrarg_post ≤ 0 ∧ sqrarg_post − sqrarg_post ≤ 0 ∧ − sqrarg_0 + sqrarg_0 ≤ 0 ∧ sqrarg_0 − sqrarg_0 ≤ 0 ∧ − sigma_post + sigma_post ≤ 0 ∧ sigma_post − sigma_post ≤ 0 ∧ − sigma_0 + sigma_0 ≤ 0 ∧ sigma_0 − sigma_0 ≤ 0 ∧ − scale_post + scale_post ≤ 0 ∧ scale_post − scale_post ≤ 0 ∧ − scale_0 + scale_0 ≤ 0 ∧ scale_0 − scale_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − maxarg2_post + maxarg2_post ≤ 0 ∧ maxarg2_post − maxarg2_post ≤ 0 ∧ − maxarg2_0 + maxarg2_0 ≤ 0 ∧ maxarg2_0 − maxarg2_0 ≤ 0 ∧ − maxarg1_post + maxarg1_post ≤ 0 ∧ maxarg1_post − maxarg1_post ≤ 0 ∧ − maxarg1_0 + maxarg1_0 ≤ 0 ∧ maxarg1_0 − maxarg1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0

15 Location Addition

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

13 77 13_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tau_post + tau_post ≤ 0 ∧ tau_post − tau_post ≤ 0 ∧ − tau_0 + tau_0 ≤ 0 ∧ tau_0 − tau_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − sqrarg_post + sqrarg_post ≤ 0 ∧ sqrarg_post − sqrarg_post ≤ 0 ∧ − sqrarg_0 + sqrarg_0 ≤ 0 ∧ sqrarg_0 − sqrarg_0 ≤ 0 ∧ − sigma_post + sigma_post ≤ 0 ∧ sigma_post − sigma_post ≤ 0 ∧ − sigma_0 + sigma_0 ≤ 0 ∧ sigma_0 − sigma_0 ≤ 0 ∧ − scale_post + scale_post ≤ 0 ∧ scale_post − scale_post ≤ 0 ∧ − scale_0 + scale_0 ≤ 0 ∧ scale_0 − scale_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − maxarg2_post + maxarg2_post ≤ 0 ∧ maxarg2_post − maxarg2_post ≤ 0 ∧ − maxarg2_0 + maxarg2_0 ≤ 0 ∧ maxarg2_0 − maxarg2_0 ≤ 0 ∧ − maxarg1_post + maxarg1_post ≤ 0 ∧ maxarg1_post − maxarg1_post ≤ 0 ∧ − maxarg1_0 + maxarg1_0 ≤ 0 ∧ maxarg1_0 − maxarg1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0

16 Location Addition

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

16* 86 16: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tau_post + tau_post ≤ 0 ∧ tau_post − tau_post ≤ 0 ∧ − tau_0 + tau_0 ≤ 0 ∧ tau_0 − tau_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − sqrarg_post + sqrarg_post ≤ 0 ∧ sqrarg_post − sqrarg_post ≤ 0 ∧ − sqrarg_0 + sqrarg_0 ≤ 0 ∧ sqrarg_0 − sqrarg_0 ≤ 0 ∧ − sigma_post + sigma_post ≤ 0 ∧ sigma_post − sigma_post ≤ 0 ∧ − sigma_0 + sigma_0 ≤ 0 ∧ sigma_0 − sigma_0 ≤ 0 ∧ − scale_post + scale_post ≤ 0 ∧ scale_post − scale_post ≤ 0 ∧ − scale_0 + scale_0 ≤ 0 ∧ scale_0 − scale_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − maxarg2_post + maxarg2_post ≤ 0 ∧ maxarg2_post − maxarg2_post ≤ 0 ∧ − maxarg2_0 + maxarg2_0 ≤ 0 ∧ maxarg2_0 − maxarg2_0 ≤ 0 ∧ − maxarg1_post + maxarg1_post ≤ 0 ∧ maxarg1_post − maxarg1_post ≤ 0 ∧ − maxarg1_0 + maxarg1_0 ≤ 0 ∧ maxarg1_0 − maxarg1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0

17 Location Addition

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

16 84 16_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tau_post + tau_post ≤ 0 ∧ tau_post − tau_post ≤ 0 ∧ − tau_0 + tau_0 ≤ 0 ∧ tau_0 − tau_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − sqrarg_post + sqrarg_post ≤ 0 ∧ sqrarg_post − sqrarg_post ≤ 0 ∧ − sqrarg_0 + sqrarg_0 ≤ 0 ∧ sqrarg_0 − sqrarg_0 ≤ 0 ∧ − sigma_post + sigma_post ≤ 0 ∧ sigma_post − sigma_post ≤ 0 ∧ − sigma_0 + sigma_0 ≤ 0 ∧ sigma_0 − sigma_0 ≤ 0 ∧ − scale_post + scale_post ≤ 0 ∧ scale_post − scale_post ≤ 0 ∧ − scale_0 + scale_0 ≤ 0 ∧ scale_0 − scale_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − maxarg2_post + maxarg2_post ≤ 0 ∧ maxarg2_post − maxarg2_post ≤ 0 ∧ − maxarg2_0 + maxarg2_0 ≤ 0 ∧ maxarg2_0 − maxarg2_0 ≤ 0 ∧ − maxarg1_post + maxarg1_post ≤ 0 ∧ maxarg1_post − maxarg1_post ≤ 0 ∧ − maxarg1_0 + maxarg1_0 ≤ 0 ∧ maxarg1_0 − maxarg1_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0

18 SCC Decomposition

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

18.1 SCC Subproblem 1/1

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

18.1.1 Transition Removal

We remove transition 36 using the following ranking functions, which are bounded by −1.

0: −2⋅i_0 + 2⋅n_0
1: −2⋅i_0 + 2⋅n_0
5: −2⋅i_0 + 2⋅n_0
6: −2⋅i_0 + 2⋅n_0
7: −2⋅i_0 + 2⋅n_0
8: −2⋅i_0 + 2⋅n_0
9: −2⋅i_0 + 2⋅n_0
10: −2⋅i_0 + 2⋅n_0
11: −2⋅i_0 + 2⋅n_0
12: −2⋅i_0 + 2⋅n_0
13: −2⋅i_0 + 2⋅n_0
14: −2⋅i_0 + 2⋅n_0
15: −2⋅i_0 + 2⋅n_0
16: −2⋅i_0 + 2⋅n_0
17: −2⋅i_0 + 2⋅n_0
18: −2⋅i_0 + 2⋅n_0
19: −2⋅i_0 + 2⋅n_0
20: −2 − 2⋅i_0 + 2⋅n_0
21: −2 − 2⋅i_0 + 2⋅n_0
22: −2⋅i_0 + 2⋅n_0
23: −2⋅i_0 + 2⋅n_0
24: −2 − 2⋅i_0 + 2⋅n_0
25: −1 − 2⋅i_0 + 2⋅n_0
0_var_snapshot: −2⋅i_0 + 2⋅n_0
0*: −2⋅i_0 + 2⋅n_0
5_var_snapshot: −2⋅i_0 + 2⋅n_0
5*: −2⋅i_0 + 2⋅n_0
8_var_snapshot: −2⋅i_0 + 2⋅n_0
8*: −2⋅i_0 + 2⋅n_0
9_var_snapshot: −2⋅i_0 + 2⋅n_0
9*: −2⋅i_0 + 2⋅n_0
10_var_snapshot: −2⋅i_0 + 2⋅n_0
10*: −2⋅i_0 + 2⋅n_0
13_var_snapshot: −2⋅i_0 + 2⋅n_0
13*: −2⋅i_0 + 2⋅n_0
16_var_snapshot: −2⋅i_0 + 2⋅n_0
16*: −2⋅i_0 + 2⋅n_0

18.1.2 Transition Removal

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

0: 0
1: 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: 1
25: 1
0_var_snapshot: 0
0*: 0
5_var_snapshot: 0
5*: 0
8_var_snapshot: 0
8*: 0
9_var_snapshot: 0
9*: 0
10_var_snapshot: 0
10*: 0
13_var_snapshot: 0
13*: 0
16_var_snapshot: 0
16*: 0

18.1.3 Transition Removal

We remove transitions 33, 34 using the following ranking functions, which are bounded by 0.

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

18.1.4 Transition Removal

We remove transition 26 using the following ranking functions, which are bounded by −1.

0: −2⋅i_0 + 2⋅n_0
1: −2⋅i_0 + 2⋅n_0
5: −2⋅i_0 + 2⋅n_0
6: −2⋅i_0 + 2⋅n_0
7: −2⋅i_0 + 2⋅n_0
8: −2⋅i_0 + 2⋅n_0
9: −2⋅i_0 + 2⋅n_0
10: −2⋅i_0 + 2⋅n_0
11: −2⋅i_0 + 2⋅n_0
12: −2⋅i_0 + 2⋅n_0
13: −2⋅i_0 + 2⋅n_0
14: −2⋅i_0 + 2⋅n_0
15: −2⋅i_0 + 2⋅n_0
16: −2⋅i_0 + 2⋅n_0
17: −2⋅i_0 + 2⋅n_0
18: −2⋅i_0 + 2⋅n_0
19: −2⋅i_0 + 2⋅n_0
20: −1 − 2⋅i_0 + 2⋅n_0
21: −2 − 2⋅i_0 + 2⋅n_0
22: −2⋅i_0 + 2⋅n_0
23: −2⋅i_0 + 2⋅n_0
24: 0
25: 0
0_var_snapshot: −2⋅i_0 + 2⋅n_0
0*: −2⋅i_0 + 2⋅n_0
5_var_snapshot: −2⋅i_0 + 2⋅n_0
5*: −2⋅i_0 + 2⋅n_0
8_var_snapshot: −2⋅i_0 + 2⋅n_0
8*: −2⋅i_0 + 2⋅n_0
9_var_snapshot: −2⋅i_0 + 2⋅n_0
9*: −2⋅i_0 + 2⋅n_0
10_var_snapshot: −2⋅i_0 + 2⋅n_0
10*: −2⋅i_0 + 2⋅n_0
13_var_snapshot: −2⋅i_0 + 2⋅n_0
13*: −2⋅i_0 + 2⋅n_0
16_var_snapshot: −2⋅i_0 + 2⋅n_0
16*: −2⋅i_0 + 2⋅n_0

18.1.5 Transition Removal

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

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

18.1.6 Transition Removal

We remove transition 23 using the following ranking functions, which are bounded by −1.

0: −30⋅i_0 + 30⋅n_0
1: −30⋅i_0 + 30⋅n_0
5: −30⋅i_0 + 30⋅n_0
6: −30⋅i_0 + 30⋅n_0
7: −30⋅i_0 + 30⋅n_0
8: −30⋅i_0 + 30⋅n_0
9: −30⋅i_0 + 30⋅n_0
10: −30⋅i_0 + 30⋅n_0
11: −30⋅i_0 + 30⋅n_0
12: −30⋅i_0 + 30⋅n_0
13: −30⋅i_0 + 30⋅n_0
14: −30⋅i_0 + 30⋅n_0
15: −30⋅i_0 + 30⋅n_0
16: −30⋅i_0 + 30⋅n_0
17: −30⋅i_0 + 30⋅n_0
18: −30⋅i_0 + 30⋅n_0
19: −30⋅i_0 + 30⋅n_0
20: −2 − 30⋅i_0 + 30⋅n_0
21: −3 − 30⋅i_0 + 30⋅n_0
22: −1 − 30⋅i_0 + 30⋅n_0
23: −30⋅i_0 + 30⋅n_0
24: 0
25: 0
0_var_snapshot: −30⋅i_0 + 30⋅n_0
0*: −30⋅i_0 + 30⋅n_0
5_var_snapshot: −30⋅i_0 + 30⋅n_0
5*: −30⋅i_0 + 30⋅n_0
8_var_snapshot: −30⋅i_0 + 30⋅n_0
8*: −30⋅i_0 + 30⋅n_0
9_var_snapshot: −30⋅i_0 + 30⋅n_0
9*: −30⋅i_0 + 30⋅n_0
10_var_snapshot: −30⋅i_0 + 30⋅n_0
10*: −30⋅i_0 + 30⋅n_0
13_var_snapshot: −30⋅i_0 + 30⋅n_0
13*: −30⋅i_0 + 30⋅n_0
16_var_snapshot: −30⋅i_0 + 30⋅n_0
16*: −30⋅i_0 + 30⋅n_0

18.1.7 Transition Removal

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

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

18.1.8 Transition Removal

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

0: 2 − 23⋅k_0 + 23⋅n_0
1: −23⋅k_0 + 23⋅n_0
5: −2 − 23⋅k_0 + 23⋅n_0
6: −4 − 23⋅k_0 + 23⋅n_0
7: −6 − 23⋅k_0 + 23⋅n_0
8: −17 − 23⋅k_0 + 23⋅n_0
9: −4 − 23⋅k_0 + 23⋅n_0
10: −7 − 23⋅k_0 + 23⋅n_0
11: −9 − 23⋅k_0 + 23⋅n_0
12: −2 − 23⋅k_0 + 23⋅n_0
13: −23⋅k_0 + 23⋅n_0
14: −19 − 23⋅k_0 + 23⋅n_0
15: −20 − 23⋅k_0 + 23⋅n_0
16: −11 − 23⋅k_0 + 23⋅n_0
17: −13 − 23⋅k_0 + 23⋅n_0
18: −15 − 23⋅k_0 + 23⋅n_0
19: −14 − 23⋅k_0 + 23⋅n_0
20: −1 − 23⋅k_0 + 23⋅n_0
21: −2 − 23⋅k_0 + 23⋅n_0
22: −23⋅k_0 + 23⋅n_0
23: −5 − 23⋅k_0 + 23⋅n_0
24: 0
25: 0
0_var_snapshot: 1 − 23⋅k_0 + 23⋅n_0
0*: 3 − 23⋅k_0 + 23⋅n_0
5_var_snapshot: −3 − 23⋅k_0 + 23⋅n_0
5*: −1 − 23⋅k_0 + 23⋅n_0
8_var_snapshot: −18 − 23⋅k_0 + 23⋅n_0
8*: −16 − 23⋅k_0 + 23⋅n_0
9_var_snapshot: −5 − 23⋅k_0 + 23⋅n_0
9*: −3 − 23⋅k_0 + 23⋅n_0
10_var_snapshot: −8 − 23⋅k_0 + 23⋅n_0
10*: −6 − 23⋅k_0 + 23⋅n_0
13_var_snapshot: −1 − 23⋅k_0 + 23⋅n_0
13*: −23⋅k_0 + 24⋅n_0
16_var_snapshot: −12 − 23⋅k_0 + 23⋅n_0
16*: −10 − 23⋅k_0 + 23⋅n_0

18.1.9 Transition Removal

We remove transitions 42, 44, 49, 51, 56, 58, 63, 65, 70, 72, 77, 79, 84, 86, 0, 4, 5, 7, 8, 10, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 24, 25, 27, 28, 29, 30, 32, 35 using the following ranking functions, which are bounded by −19.

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

18.1.10 Splitting Cut-Point Transitions

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

18.1.10.1 Cut-Point Subproblem 1/7

Here we consider cut-point transition 41.

18.1.10.1.1 Splitting Cut-Point Transitions

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

18.1.10.2 Cut-Point Subproblem 2/7

Here we consider cut-point transition 48.

18.1.10.2.1 Splitting Cut-Point Transitions

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

18.1.10.3 Cut-Point Subproblem 3/7

Here we consider cut-point transition 55.

18.1.10.3.1 Splitting Cut-Point Transitions

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

18.1.10.4 Cut-Point Subproblem 4/7

Here we consider cut-point transition 62.

18.1.10.4.1 Splitting Cut-Point Transitions

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

18.1.10.5 Cut-Point Subproblem 5/7

Here we consider cut-point transition 69.

18.1.10.5.1 Splitting Cut-Point Transitions

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

18.1.10.6 Cut-Point Subproblem 6/7

Here we consider cut-point transition 76.

18.1.10.6.1 Splitting Cut-Point Transitions

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

18.1.10.7 Cut-Point Subproblem 7/7

Here we consider cut-point transition 83.

18.1.10.7.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert