LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
2 56 2: − x7_post + x7_post ≤ 0 ∧ x7_post − x7_post ≤ 0 ∧ − x7_0 + x7_0 ≤ 0 ∧ x7_0 − x7_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x5_post + x5_post ≤ 0 ∧ x5_post − x5_post ≤ 0 ∧ − x5_0 + x5_0 ≤ 0 ∧ x5_0 − x5_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX9_post + oldX9_post ≤ 0 ∧ oldX9_post − oldX9_post ≤ 0 ∧ − oldX9_0 + oldX9_0 ≤ 0 ∧ oldX9_0 − oldX9_0 ≤ 0 ∧ − oldX8_post + oldX8_post ≤ 0 ∧ oldX8_post − oldX8_post ≤ 0 ∧ − oldX8_0 + oldX8_0 ≤ 0 ∧ oldX8_0 − oldX8_0 ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX16_post + oldX16_post ≤ 0 ∧ oldX16_post − oldX16_post ≤ 0 ∧ − oldX16_0 + oldX16_0 ≤ 0 ∧ oldX16_0 − oldX16_0 ≤ 0 ∧ − oldX15_post + oldX15_post ≤ 0 ∧ oldX15_post − oldX15_post ≤ 0 ∧ − oldX15_0 + oldX15_0 ≤ 0 ∧ oldX15_0 − oldX15_0 ≤ 0 ∧ − oldX14_post + oldX14_post ≤ 0 ∧ oldX14_post − oldX14_post ≤ 0 ∧ − oldX14_0 + oldX14_0 ≤ 0 ∧ oldX14_0 − oldX14_0 ≤ 0 ∧ − oldX13_post + oldX13_post ≤ 0 ∧ oldX13_post − oldX13_post ≤ 0 ∧ − oldX13_0 + oldX13_0 ≤ 0 ∧ oldX13_0 − oldX13_0 ≤ 0 ∧ − oldX12_post + oldX12_post ≤ 0 ∧ oldX12_post − oldX12_post ≤ 0 ∧ − oldX12_0 + oldX12_0 ≤ 0 ∧ oldX12_0 − oldX12_0 ≤ 0 ∧ − oldX11_post + oldX11_post ≤ 0 ∧ oldX11_post − oldX11_post ≤ 0 ∧ − oldX11_0 + oldX11_0 ≤ 0 ∧ oldX11_0 − oldX11_0 ≤ 0 ∧ − oldX10_post + oldX10_post ≤ 0 ∧ oldX10_post − oldX10_post ≤ 0 ∧ − oldX10_0 + oldX10_0 ≤ 0 ∧ oldX10_0 − oldX10_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0
4 63 4: − x7_post + x7_post ≤ 0 ∧ x7_post − x7_post ≤ 0 ∧ − x7_0 + x7_0 ≤ 0 ∧ x7_0 − x7_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x5_post + x5_post ≤ 0 ∧ x5_post − x5_post ≤ 0 ∧ − x5_0 + x5_0 ≤ 0 ∧ x5_0 − x5_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX9_post + oldX9_post ≤ 0 ∧ oldX9_post − oldX9_post ≤ 0 ∧ − oldX9_0 + oldX9_0 ≤ 0 ∧ oldX9_0 − oldX9_0 ≤ 0 ∧ − oldX8_post + oldX8_post ≤ 0 ∧ oldX8_post − oldX8_post ≤ 0 ∧ − oldX8_0 + oldX8_0 ≤ 0 ∧ oldX8_0 − oldX8_0 ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX16_post + oldX16_post ≤ 0 ∧ oldX16_post − oldX16_post ≤ 0 ∧ − oldX16_0 + oldX16_0 ≤ 0 ∧ oldX16_0 − oldX16_0 ≤ 0 ∧ − oldX15_post + oldX15_post ≤ 0 ∧ oldX15_post − oldX15_post ≤ 0 ∧ − oldX15_0 + oldX15_0 ≤ 0 ∧ oldX15_0 − oldX15_0 ≤ 0 ∧ − oldX14_post + oldX14_post ≤ 0 ∧ oldX14_post − oldX14_post ≤ 0 ∧ − oldX14_0 + oldX14_0 ≤ 0 ∧ oldX14_0 − oldX14_0 ≤ 0 ∧ − oldX13_post + oldX13_post ≤ 0 ∧ oldX13_post − oldX13_post ≤ 0 ∧ − oldX13_0 + oldX13_0 ≤ 0 ∧ oldX13_0 − oldX13_0 ≤ 0 ∧ − oldX12_post + oldX12_post ≤ 0 ∧ oldX12_post − oldX12_post ≤ 0 ∧ − oldX12_0 + oldX12_0 ≤ 0 ∧ oldX12_0 − oldX12_0 ≤ 0 ∧ − oldX11_post + oldX11_post ≤ 0 ∧ oldX11_post − oldX11_post ≤ 0 ∧ − oldX11_0 + oldX11_0 ≤ 0 ∧ oldX11_0 − oldX11_0 ≤ 0 ∧ − oldX10_post + oldX10_post ≤ 0 ∧ oldX10_post − oldX10_post ≤ 0 ∧ − oldX10_0 + oldX10_0 ≤ 0 ∧ oldX10_0 − oldX10_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0
12 70 12: − x7_post + x7_post ≤ 0 ∧ x7_post − x7_post ≤ 0 ∧ − x7_0 + x7_0 ≤ 0 ∧ x7_0 − x7_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x5_post + x5_post ≤ 0 ∧ x5_post − x5_post ≤ 0 ∧ − x5_0 + x5_0 ≤ 0 ∧ x5_0 − x5_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX9_post + oldX9_post ≤ 0 ∧ oldX9_post − oldX9_post ≤ 0 ∧ − oldX9_0 + oldX9_0 ≤ 0 ∧ oldX9_0 − oldX9_0 ≤ 0 ∧ − oldX8_post + oldX8_post ≤ 0 ∧ oldX8_post − oldX8_post ≤ 0 ∧ − oldX8_0 + oldX8_0 ≤ 0 ∧ oldX8_0 − oldX8_0 ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX16_post + oldX16_post ≤ 0 ∧ oldX16_post − oldX16_post ≤ 0 ∧ − oldX16_0 + oldX16_0 ≤ 0 ∧ oldX16_0 − oldX16_0 ≤ 0 ∧ − oldX15_post + oldX15_post ≤ 0 ∧ oldX15_post − oldX15_post ≤ 0 ∧ − oldX15_0 + oldX15_0 ≤ 0 ∧ oldX15_0 − oldX15_0 ≤ 0 ∧ − oldX14_post + oldX14_post ≤ 0 ∧ oldX14_post − oldX14_post ≤ 0 ∧ − oldX14_0 + oldX14_0 ≤ 0 ∧ oldX14_0 − oldX14_0 ≤ 0 ∧ − oldX13_post + oldX13_post ≤ 0 ∧ oldX13_post − oldX13_post ≤ 0 ∧ − oldX13_0 + oldX13_0 ≤ 0 ∧ oldX13_0 − oldX13_0 ≤ 0 ∧ − oldX12_post + oldX12_post ≤ 0 ∧ oldX12_post − oldX12_post ≤ 0 ∧ − oldX12_0 + oldX12_0 ≤ 0 ∧ oldX12_0 − oldX12_0 ≤ 0 ∧ − oldX11_post + oldX11_post ≤ 0 ∧ oldX11_post − oldX11_post ≤ 0 ∧ − oldX11_0 + oldX11_0 ≤ 0 ∧ oldX11_0 − oldX11_0 ≤ 0 ∧ − oldX10_post + oldX10_post ≤ 0 ∧ oldX10_post − oldX10_post ≤ 0 ∧ − oldX10_0 + oldX10_0 ≤ 0 ∧ oldX10_0 − oldX10_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0
17 77 17: − x7_post + x7_post ≤ 0 ∧ x7_post − x7_post ≤ 0 ∧ − x7_0 + x7_0 ≤ 0 ∧ x7_0 − x7_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x5_post + x5_post ≤ 0 ∧ x5_post − x5_post ≤ 0 ∧ − x5_0 + x5_0 ≤ 0 ∧ x5_0 − x5_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX9_post + oldX9_post ≤ 0 ∧ oldX9_post − oldX9_post ≤ 0 ∧ − oldX9_0 + oldX9_0 ≤ 0 ∧ oldX9_0 − oldX9_0 ≤ 0 ∧ − oldX8_post + oldX8_post ≤ 0 ∧ oldX8_post − oldX8_post ≤ 0 ∧ − oldX8_0 + oldX8_0 ≤ 0 ∧ oldX8_0 − oldX8_0 ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX16_post + oldX16_post ≤ 0 ∧ oldX16_post − oldX16_post ≤ 0 ∧ − oldX16_0 + oldX16_0 ≤ 0 ∧ oldX16_0 − oldX16_0 ≤ 0 ∧ − oldX15_post + oldX15_post ≤ 0 ∧ oldX15_post − oldX15_post ≤ 0 ∧ − oldX15_0 + oldX15_0 ≤ 0 ∧ oldX15_0 − oldX15_0 ≤ 0 ∧ − oldX14_post + oldX14_post ≤ 0 ∧ oldX14_post − oldX14_post ≤ 0 ∧ − oldX14_0 + oldX14_0 ≤ 0 ∧ oldX14_0 − oldX14_0 ≤ 0 ∧ − oldX13_post + oldX13_post ≤ 0 ∧ oldX13_post − oldX13_post ≤ 0 ∧ − oldX13_0 + oldX13_0 ≤ 0 ∧ oldX13_0 − oldX13_0 ≤ 0 ∧ − oldX12_post + oldX12_post ≤ 0 ∧ oldX12_post − oldX12_post ≤ 0 ∧ − oldX12_0 + oldX12_0 ≤ 0 ∧ oldX12_0 − oldX12_0 ≤ 0 ∧ − oldX11_post + oldX11_post ≤ 0 ∧ oldX11_post − oldX11_post ≤ 0 ∧ − oldX11_0 + oldX11_0 ≤ 0 ∧ oldX11_0 − oldX11_0 ≤ 0 ∧ − oldX10_post + oldX10_post ≤ 0 ∧ oldX10_post − oldX10_post ≤ 0 ∧ − oldX10_0 + oldX10_0 ≤ 0 ∧ oldX10_0 − oldX10_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0
19 84 19: − x7_post + x7_post ≤ 0 ∧ x7_post − x7_post ≤ 0 ∧ − x7_0 + x7_0 ≤ 0 ∧ x7_0 − x7_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x5_post + x5_post ≤ 0 ∧ x5_post − x5_post ≤ 0 ∧ − x5_0 + x5_0 ≤ 0 ∧ x5_0 − x5_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX9_post + oldX9_post ≤ 0 ∧ oldX9_post − oldX9_post ≤ 0 ∧ − oldX9_0 + oldX9_0 ≤ 0 ∧ oldX9_0 − oldX9_0 ≤ 0 ∧ − oldX8_post + oldX8_post ≤ 0 ∧ oldX8_post − oldX8_post ≤ 0 ∧ − oldX8_0 + oldX8_0 ≤ 0 ∧ oldX8_0 − oldX8_0 ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX16_post + oldX16_post ≤ 0 ∧ oldX16_post − oldX16_post ≤ 0 ∧ − oldX16_0 + oldX16_0 ≤ 0 ∧ oldX16_0 − oldX16_0 ≤ 0 ∧ − oldX15_post + oldX15_post ≤ 0 ∧ oldX15_post − oldX15_post ≤ 0 ∧ − oldX15_0 + oldX15_0 ≤ 0 ∧ oldX15_0 − oldX15_0 ≤ 0 ∧ − oldX14_post + oldX14_post ≤ 0 ∧ oldX14_post − oldX14_post ≤ 0 ∧ − oldX14_0 + oldX14_0 ≤ 0 ∧ oldX14_0 − oldX14_0 ≤ 0 ∧ − oldX13_post + oldX13_post ≤ 0 ∧ oldX13_post − oldX13_post ≤ 0 ∧ − oldX13_0 + oldX13_0 ≤ 0 ∧ oldX13_0 − oldX13_0 ≤ 0 ∧ − oldX12_post + oldX12_post ≤ 0 ∧ oldX12_post − oldX12_post ≤ 0 ∧ − oldX12_0 + oldX12_0 ≤ 0 ∧ oldX12_0 − oldX12_0 ≤ 0 ∧ − oldX11_post + oldX11_post ≤ 0 ∧ oldX11_post − oldX11_post ≤ 0 ∧ − oldX11_0 + oldX11_0 ≤ 0 ∧ oldX11_0 − oldX11_0 ≤ 0 ∧ − oldX10_post + oldX10_post ≤ 0 ∧ oldX10_post − oldX10_post ≤ 0 ∧ − oldX10_0 + oldX10_0 ≤ 0 ∧ oldX10_0 − oldX10_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0
and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 0, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 14, 15, 16, 17, 19, 21, 22, 28, 29, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55 using the following ranking functions, which are bounded by −45.

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

