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: TRUE
26: 2 − n_0 ≤ 0
27: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
3 42 3: − 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 49 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 56 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 63 11: − 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 70 17: − 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
20 77 20: − 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
24 84 24: − 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 3, 4, 5, 6, 16, 34, 41 using the following ranking functions, which are bounded by −29.

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

4 Location Addition

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

3* 45 3: − 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.

3 43 3_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.

8* 52 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

7 Location Addition

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

8 50 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

8 Location Addition

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

9* 59 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

9 Location Addition

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

9 57 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

10 Location Addition

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

11* 66 11: − 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.

11 64 11_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.

17* 73 17: − 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.

17 71 17_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.

20* 80 20: − 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.

20 78 20_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.

24* 87 24: − 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.

24 85 24_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, 2, 3, 7, 8, 9, 10, 11, 12, 13, 15, 16, 18, 19, 20, 21, 22, 23, 24, 26, 14, 17, 3_var_snapshot, 3*, 8_var_snapshot, 8*, 9_var_snapshot, 9*, 11_var_snapshot, 11*, 17_var_snapshot, 17*, 20_var_snapshot, 20*, 24_var_snapshot, 24* }.

18.1.1 Transition Removal

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

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

18.1.2 Transition Removal

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

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

18.1.3 Transition Removal

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

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

18.1.4 Transition Removal

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

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

18.1.5 Transition Removal

We remove transitions 43, 45, 11, 38, 39 using the following ranking functions, which are bounded by −12.

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

18.1.6 Transition Removal

We remove transitions 0, 8, 28 using the following ranking functions, which are bounded by −27.

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

18.1.7 Transition Removal

We remove transition 14 using the following ranking functions, which are bounded by −15.

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

18.1.8 Transition Removal

We remove transitions 50, 52, 57, 59, 64, 66, 71, 73, 78, 80, 85, 87, 2, 7, 9, 10, 12, 13, 15, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 29, 30, 32, 33, 35, 36, 37 using the following ranking functions, which are bounded by −19.

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

18.1.9 Splitting Cut-Point Transitions

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

18.1.9.1 Cut-Point Subproblem 1/7

Here we consider cut-point transition 42.

18.1.9.1.1 Splitting Cut-Point Transitions

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

18.1.9.2 Cut-Point Subproblem 2/7

Here we consider cut-point transition 49.

18.1.9.2.1 Splitting Cut-Point Transitions

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

18.1.9.3 Cut-Point Subproblem 3/7

Here we consider cut-point transition 56.

18.1.9.3.1 Splitting Cut-Point Transitions

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

18.1.9.4 Cut-Point Subproblem 4/7

Here we consider cut-point transition 63.

18.1.9.4.1 Splitting Cut-Point Transitions

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

18.1.9.5 Cut-Point Subproblem 5/7

Here we consider cut-point transition 70.

18.1.9.5.1 Splitting Cut-Point Transitions

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

18.1.9.6 Cut-Point Subproblem 6/7

Here we consider cut-point transition 77.

18.1.9.6.1 Splitting Cut-Point Transitions

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

18.1.9.7 Cut-Point Subproblem 7/7

Here we consider cut-point transition 84.

18.1.9.7.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert