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 ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0
4 63 4: x7_post + x7_post ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0
12 70 12: x7_post + x7_post ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0
17 77 17: x7_post + x7_post ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0
19 84 19: x7_post + x7_post ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_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 ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_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 ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_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 ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_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 ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_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 ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_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 ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_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 ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_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 ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_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 ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_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 ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_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