3 Location Addition

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

2* 59 2: − x7_post + x7_post ≤ 0 ∧ x7_post − x7_post ≤ 0 ∧ − x7_0 + x7_0 ≤ 0 ∧ x7_0 − x7_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x5_post + x5_post ≤ 0 ∧ x5_post − x5_post ≤ 0 ∧ − x5_0 + x5_0 ≤ 0 ∧ x5_0 − x5_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX9_post + oldX9_post ≤ 0 ∧ oldX9_post − oldX9_post ≤ 0 ∧ − oldX9_0 + oldX9_0 ≤ 0 ∧ oldX9_0 − oldX9_0 ≤ 0 ∧ − oldX8_post + oldX8_post ≤ 0 ∧ oldX8_post − oldX8_post ≤ 0 ∧ − oldX8_0 + oldX8_0 ≤ 0 ∧ oldX8_0 − oldX8_0 ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX16_post + oldX16_post ≤ 0 ∧ oldX16_post − oldX16_post ≤ 0 ∧ − oldX16_0 + oldX16_0 ≤ 0 ∧ oldX16_0 − oldX16_0 ≤ 0 ∧ − oldX15_post + oldX15_post ≤ 0 ∧ oldX15_post − oldX15_post ≤ 0 ∧ − oldX15_0 + oldX15_0 ≤ 0 ∧ oldX15_0 − oldX15_0 ≤ 0 ∧ − oldX14_post + oldX14_post ≤ 0 ∧ oldX14_post − oldX14_post ≤ 0 ∧ − oldX14_0 + oldX14_0 ≤ 0 ∧ oldX14_0 − oldX14_0 ≤ 0 ∧ − oldX13_post + oldX13_post ≤ 0 ∧ oldX13_post − oldX13_post ≤ 0 ∧ − oldX13_0 + oldX13_0 ≤ 0 ∧ oldX13_0 − oldX13_0 ≤ 0 ∧ − oldX12_post + oldX12_post ≤ 0 ∧ oldX12_post − oldX12_post ≤ 0 ∧ − oldX12_0 + oldX12_0 ≤ 0 ∧ oldX12_0 − oldX12_0 ≤ 0 ∧ − oldX11_post + oldX11_post ≤ 0 ∧ oldX11_post − oldX11_post ≤ 0 ∧ − oldX11_0 + oldX11_0 ≤ 0 ∧ oldX11_0 − oldX11_0 ≤ 0 ∧ − oldX10_post + oldX10_post ≤ 0 ∧ oldX10_post − oldX10_post ≤ 0 ∧ − oldX10_0 + oldX10_0 ≤ 0 ∧ oldX10_0 − oldX10_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0

4 Location Addition

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

2 57 2_var_snapshot: − x7_post + x7_post ≤ 0 ∧ x7_post − x7_post ≤ 0 ∧ − x7_0 + x7_0 ≤ 0 ∧ x7_0 − x7_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x5_post + x5_post ≤ 0 ∧ x5_post − x5_post ≤ 0 ∧ − x5_0 + x5_0 ≤ 0 ∧ x5_0 − x5_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX9_post + oldX9_post ≤ 0 ∧ oldX9_post − oldX9_post ≤ 0 ∧ − oldX9_0 + oldX9_0 ≤ 0 ∧ oldX9_0 − oldX9_0 ≤ 0 ∧ − oldX8_post + oldX8_post ≤ 0 ∧ oldX8_post − oldX8_post ≤ 0 ∧ − oldX8_0 + oldX8_0 ≤ 0 ∧ oldX8_0 − oldX8_0 ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX16_post + oldX16_post ≤ 0 ∧ oldX16_post − oldX16_post ≤ 0 ∧ − oldX16_0 + oldX16_0 ≤ 0 ∧ oldX16_0 − oldX16_0 ≤ 0 ∧ − oldX15_post + oldX15_post ≤ 0 ∧ oldX15_post − oldX15_post ≤ 0 ∧ − oldX15_0 + oldX15_0 ≤ 0 ∧ oldX15_0 − oldX15_0 ≤ 0 ∧ − oldX14_post + oldX14_post ≤ 0 ∧ oldX14_post − oldX14_post ≤ 0 ∧ − oldX14_0 + oldX14_0 ≤ 0 ∧ oldX14_0 − oldX14_0 ≤ 0 ∧ − oldX13_post + oldX13_post ≤ 0 ∧ oldX13_post − oldX13_post ≤ 0 ∧ − oldX13_0 + oldX13_0 ≤ 0 ∧ oldX13_0 − oldX13_0 ≤ 0 ∧ − oldX12_post + oldX12_post ≤ 0 ∧ oldX12_post − oldX12_post ≤ 0 ∧ − oldX12_0 + oldX12_0 ≤ 0 ∧ oldX12_0 − oldX12_0 ≤ 0 ∧ − oldX11_post + oldX11_post ≤ 0 ∧ oldX11_post − oldX11_post ≤ 0 ∧ − oldX11_0 + oldX11_0 ≤ 0 ∧ oldX11_0 − oldX11_0 ≤ 0 ∧ − oldX10_post + oldX10_post ≤ 0 ∧ oldX10_post − oldX10_post ≤ 0 ∧ − oldX10_0 + oldX10_0 ≤ 0 ∧ oldX10_0 − oldX10_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0

5 Location Addition

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

4* 66 4: − x7_post + x7_post ≤ 0 ∧ x7_post − x7_post ≤ 0 ∧ − x7_0 + x7_0 ≤ 0 ∧ x7_0 − x7_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x5_post + x5_post ≤ 0 ∧ x5_post − x5_post ≤ 0 ∧ − x5_0 + x5_0 ≤ 0 ∧ x5_0 − x5_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX9_post + oldX9_post ≤ 0 ∧ oldX9_post − oldX9_post ≤ 0 ∧ − oldX9_0 + oldX9_0 ≤ 0 ∧ oldX9_0 − oldX9_0 ≤ 0 ∧ − oldX8_post + oldX8_post ≤ 0 ∧ oldX8_post − oldX8_post ≤ 0 ∧ − oldX8_0 + oldX8_0 ≤ 0 ∧ oldX8_0 − oldX8_0 ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX16_post + oldX16_post ≤ 0 ∧ oldX16_post − oldX16_post ≤ 0 ∧ − oldX16_0 + oldX16_0 ≤ 0 ∧ oldX16_0 − oldX16_0 ≤ 0 ∧ − oldX15_post + oldX15_post ≤ 0 ∧ oldX15_post − oldX15_post ≤ 0 ∧ − oldX15_0 + oldX15_0 ≤ 0 ∧ oldX15_0 − oldX15_0 ≤ 0 ∧ − oldX14_post + oldX14_post ≤ 0 ∧ oldX14_post − oldX14_post ≤ 0 ∧ − oldX14_0 + oldX14_0 ≤ 0 ∧ oldX14_0 − oldX14_0 ≤ 0 ∧ − oldX13_post + oldX13_post ≤ 0 ∧ oldX13_post − oldX13_post ≤ 0 ∧ − oldX13_0 + oldX13_0 ≤ 0 ∧ oldX13_0 − oldX13_0 ≤ 0 ∧ − oldX12_post + oldX12_post ≤ 0 ∧ oldX12_post − oldX12_post ≤ 0 ∧ − oldX12_0 + oldX12_0 ≤ 0 ∧ oldX12_0 − oldX12_0 ≤ 0 ∧ − oldX11_post + oldX11_post ≤ 0 ∧ oldX11_post − oldX11_post ≤ 0 ∧ − oldX11_0 + oldX11_0 ≤ 0 ∧ oldX11_0 − oldX11_0 ≤ 0 ∧ − oldX10_post + oldX10_post ≤ 0 ∧ oldX10_post − oldX10_post ≤ 0 ∧ − oldX10_0 + oldX10_0 ≤ 0 ∧ oldX10_0 − oldX10_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0

6 Location Addition

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

4 64 4_var_snapshot: − x7_post + x7_post ≤ 0 ∧ x7_post − x7_post ≤ 0 ∧ − x7_0 + x7_0 ≤ 0 ∧ x7_0 − x7_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x5_post + x5_post ≤ 0 ∧ x5_post − x5_post ≤ 0 ∧ − x5_0 + x5_0 ≤ 0 ∧ x5_0 − x5_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX9_post + oldX9_post ≤ 0 ∧ oldX9_post − oldX9_post ≤ 0 ∧ − oldX9_0 + oldX9_0 ≤ 0 ∧ oldX9_0 − oldX9_0 ≤ 0 ∧ − oldX8_post + oldX8_post ≤ 0 ∧ oldX8_post − oldX8_post ≤ 0 ∧ − oldX8_0 + oldX8_0 ≤ 0 ∧ oldX8_0 − oldX8_0 ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX16_post + oldX16_post ≤ 0 ∧ oldX16_post − oldX16_post ≤ 0 ∧ − oldX16_0 + oldX16_0 ≤ 0 ∧ oldX16_0 − oldX16_0 ≤ 0 ∧ − oldX15_post + oldX15_post ≤ 0 ∧ oldX15_post − oldX15_post ≤ 0 ∧ − oldX15_0 + oldX15_0 ≤ 0 ∧ oldX15_0 − oldX15_0 ≤ 0 ∧ − oldX14_post + oldX14_post ≤ 0 ∧ oldX14_post − oldX14_post ≤ 0 ∧ − oldX14_0 + oldX14_0 ≤ 0 ∧ oldX14_0 − oldX14_0 ≤ 0 ∧ − oldX13_post + oldX13_post ≤ 0 ∧ oldX13_post − oldX13_post ≤ 0 ∧ − oldX13_0 + oldX13_0 ≤ 0 ∧ oldX13_0 − oldX13_0 ≤ 0 ∧ − oldX12_post + oldX12_post ≤ 0 ∧ oldX12_post − oldX12_post ≤ 0 ∧ − oldX12_0 + oldX12_0 ≤ 0 ∧ oldX12_0 − oldX12_0 ≤ 0 ∧ − oldX11_post + oldX11_post ≤ 0 ∧ oldX11_post − oldX11_post ≤ 0 ∧ − oldX11_0 + oldX11_0 ≤ 0 ∧ oldX11_0 − oldX11_0 ≤ 0 ∧ − oldX10_post + oldX10_post ≤ 0 ∧ oldX10_post − oldX10_post ≤ 0 ∧ − oldX10_0 + oldX10_0 ≤ 0 ∧ oldX10_0 − oldX10_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0

7 Location Addition

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

12* 73 12: − x7_post + x7_post ≤ 0 ∧ x7_post − x7_post ≤ 0 ∧ − x7_0 + x7_0 ≤ 0 ∧ x7_0 − x7_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x5_post + x5_post ≤ 0 ∧ x5_post − x5_post ≤ 0 ∧ − x5_0 + x5_0 ≤ 0 ∧ x5_0 − x5_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX9_post + oldX9_post ≤ 0 ∧ oldX9_post − oldX9_post ≤ 0 ∧ − oldX9_0 + oldX9_0 ≤ 0 ∧ oldX9_0 − oldX9_0 ≤ 0 ∧ − oldX8_post + oldX8_post ≤ 0 ∧ oldX8_post − oldX8_post ≤ 0 ∧ − oldX8_0 + oldX8_0 ≤ 0 ∧ oldX8_0 − oldX8_0 ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX16_post + oldX16_post ≤ 0 ∧ oldX16_post − oldX16_post ≤ 0 ∧ − oldX16_0 + oldX16_0 ≤ 0 ∧ oldX16_0 − oldX16_0 ≤ 0 ∧ − oldX15_post + oldX15_post ≤ 0 ∧ oldX15_post − oldX15_post ≤ 0 ∧ − oldX15_0 + oldX15_0 ≤ 0 ∧ oldX15_0 − oldX15_0 ≤ 0 ∧ − oldX14_post + oldX14_post ≤ 0 ∧ oldX14_post − oldX14_post ≤ 0 ∧ − oldX14_0 + oldX14_0 ≤ 0 ∧ oldX14_0 − oldX14_0 ≤ 0 ∧ − oldX13_post + oldX13_post ≤ 0 ∧ oldX13_post − oldX13_post ≤ 0 ∧ − oldX13_0 + oldX13_0 ≤ 0 ∧ oldX13_0 − oldX13_0 ≤ 0 ∧ − oldX12_post + oldX12_post ≤ 0 ∧ oldX12_post − oldX12_post ≤ 0 ∧ − oldX12_0 + oldX12_0 ≤ 0 ∧ oldX12_0 − oldX12_0 ≤ 0 ∧ − oldX11_post + oldX11_post ≤ 0 ∧ oldX11_post − oldX11_post ≤ 0 ∧ − oldX11_0 + oldX11_0 ≤ 0 ∧ oldX11_0 − oldX11_0 ≤ 0 ∧ − oldX10_post + oldX10_post ≤ 0 ∧ oldX10_post − oldX10_post ≤ 0 ∧ − oldX10_0 + oldX10_0 ≤ 0 ∧ oldX10_0 − oldX10_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0

8 Location Addition

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

12 71 12_var_snapshot: − x7_post + x7_post ≤ 0 ∧ x7_post − x7_post ≤ 0 ∧ − x7_0 + x7_0 ≤ 0 ∧ x7_0 − x7_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x5_post + x5_post ≤ 0 ∧ x5_post − x5_post ≤ 0 ∧ − x5_0 + x5_0 ≤ 0 ∧ x5_0 − x5_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX9_post + oldX9_post ≤ 0 ∧ oldX9_post − oldX9_post ≤ 0 ∧ − oldX9_0 + oldX9_0 ≤ 0 ∧ oldX9_0 − oldX9_0 ≤ 0 ∧ − oldX8_post + oldX8_post ≤ 0 ∧ oldX8_post − oldX8_post ≤ 0 ∧ − oldX8_0 + oldX8_0 ≤ 0 ∧ oldX8_0 − oldX8_0 ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX16_post + oldX16_post ≤ 0 ∧ oldX16_post − oldX16_post ≤ 0 ∧ − oldX16_0 + oldX16_0 ≤ 0 ∧ oldX16_0 − oldX16_0 ≤ 0 ∧ − oldX15_post + oldX15_post ≤ 0 ∧ oldX15_post − oldX15_post ≤ 0 ∧ − oldX15_0 + oldX15_0 ≤ 0 ∧ oldX15_0 − oldX15_0 ≤ 0 ∧ − oldX14_post + oldX14_post ≤ 0 ∧ oldX14_post − oldX14_post ≤ 0 ∧ − oldX14_0 + oldX14_0 ≤ 0 ∧ oldX14_0 − oldX14_0 ≤ 0 ∧ − oldX13_post + oldX13_post ≤ 0 ∧ oldX13_post − oldX13_post ≤ 0 ∧ − oldX13_0 + oldX13_0 ≤ 0 ∧ oldX13_0 − oldX13_0 ≤ 0 ∧ − oldX12_post + oldX12_post ≤ 0 ∧ oldX12_post − oldX12_post ≤ 0 ∧ − oldX12_0 + oldX12_0 ≤ 0 ∧ oldX12_0 − oldX12_0 ≤ 0 ∧ − oldX11_post + oldX11_post ≤ 0 ∧ oldX11_post − oldX11_post ≤ 0 ∧ − oldX11_0 + oldX11_0 ≤ 0 ∧ oldX11_0 − oldX11_0 ≤ 0 ∧ − oldX10_post + oldX10_post ≤ 0 ∧ oldX10_post − oldX10_post ≤ 0 ∧ − oldX10_0 + oldX10_0 ≤ 0 ∧ oldX10_0 − oldX10_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0

9 Location Addition

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

17* 80 17: − x7_post + x7_post ≤ 0 ∧ x7_post − x7_post ≤ 0 ∧ − x7_0 + x7_0 ≤ 0 ∧ x7_0 − x7_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x5_post + x5_post ≤ 0 ∧ x5_post − x5_post ≤ 0 ∧ − x5_0 + x5_0 ≤ 0 ∧ x5_0 − x5_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX9_post + oldX9_post ≤ 0 ∧ oldX9_post − oldX9_post ≤ 0 ∧ − oldX9_0 + oldX9_0 ≤ 0 ∧ oldX9_0 − oldX9_0 ≤ 0 ∧ − oldX8_post + oldX8_post ≤ 0 ∧ oldX8_post − oldX8_post ≤ 0 ∧ − oldX8_0 + oldX8_0 ≤ 0 ∧ oldX8_0 − oldX8_0 ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX16_post + oldX16_post ≤ 0 ∧ oldX16_post − oldX16_post ≤ 0 ∧ − oldX16_0 + oldX16_0 ≤ 0 ∧ oldX16_0 − oldX16_0 ≤ 0 ∧ − oldX15_post + oldX15_post ≤ 0 ∧ oldX15_post − oldX15_post ≤ 0 ∧ − oldX15_0 + oldX15_0 ≤ 0 ∧ oldX15_0 − oldX15_0 ≤ 0 ∧ − oldX14_post + oldX14_post ≤ 0 ∧ oldX14_post − oldX14_post ≤ 0 ∧ − oldX14_0 + oldX14_0 ≤ 0 ∧ oldX14_0 − oldX14_0 ≤ 0 ∧ − oldX13_post + oldX13_post ≤ 0 ∧ oldX13_post − oldX13_post ≤ 0 ∧ − oldX13_0 + oldX13_0 ≤ 0 ∧ oldX13_0 − oldX13_0 ≤ 0 ∧ − oldX12_post + oldX12_post ≤ 0 ∧ oldX12_post − oldX12_post ≤ 0 ∧ − oldX12_0 + oldX12_0 ≤ 0 ∧ oldX12_0 − oldX12_0 ≤ 0 ∧ − oldX11_post + oldX11_post ≤ 0 ∧ oldX11_post − oldX11_post ≤ 0 ∧ − oldX11_0 + oldX11_0 ≤ 0 ∧ oldX11_0 − oldX11_0 ≤ 0 ∧ − oldX10_post + oldX10_post ≤ 0 ∧ oldX10_post − oldX10_post ≤ 0 ∧ − oldX10_0 + oldX10_0 ≤ 0 ∧ oldX10_0 − oldX10_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0

10 Location Addition

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

17 78 17_var_snapshot: − x7_post + x7_post ≤ 0 ∧ x7_post − x7_post ≤ 0 ∧ − x7_0 + x7_0 ≤ 0 ∧ x7_0 − x7_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x5_post + x5_post ≤ 0 ∧ x5_post − x5_post ≤ 0 ∧ − x5_0 + x5_0 ≤ 0 ∧ x5_0 − x5_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX9_post + oldX9_post ≤ 0 ∧ oldX9_post − oldX9_post ≤ 0 ∧ − oldX9_0 + oldX9_0 ≤ 0 ∧ oldX9_0 − oldX9_0 ≤ 0 ∧ − oldX8_post + oldX8_post ≤ 0 ∧ oldX8_post − oldX8_post ≤ 0 ∧ − oldX8_0 + oldX8_0 ≤ 0 ∧ oldX8_0 − oldX8_0 ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX16_post + oldX16_post ≤ 0 ∧ oldX16_post − oldX16_post ≤ 0 ∧ − oldX16_0 + oldX16_0 ≤ 0 ∧ oldX16_0 − oldX16_0 ≤ 0 ∧ − oldX15_post + oldX15_post ≤ 0 ∧ oldX15_post − oldX15_post ≤ 0 ∧ − oldX15_0 + oldX15_0 ≤ 0 ∧ oldX15_0 − oldX15_0 ≤ 0 ∧ − oldX14_post + oldX14_post ≤ 0 ∧ oldX14_post − oldX14_post ≤ 0 ∧ − oldX14_0 + oldX14_0 ≤ 0 ∧ oldX14_0 − oldX14_0 ≤ 0 ∧ − oldX13_post + oldX13_post ≤ 0 ∧ oldX13_post − oldX13_post ≤ 0 ∧ − oldX13_0 + oldX13_0 ≤ 0 ∧ oldX13_0 − oldX13_0 ≤ 0 ∧ − oldX12_post + oldX12_post ≤ 0 ∧ oldX12_post − oldX12_post ≤ 0 ∧ − oldX12_0 + oldX12_0 ≤ 0 ∧ oldX12_0 − oldX12_0 ≤ 0 ∧ − oldX11_post + oldX11_post ≤ 0 ∧ oldX11_post − oldX11_post ≤ 0 ∧ − oldX11_0 + oldX11_0 ≤ 0 ∧ oldX11_0 − oldX11_0 ≤ 0 ∧ − oldX10_post + oldX10_post ≤ 0 ∧ oldX10_post − oldX10_post ≤ 0 ∧ − oldX10_0 + oldX10_0 ≤ 0 ∧ oldX10_0 − oldX10_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0

11 Location Addition

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

19* 87 19: − x7_post + x7_post ≤ 0 ∧ x7_post − x7_post ≤ 0 ∧ − x7_0 + x7_0 ≤ 0 ∧ x7_0 − x7_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x5_post + x5_post ≤ 0 ∧ x5_post − x5_post ≤ 0 ∧ − x5_0 + x5_0 ≤ 0 ∧ x5_0 − x5_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX9_post + oldX9_post ≤ 0 ∧ oldX9_post − oldX9_post ≤ 0 ∧ − oldX9_0 + oldX9_0 ≤ 0 ∧ oldX9_0 − oldX9_0 ≤ 0 ∧ − oldX8_post + oldX8_post ≤ 0 ∧ oldX8_post − oldX8_post ≤ 0 ∧ − oldX8_0 + oldX8_0 ≤ 0 ∧ oldX8_0 − oldX8_0 ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX16_post + oldX16_post ≤ 0 ∧ oldX16_post − oldX16_post ≤ 0 ∧ − oldX16_0 + oldX16_0 ≤ 0 ∧ oldX16_0 − oldX16_0 ≤ 0 ∧ − oldX15_post + oldX15_post ≤ 0 ∧ oldX15_post − oldX15_post ≤ 0 ∧ − oldX15_0 + oldX15_0 ≤ 0 ∧ oldX15_0 − oldX15_0 ≤ 0 ∧ − oldX14_post + oldX14_post ≤ 0 ∧ oldX14_post − oldX14_post ≤ 0 ∧ − oldX14_0 + oldX14_0 ≤ 0 ∧ oldX14_0 − oldX14_0 ≤ 0 ∧ − oldX13_post + oldX13_post ≤ 0 ∧ oldX13_post − oldX13_post ≤ 0 ∧ − oldX13_0 + oldX13_0 ≤ 0 ∧ oldX13_0 − oldX13_0 ≤ 0 ∧ − oldX12_post + oldX12_post ≤ 0 ∧ oldX12_post − oldX12_post ≤ 0 ∧ − oldX12_0 + oldX12_0 ≤ 0 ∧ oldX12_0 − oldX12_0 ≤ 0 ∧ − oldX11_post + oldX11_post ≤ 0 ∧ oldX11_post − oldX11_post ≤ 0 ∧ − oldX11_0 + oldX11_0 ≤ 0 ∧ oldX11_0 − oldX11_0 ≤ 0 ∧ − oldX10_post + oldX10_post ≤ 0 ∧ oldX10_post − oldX10_post ≤ 0 ∧ − oldX10_0 + oldX10_0 ≤ 0 ∧ oldX10_0 − oldX10_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0

12 Location Addition

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

19 85 19_var_snapshot: − x7_post + x7_post ≤ 0 ∧ x7_post − x7_post ≤ 0 ∧ − x7_0 + x7_0 ≤ 0 ∧ x7_0 − x7_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x5_post + x5_post ≤ 0 ∧ x5_post − x5_post ≤ 0 ∧ − x5_0 + x5_0 ≤ 0 ∧ x5_0 − x5_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX9_post + oldX9_post ≤ 0 ∧ oldX9_post − oldX9_post ≤ 0 ∧ − oldX9_0 + oldX9_0 ≤ 0 ∧ oldX9_0 − oldX9_0 ≤ 0 ∧ − oldX8_post + oldX8_post ≤ 0 ∧ oldX8_post − oldX8_post ≤ 0 ∧ − oldX8_0 + oldX8_0 ≤ 0 ∧ oldX8_0 − oldX8_0 ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX16_post + oldX16_post ≤ 0 ∧ oldX16_post − oldX16_post ≤ 0 ∧ − oldX16_0 + oldX16_0 ≤ 0 ∧ oldX16_0 − oldX16_0 ≤ 0 ∧ − oldX15_post + oldX15_post ≤ 0 ∧ oldX15_post − oldX15_post ≤ 0 ∧ − oldX15_0 + oldX15_0 ≤ 0 ∧ oldX15_0 − oldX15_0 ≤ 0 ∧ − oldX14_post + oldX14_post ≤ 0 ∧ oldX14_post − oldX14_post ≤ 0 ∧ − oldX14_0 + oldX14_0 ≤ 0 ∧ oldX14_0 − oldX14_0 ≤ 0 ∧ − oldX13_post + oldX13_post ≤ 0 ∧ oldX13_post − oldX13_post ≤ 0 ∧ − oldX13_0 + oldX13_0 ≤ 0 ∧ oldX13_0 − oldX13_0 ≤ 0 ∧ − oldX12_post + oldX12_post ≤ 0 ∧ oldX12_post − oldX12_post ≤ 0 ∧ − oldX12_0 + oldX12_0 ≤ 0 ∧ oldX12_0 − oldX12_0 ≤ 0 ∧ − oldX11_post + oldX11_post ≤ 0 ∧ oldX11_post − oldX11_post ≤ 0 ∧ − oldX11_0 + oldX11_0 ≤ 0 ∧ oldX11_0 − oldX11_0 ≤ 0 ∧ − oldX10_post + oldX10_post ≤ 0 ∧ oldX10_post − oldX10_post ≤ 0 ∧ − oldX10_0 + oldX10_0 ≤ 0 ∧ oldX10_0 − oldX10_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0

13 SCC Decomposition

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

13.1 SCC Subproblem 1/4

Here we consider the SCC { 11, 12, 12_var_snapshot, 12* }.

13.1.1 Transition Removal

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

11: 3 + 4⋅x7_0
12: 1 + 4⋅x6_0
12_var_snapshot: 4⋅x6_0
12*: 2 + 4⋅x6_0

13.1.2 Transition Removal

We remove transitions 71, 73, 13 using the following ranking functions, which are bounded by −1.

11: 2
12: 0
12_var_snapshot: −1
12*: 1

13.1.3 Splitting Cut-Point Transitions

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

13.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 70.

13.1.3.1.1 Splitting Cut-Point Transitions

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

13.2 SCC Subproblem 2/4

Here we consider the SCC { 16, 17, 17_var_snapshot, 17* }.

13.2.1 Transition Removal

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

16: −16 + 4⋅x5_0
17: 16 + 4⋅x5_0
17_var_snapshot: 4⋅x5_0
17*: 32 + 4⋅x5_0

13.2.2 Transition Removal

We remove transitions 78, 80, 20 using the following ranking functions, which are bounded by −2.

16: 1
17: −1
17_var_snapshot: −2
17*: 0

13.2.3 Splitting Cut-Point Transitions

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

13.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 77.

13.2.3.1.1 Splitting Cut-Point Transitions

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

13.3 SCC Subproblem 3/4

Here we consider the SCC { 0, 2, 18, 19, 20, 2_var_snapshot, 2*, 19_var_snapshot, 19* }.

13.3.1 Transition Removal

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

0: −49964 + 9⋅x4_0
2: −49966 + 9⋅x4_0
18: −49963 + 9⋅x5_0
19: 9⋅x5_0
20: 9⋅x5_0
2_var_snapshot: −49967 + 9⋅x4_0
2*: −49965 + 9⋅x4_0
19_var_snapshot: 9⋅x5_0
19*: 9⋅x5_0

13.3.2 Transition Removal

We remove transitions 57, 26, 30 using the following ranking functions, which are bounded by −1384.

0: −1393 + 4⋅oldX6_post
2: 1
18: −1392 + 4⋅x6_0
19: −1390 + 4⋅x6_0
20: −1388 + 4⋅x6_0
2_var_snapshot: 0
2*: 2
19_var_snapshot: −1391 + 4⋅x6_0
19*: −1389 + 4⋅x6_0

13.3.3 Transition Removal

We remove transitions 59, 85, 87, 24, 25, 27 using the following ranking functions, which are bounded by −5.

0: −5
2: −1
18: −4
19: −2
20: 0
2_var_snapshot: 0
2*: 0
19_var_snapshot: −3
19*: −1

13.3.4 Splitting Cut-Point Transitions

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

13.3.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 56.

13.3.4.1.1 Splitting Cut-Point Transitions

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

13.3.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 84.

13.3.4.2.1 Splitting Cut-Point Transitions

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

13.4 SCC Subproblem 4/4

Here we consider the SCC { 3, 4, 4_var_snapshot, 4* }.

13.4.1 Transition Removal

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

3: −1 + 4⋅x4_0
4: 1 + 4⋅x6_0
4_var_snapshot: 4⋅x6_0
4*: 2 + 4⋅x6_0

13.4.2 Transition Removal

We remove transitions 64, 66, 31 using the following ranking functions, which are bounded by −3.

3: −3
4: −1
4_var_snapshot: −2
4*: 0

13.4.3 Splitting Cut-Point Transitions

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

13.4.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 63.

13.4.3.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert