LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
1 37 1: − 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 ∧ − 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
3 44 3: − 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 ∧ − 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 51 4: − 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 ∧ − 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 17, 19, 21, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36 using the following ranking functions, which are bounded by −21.

12: 0
11: 0
10: 0
0: 0
1: 0
2: 0
3: 0
4: 0
5: 0
8: 0
9: 0
6: 0
7: 0
12: −7
11: −8
10: −9
0: −10
1: −10
2: −10
3: −10
4: −10
5: −10
8: −10
9: −10
1_var_snapshot: −10
1*: −10
3_var_snapshot: −10
3*: −10
4_var_snapshot: −10
4*: −10
6: −13
7: −14

3 Location Addition

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

1* 40 1: − 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 ∧ − 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.

1 38 1_var_snapshot: − 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 ∧ − 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.

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

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

4* 54 4: − 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 ∧ − 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.

4 52 4_var_snapshot: − 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 ∧ − 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 SCC Decomposition

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

9.1 SCC Subproblem 1/1

Here we consider the SCC { 0, 1, 2, 3, 4, 5, 8, 9, 1_var_snapshot, 1*, 3_var_snapshot, 3*, 4_var_snapshot, 4* }.

9.1.1 Transition Removal

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

0: 5 + 10⋅x0_0 − 10⋅x2_0
1: 5 + 10⋅x0_0 − 10⋅x2_0
2: 4 + 10⋅x0_0 − 10⋅x2_0
3: −1 + 10⋅x0_0 − 10⋅x2_0
4: 2 + 10⋅x0_0 − 10⋅x2_0
5: 5 + 10⋅x0_0 − 10⋅x2_0
8: 6 + 10⋅x0_0 − 10⋅x2_0
9: 7 + 10⋅x0_0 − 10⋅x2_0
1_var_snapshot: 5 + 10⋅x0_0 − 10⋅x2_0
1*: 5 + 10⋅x0_0 − 10⋅x2_0
3_var_snapshot: −2 + 10⋅x0_0 − 10⋅x2_0
3*: 10⋅x0_0 − 10⋅x2_0
4_var_snapshot: 1 + 10⋅x0_0 − 10⋅x2_0
4*: 3 + 10⋅x0_0 − 10⋅x2_0

9.1.2 Transition Removal

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

0: 6 − 15⋅x6_0
1: 5 − 15⋅x5_0
2: 4 − 15⋅x5_0
3: −1 − 15⋅x5_0
4: 2 − 15⋅x5_0
5: 5 − 15⋅x5_0
8: 6
9: −3 − 15⋅oldX5_post
1_var_snapshot: 5 − 15⋅x5_0
1*: 5 − 15⋅x5_0
3_var_snapshot: −2 − 15⋅x5_0
3*: −15⋅x5_0
4_var_snapshot: 1 − 15⋅x5_0
4*: 3 − 15⋅x5_0

9.1.3 Transition Removal

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

0: 0
1: 0
2: 0
3: −1
4: 0
5: 0
8: 0
9: −1
1_var_snapshot: 0
1*: 0
3_var_snapshot: −1
3*: −1
4_var_snapshot: −1
4*: 0

9.1.4 Transition Removal

We remove transitions 54, 3, 10, 23 using the following ranking functions, which are bounded by −3.

0: 0
1: 0
2: 0
3: −3
4: −2
5: 0
8: 0
9: −3
1_var_snapshot: 0
1*: 0
3_var_snapshot: −3
3*: −3
4_var_snapshot: −2
4*: −1

9.1.5 Transition Removal

We remove transitions 45, 47, 22 using the following ranking functions, which are bounded by −2.

0: x1_0 − x6_0
1: x1_0 − x5_0
2: −1 + x1_0 − x5_0
3: 0
4: 1
5: x1_0 − x5_0
8: 0
9: −2
1_var_snapshot: x1_0 − x5_0
1*: x1_0 − x5_0
3_var_snapshot: −1
3*: 1
4_var_snapshot: 0
4*: 0

9.1.6 Transition Removal

We remove transitions 5, 13, 14, 15 using the following ranking functions, which are bounded by −1.

0: 0
1: 0
2: −1
3: 0
4: 0
5: 0
8: 0
9: 0
1_var_snapshot: 0
1*: 0
3_var_snapshot: 0
3*: 0
4_var_snapshot: 0
4*: 0

9.1.7 Transition Removal

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

0: 0
1: 0
2: 0
3: 0
4: 0
5: 0
8: 0
9: 0
1_var_snapshot: 0
1*: 0
3_var_snapshot: 0
3*: 0
4_var_snapshot: 0
4*: 0

9.1.8 Transition Removal

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

0: 0
1: 0
2: 0
3: 0
4: 0
5: 0
8: 0
9: 0
1_var_snapshot: 0
1*: 0
3_var_snapshot: 0
3*: 0
4_var_snapshot: 0
4*: 0

9.1.9 Splitting Cut-Point Transitions

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

9.1.9.1 Cut-Point Subproblem 1/3

Here we consider cut-point transition 37.

9.1.9.1.1 Fresh Variable Addition

The new variable __snapshot_1_x6_post is introduced. The transition formulas are extended as follows:

38: __snapshot_1_x6_post ≤ x6_post ∧ x6_post ≤ __snapshot_1_x6_post
40: __snapshot_1_x6_post ≤ __snapshot_1_x6_post ∧ __snapshot_1_x6_post ≤ __snapshot_1_x6_post
45: __snapshot_1_x6_post ≤ __snapshot_1_x6_post ∧ __snapshot_1_x6_post ≤ __snapshot_1_x6_post
52: __snapshot_1_x6_post ≤ __snapshot_1_x6_post ∧ __snapshot_1_x6_post ≤ __snapshot_1_x6_post
0: __snapshot_1_x6_post ≤ __snapshot_1_x6_post ∧ __snapshot_1_x6_post ≤ __snapshot_1_x6_post
4: __snapshot_1_x6_post ≤ __snapshot_1_x6_post ∧ __snapshot_1_x6_post ≤ __snapshot_1_x6_post
7: __snapshot_1_x6_post ≤ __snapshot_1_x6_post ∧ __snapshot_1_x6_post ≤ __snapshot_1_x6_post
12: __snapshot_1_x6_post ≤ __snapshot_1_x6_post ∧ __snapshot_1_x6_post ≤ __snapshot_1_x6_post
16: __snapshot_1_x6_post ≤ __snapshot_1_x6_post ∧ __snapshot_1_x6_post ≤ __snapshot_1_x6_post

9.1.9.1.2 Fresh Variable Addition

The new variable __snapshot_1_x6_0 is introduced. The transition formulas are extended as follows:

38: __snapshot_1_x6_0 ≤ x6_0 ∧ x6_0 ≤ __snapshot_1_x6_0
40: __snapshot_1_x6_0 ≤ __snapshot_1_x6_0 ∧ __snapshot_1_x6_0 ≤ __snapshot_1_x6_0
45: __snapshot_1_x6_0 ≤ __snapshot_1_x6_0 ∧ __snapshot_1_x6_0 ≤ __snapshot_1_x6_0
52: __snapshot_1_x6_0 ≤ __snapshot_1_x6_0 ∧ __snapshot_1_x6_0 ≤ __snapshot_1_x6_0
0: __snapshot_1_x6_0 ≤ __snapshot_1_x6_0 ∧ __snapshot_1_x6_0 ≤ __snapshot_1_x6_0
4: __snapshot_1_x6_0 ≤ __snapshot_1_x6_0 ∧ __snapshot_1_x6_0 ≤ __snapshot_1_x6_0
7: __snapshot_1_x6_0 ≤ __snapshot_1_x6_0 ∧ __snapshot_1_x6_0 ≤ __snapshot_1_x6_0
12: __snapshot_1_x6_0 ≤ __snapshot_1_x6_0 ∧ __snapshot_1_x6_0 ≤ __snapshot_1_x6_0
16: __snapshot_1_x6_0 ≤ __snapshot_1_x6_0 ∧ __snapshot_1_x6_0 ≤ __snapshot_1_x6_0

9.1.9.1.3 Fresh Variable Addition

The new variable __snapshot_1_x5_post is introduced. The transition formulas are extended as follows:

38: __snapshot_1_x5_post ≤ x5_post ∧ x5_post ≤ __snapshot_1_x5_post
40: __snapshot_1_x5_post ≤ __snapshot_1_x5_post ∧ __snapshot_1_x5_post ≤ __snapshot_1_x5_post
45: __snapshot_1_x5_post ≤ __snapshot_1_x5_post ∧ __snapshot_1_x5_post ≤ __snapshot_1_x5_post
52: __snapshot_1_x5_post ≤ __snapshot_1_x5_post ∧ __snapshot_1_x5_post ≤ __snapshot_1_x5_post
0: __snapshot_1_x5_post ≤ __snapshot_1_x5_post ∧ __snapshot_1_x5_post ≤ __snapshot_1_x5_post
4: __snapshot_1_x5_post ≤ __snapshot_1_x5_post ∧ __snapshot_1_x5_post ≤ __snapshot_1_x5_post
7: __snapshot_1_x5_post ≤ __snapshot_1_x5_post ∧ __snapshot_1_x5_post ≤ __snapshot_1_x5_post
12: __snapshot_1_x5_post ≤ __snapshot_1_x5_post ∧ __snapshot_1_x5_post ≤ __snapshot_1_x5_post
16: __snapshot_1_x5_post ≤ __snapshot_1_x5_post ∧ __snapshot_1_x5_post ≤ __snapshot_1_x5_post

9.1.9.1.4 Fresh Variable Addition

The new variable __snapshot_1_x5_0 is introduced. The transition formulas are extended as follows:

38: __snapshot_1_x5_0 ≤ x5_0 ∧ x5_0 ≤ __snapshot_1_x5_0
40: __snapshot_1_x5_0 ≤ __snapshot_1_x5_0 ∧ __snapshot_1_x5_0 ≤ __snapshot_1_x5_0
45: __snapshot_1_x5_0 ≤ __snapshot_1_x5_0 ∧ __snapshot_1_x5_0 ≤ __snapshot_1_x5_0
52: __snapshot_1_x5_0 ≤ __snapshot_1_x5_0 ∧ __snapshot_1_x5_0 ≤ __snapshot_1_x5_0
0: __snapshot_1_x5_0 ≤ __snapshot_1_x5_0 ∧ __snapshot_1_x5_0 ≤ __snapshot_1_x5_0
4: __snapshot_1_x5_0 ≤ __snapshot_1_x5_0 ∧ __snapshot_1_x5_0 ≤ __snapshot_1_x5_0
7: __snapshot_1_x5_0 ≤ __snapshot_1_x5_0 ∧ __snapshot_1_x5_0 ≤ __snapshot_1_x5_0
12: __snapshot_1_x5_0 ≤ __snapshot_1_x5_0 ∧ __snapshot_1_x5_0 ≤ __snapshot_1_x5_0
16: __snapshot_1_x5_0 ≤ __snapshot_1_x5_0 ∧ __snapshot_1_x5_0 ≤ __snapshot_1_x5_0

9.1.9.1.5 Fresh Variable Addition

The new variable __snapshot_1_x4_post is introduced. The transition formulas are extended as follows:

38: __snapshot_1_x4_post ≤ x4_post ∧ x4_post ≤ __snapshot_1_x4_post
40: __snapshot_1_x4_post ≤ __snapshot_1_x4_post ∧ __snapshot_1_x4_post ≤ __snapshot_1_x4_post
45: __snapshot_1_x4_post ≤ __snapshot_1_x4_post ∧ __snapshot_1_x4_post ≤ __snapshot_1_x4_post
52: __snapshot_1_x4_post ≤ __snapshot_1_x4_post ∧ __snapshot_1_x4_post ≤ __snapshot_1_x4_post
0: __snapshot_1_x4_post ≤ __snapshot_1_x4_post ∧ __snapshot_1_x4_post ≤ __snapshot_1_x4_post
4: __snapshot_1_x4_post ≤ __snapshot_1_x4_post ∧ __snapshot_1_x4_post ≤ __snapshot_1_x4_post
7: __snapshot_1_x4_post ≤ __snapshot_1_x4_post ∧ __snapshot_1_x4_post ≤ __snapshot_1_x4_post
12: __snapshot_1_x4_post ≤ __snapshot_1_x4_post ∧ __snapshot_1_x4_post ≤ __snapshot_1_x4_post
16: __snapshot_1_x4_post ≤ __snapshot_1_x4_post ∧ __snapshot_1_x4_post ≤ __snapshot_1_x4_post

9.1.9.1.6 Fresh Variable Addition

The new variable __snapshot_1_x4_0 is introduced. The transition formulas are extended as follows:

38: __snapshot_1_x4_0 ≤ x4_0 ∧ x4_0 ≤ __snapshot_1_x4_0
40: __snapshot_1_x4_0 ≤ __snapshot_1_x4_0 ∧ __snapshot_1_x4_0 ≤ __snapshot_1_x4_0
45: __snapshot_1_x4_0 ≤ __snapshot_1_x4_0 ∧ __snapshot_1_x4_0 ≤ __snapshot_1_x4_0
52: __snapshot_1_x4_0 ≤ __snapshot_1_x4_0 ∧ __snapshot_1_x4_0 ≤ __snapshot_1_x4_0
0: __snapshot_1_x4_0 ≤ __snapshot_1_x4_0 ∧ __snapshot_1_x4_0 ≤ __snapshot_1_x4_0
4: __snapshot_1_x4_0 ≤ __snapshot_1_x4_0 ∧ __snapshot_1_x4_0 ≤ __snapshot_1_x4_0
7: __snapshot_1_x4_0 ≤ __snapshot_1_x4_0 ∧ __snapshot_1_x4_0 ≤ __snapshot_1_x4_0
12: __snapshot_1_x4_0 ≤ __snapshot_1_x4_0 ∧ __snapshot_1_x4_0 ≤ __snapshot_1_x4_0
16: __snapshot_1_x4_0 ≤ __snapshot_1_x4_0 ∧ __snapshot_1_x4_0 ≤ __snapshot_1_x4_0

9.1.9.1.7 Fresh Variable Addition

The new variable __snapshot_1_x3_post is introduced. The transition formulas are extended as follows:

38: __snapshot_1_x3_post ≤ x3_post ∧ x3_post ≤ __snapshot_1_x3_post
40: __snapshot_1_x3_post ≤ __snapshot_1_x3_post ∧ __snapshot_1_x3_post ≤ __snapshot_1_x3_post
45: __snapshot_1_x3_post ≤ __snapshot_1_x3_post ∧ __snapshot_1_x3_post ≤ __snapshot_1_x3_post
52: __snapshot_1_x3_post ≤ __snapshot_1_x3_post ∧ __snapshot_1_x3_post ≤ __snapshot_1_x3_post
0: __snapshot_1_x3_post ≤ __snapshot_1_x3_post ∧ __snapshot_1_x3_post ≤ __snapshot_1_x3_post
4: __snapshot_1_x3_post ≤ __snapshot_1_x3_post ∧ __snapshot_1_x3_post ≤ __snapshot_1_x3_post
7: __snapshot_1_x3_post ≤ __snapshot_1_x3_post ∧ __snapshot_1_x3_post ≤ __snapshot_1_x3_post
12: __snapshot_1_x3_post ≤ __snapshot_1_x3_post ∧ __snapshot_1_x3_post ≤ __snapshot_1_x3_post
16: __snapshot_1_x3_post ≤ __snapshot_1_x3_post ∧ __snapshot_1_x3_post ≤ __snapshot_1_x3_post

9.1.9.1.8 Fresh Variable Addition

The new variable __snapshot_1_x3_0 is introduced. The transition formulas are extended as follows:

38: __snapshot_1_x3_0 ≤ x3_0 ∧ x3_0 ≤ __snapshot_1_x3_0
40: __snapshot_1_x3_0 ≤ __snapshot_1_x3_0 ∧ __snapshot_1_x3_0 ≤ __snapshot_1_x3_0
45: __snapshot_1_x3_0 ≤ __snapshot_1_x3_0 ∧ __snapshot_1_x3_0 ≤ __snapshot_1_x3_0
52: __snapshot_1_x3_0 ≤ __snapshot_1_x3_0 ∧ __snapshot_1_x3_0 ≤ __snapshot_1_x3_0
0: __snapshot_1_x3_0 ≤ __snapshot_1_x3_0 ∧ __snapshot_1_x3_0 ≤ __snapshot_1_x3_0
4: __snapshot_1_x3_0 ≤ __snapshot_1_x3_0 ∧ __snapshot_1_x3_0 ≤ __snapshot_1_x3_0
7: __snapshot_1_x3_0 ≤ __snapshot_1_x3_0 ∧ __snapshot_1_x3_0 ≤ __snapshot_1_x3_0
12: __snapshot_1_x3_0 ≤ __snapshot_1_x3_0 ∧ __snapshot_1_x3_0 ≤ __snapshot_1_x3_0
16: __snapshot_1_x3_0 ≤ __snapshot_1_x3_0 ∧ __snapshot_1_x3_0 ≤ __snapshot_1_x3_0

9.1.9.1.9 Fresh Variable Addition

The new variable __snapshot_1_x2_post is introduced. The transition formulas are extended as follows:

38: __snapshot_1_x2_post ≤ x2_post ∧ x2_post ≤ __snapshot_1_x2_post
40: __snapshot_1_x2_post ≤ __snapshot_1_x2_post ∧ __snapshot_1_x2_post ≤ __snapshot_1_x2_post
45: __snapshot_1_x2_post ≤ __snapshot_1_x2_post ∧ __snapshot_1_x2_post ≤ __snapshot_1_x2_post
52: __snapshot_1_x2_post ≤ __snapshot_1_x2_post ∧ __snapshot_1_x2_post ≤ __snapshot_1_x2_post
0: __snapshot_1_x2_post ≤ __snapshot_1_x2_post ∧ __snapshot_1_x2_post ≤ __snapshot_1_x2_post
4: __snapshot_1_x2_post ≤ __snapshot_1_x2_post ∧ __snapshot_1_x2_post ≤ __snapshot_1_x2_post
7: __snapshot_1_x2_post ≤ __snapshot_1_x2_post ∧ __snapshot_1_x2_post ≤ __snapshot_1_x2_post
12: __snapshot_1_x2_post ≤ __snapshot_1_x2_post ∧ __snapshot_1_x2_post ≤ __snapshot_1_x2_post
16: __snapshot_1_x2_post ≤ __snapshot_1_x2_post ∧ __snapshot_1_x2_post ≤ __snapshot_1_x2_post

9.1.9.1.10 Fresh Variable Addition

The new variable __snapshot_1_x2_0 is introduced. The transition formulas are extended as follows:

38: __snapshot_1_x2_0 ≤ x2_0 ∧ x2_0 ≤ __snapshot_1_x2_0
40: __snapshot_1_x2_0 ≤ __snapshot_1_x2_0 ∧ __snapshot_1_x2_0 ≤ __snapshot_1_x2_0
45: __snapshot_1_x2_0 ≤ __snapshot_1_x2_0 ∧ __snapshot_1_x2_0 ≤ __snapshot_1_x2_0
52: __snapshot_1_x2_0 ≤ __snapshot_1_x2_0 ∧ __snapshot_1_x2_0 ≤ __snapshot_1_x2_0
0: __snapshot_1_x2_0 ≤ __snapshot_1_x2_0 ∧ __snapshot_1_x2_0 ≤ __snapshot_1_x2_0
4: __snapshot_1_x2_0 ≤ __snapshot_1_x2_0 ∧ __snapshot_1_x2_0 ≤ __snapshot_1_x2_0
7: __snapshot_1_x2_0 ≤ __snapshot_1_x2_0 ∧ __snapshot_1_x2_0 ≤ __snapshot_1_x2_0
12: __snapshot_1_x2_0 ≤ __snapshot_1_x2_0 ∧ __snapshot_1_x2_0 ≤ __snapshot_1_x2_0
16: __snapshot_1_x2_0 ≤ __snapshot_1_x2_0 ∧ __snapshot_1_x2_0 ≤ __snapshot_1_x2_0

9.1.9.1.11 Fresh Variable Addition

The new variable __snapshot_1_x1_post is introduced. The transition formulas are extended as follows:

38: __snapshot_1_x1_post ≤ x1_post ∧ x1_post ≤ __snapshot_1_x1_post
40: __snapshot_1_x1_post ≤ __snapshot_1_x1_post ∧ __snapshot_1_x1_post ≤ __snapshot_1_x1_post
45: __snapshot_1_x1_post ≤ __snapshot_1_x1_post ∧ __snapshot_1_x1_post ≤ __snapshot_1_x1_post
52: __snapshot_1_x1_post ≤ __snapshot_1_x1_post ∧ __snapshot_1_x1_post ≤ __snapshot_1_x1_post
0: __snapshot_1_x1_post ≤ __snapshot_1_x1_post ∧ __snapshot_1_x1_post ≤ __snapshot_1_x1_post
4: __snapshot_1_x1_post ≤ __snapshot_1_x1_post ∧ __snapshot_1_x1_post ≤ __snapshot_1_x1_post
7: __snapshot_1_x1_post ≤ __snapshot_1_x1_post ∧ __snapshot_1_x1_post ≤ __snapshot_1_x1_post
12: __snapshot_1_x1_post ≤ __snapshot_1_x1_post ∧ __snapshot_1_x1_post ≤ __snapshot_1_x1_post
16: __snapshot_1_x1_post ≤ __snapshot_1_x1_post ∧ __snapshot_1_x1_post ≤ __snapshot_1_x1_post

9.1.9.1.12 Fresh Variable Addition

The new variable __snapshot_1_x1_0 is introduced. The transition formulas are extended as follows:

38: __snapshot_1_x1_0 ≤ x1_0 ∧ x1_0 ≤ __snapshot_1_x1_0
40: __snapshot_1_x1_0 ≤ __snapshot_1_x1_0 ∧ __snapshot_1_x1_0 ≤ __snapshot_1_x1_0
45: __snapshot_1_x1_0 ≤ __snapshot_1_x1_0 ∧ __snapshot_1_x1_0 ≤ __snapshot_1_x1_0
52: __snapshot_1_x1_0 ≤ __snapshot_1_x1_0 ∧ __snapshot_1_x1_0 ≤ __snapshot_1_x1_0
0: __snapshot_1_x1_0 ≤ __snapshot_1_x1_0 ∧ __snapshot_1_x1_0 ≤ __snapshot_1_x1_0
4: __snapshot_1_x1_0 ≤ __snapshot_1_x1_0 ∧ __snapshot_1_x1_0 ≤ __snapshot_1_x1_0
7: __snapshot_1_x1_0 ≤ __snapshot_1_x1_0 ∧ __snapshot_1_x1_0 ≤ __snapshot_1_x1_0
12: __snapshot_1_x1_0 ≤ __snapshot_1_x1_0 ∧ __snapshot_1_x1_0 ≤ __snapshot_1_x1_0
16: __snapshot_1_x1_0 ≤ __snapshot_1_x1_0 ∧ __snapshot_1_x1_0 ≤ __snapshot_1_x1_0

9.1.9.1.13 Fresh Variable Addition

The new variable __snapshot_1_x0_post is introduced. The transition formulas are extended as follows:

38: __snapshot_1_x0_post ≤ x0_post ∧ x0_post ≤ __snapshot_1_x0_post
40: __snapshot_1_x0_post ≤ __snapshot_1_x0_post ∧ __snapshot_1_x0_post ≤ __snapshot_1_x0_post
45: __snapshot_1_x0_post ≤ __snapshot_1_x0_post ∧ __snapshot_1_x0_post ≤ __snapshot_1_x0_post
52: __snapshot_1_x0_post ≤ __snapshot_1_x0_post ∧ __snapshot_1_x0_post ≤ __snapshot_1_x0_post
0: __snapshot_1_x0_post ≤ __snapshot_1_x0_post ∧ __snapshot_1_x0_post ≤ __snapshot_1_x0_post
4: __snapshot_1_x0_post ≤ __snapshot_1_x0_post ∧ __snapshot_1_x0_post ≤ __snapshot_1_x0_post
7: __snapshot_1_x0_post ≤ __snapshot_1_x0_post ∧ __snapshot_1_x0_post ≤ __snapshot_1_x0_post
12: __snapshot_1_x0_post ≤ __snapshot_1_x0_post ∧ __snapshot_1_x0_post ≤ __snapshot_1_x0_post
16: __snapshot_1_x0_post ≤ __snapshot_1_x0_post ∧ __snapshot_1_x0_post ≤ __snapshot_1_x0_post

9.1.9.1.14 Fresh Variable Addition

The new variable __snapshot_1_x0_0 is introduced. The transition formulas are extended as follows:

38: __snapshot_1_x0_0 ≤ x0_0 ∧ x0_0 ≤ __snapshot_1_x0_0
40: __snapshot_1_x0_0 ≤ __snapshot_1_x0_0 ∧ __snapshot_1_x0_0 ≤ __snapshot_1_x0_0
45: __snapshot_1_x0_0 ≤ __snapshot_1_x0_0 ∧ __snapshot_1_x0_0 ≤ __snapshot_1_x0_0
52: __snapshot_1_x0_0 ≤ __snapshot_1_x0_0 ∧ __snapshot_1_x0_0 ≤ __snapshot_1_x0_0
0: __snapshot_1_x0_0 ≤ __snapshot_1_x0_0 ∧ __snapshot_1_x0_0 ≤ __snapshot_1_x0_0
4: __snapshot_1_x0_0 ≤ __snapshot_1_x0_0 ∧ __snapshot_1_x0_0 ≤ __snapshot_1_x0_0
7: __snapshot_1_x0_0 ≤ __snapshot_1_x0_0 ∧ __snapshot_1_x0_0 ≤ __snapshot_1_x0_0
12: __snapshot_1_x0_0 ≤ __snapshot_1_x0_0 ∧ __snapshot_1_x0_0 ≤ __snapshot_1_x0_0
16: __snapshot_1_x0_0 ≤ __snapshot_1_x0_0 ∧ __snapshot_1_x0_0 ≤ __snapshot_1_x0_0

9.1.9.1.15 Fresh Variable Addition

The new variable __snapshot_1_oldX9_post is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX9_post ≤ oldX9_post ∧ oldX9_post ≤ __snapshot_1_oldX9_post
40: __snapshot_1_oldX9_post ≤ __snapshot_1_oldX9_post ∧ __snapshot_1_oldX9_post ≤ __snapshot_1_oldX9_post
45: __snapshot_1_oldX9_post ≤ __snapshot_1_oldX9_post ∧ __snapshot_1_oldX9_post ≤ __snapshot_1_oldX9_post
52: __snapshot_1_oldX9_post ≤ __snapshot_1_oldX9_post ∧ __snapshot_1_oldX9_post ≤ __snapshot_1_oldX9_post
0: __snapshot_1_oldX9_post ≤ __snapshot_1_oldX9_post ∧ __snapshot_1_oldX9_post ≤ __snapshot_1_oldX9_post
4: __snapshot_1_oldX9_post ≤ __snapshot_1_oldX9_post ∧ __snapshot_1_oldX9_post ≤ __snapshot_1_oldX9_post
7: __snapshot_1_oldX9_post ≤ __snapshot_1_oldX9_post ∧ __snapshot_1_oldX9_post ≤ __snapshot_1_oldX9_post
12: __snapshot_1_oldX9_post ≤ __snapshot_1_oldX9_post ∧ __snapshot_1_oldX9_post ≤ __snapshot_1_oldX9_post
16: __snapshot_1_oldX9_post ≤ __snapshot_1_oldX9_post ∧ __snapshot_1_oldX9_post ≤ __snapshot_1_oldX9_post

9.1.9.1.16 Fresh Variable Addition

The new variable __snapshot_1_oldX9_0 is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX9_0 ≤ oldX9_0 ∧ oldX9_0 ≤ __snapshot_1_oldX9_0
40: __snapshot_1_oldX9_0 ≤ __snapshot_1_oldX9_0 ∧ __snapshot_1_oldX9_0 ≤ __snapshot_1_oldX9_0
45: __snapshot_1_oldX9_0 ≤ __snapshot_1_oldX9_0 ∧ __snapshot_1_oldX9_0 ≤ __snapshot_1_oldX9_0
52: __snapshot_1_oldX9_0 ≤ __snapshot_1_oldX9_0 ∧ __snapshot_1_oldX9_0 ≤ __snapshot_1_oldX9_0
0: __snapshot_1_oldX9_0 ≤ __snapshot_1_oldX9_0 ∧ __snapshot_1_oldX9_0 ≤ __snapshot_1_oldX9_0
4: __snapshot_1_oldX9_0 ≤ __snapshot_1_oldX9_0 ∧ __snapshot_1_oldX9_0 ≤ __snapshot_1_oldX9_0
7: __snapshot_1_oldX9_0 ≤ __snapshot_1_oldX9_0 ∧ __snapshot_1_oldX9_0 ≤ __snapshot_1_oldX9_0
12: __snapshot_1_oldX9_0 ≤ __snapshot_1_oldX9_0 ∧ __snapshot_1_oldX9_0 ≤ __snapshot_1_oldX9_0
16: __snapshot_1_oldX9_0 ≤ __snapshot_1_oldX9_0 ∧ __snapshot_1_oldX9_0 ≤ __snapshot_1_oldX9_0

9.1.9.1.17 Fresh Variable Addition

The new variable __snapshot_1_oldX8_post is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX8_post ≤ oldX8_post ∧ oldX8_post ≤ __snapshot_1_oldX8_post
40: __snapshot_1_oldX8_post ≤ __snapshot_1_oldX8_post ∧ __snapshot_1_oldX8_post ≤ __snapshot_1_oldX8_post
45: __snapshot_1_oldX8_post ≤ __snapshot_1_oldX8_post ∧ __snapshot_1_oldX8_post ≤ __snapshot_1_oldX8_post
52: __snapshot_1_oldX8_post ≤ __snapshot_1_oldX8_post ∧ __snapshot_1_oldX8_post ≤ __snapshot_1_oldX8_post
0: __snapshot_1_oldX8_post ≤ __snapshot_1_oldX8_post ∧ __snapshot_1_oldX8_post ≤ __snapshot_1_oldX8_post
4: __snapshot_1_oldX8_post ≤ __snapshot_1_oldX8_post ∧ __snapshot_1_oldX8_post ≤ __snapshot_1_oldX8_post
7: __snapshot_1_oldX8_post ≤ __snapshot_1_oldX8_post ∧ __snapshot_1_oldX8_post ≤ __snapshot_1_oldX8_post
12: __snapshot_1_oldX8_post ≤ __snapshot_1_oldX8_post ∧ __snapshot_1_oldX8_post ≤ __snapshot_1_oldX8_post
16: __snapshot_1_oldX8_post ≤ __snapshot_1_oldX8_post ∧ __snapshot_1_oldX8_post ≤ __snapshot_1_oldX8_post

9.1.9.1.18 Fresh Variable Addition

The new variable __snapshot_1_oldX8_0 is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX8_0 ≤ oldX8_0 ∧ oldX8_0 ≤ __snapshot_1_oldX8_0
40: __snapshot_1_oldX8_0 ≤ __snapshot_1_oldX8_0 ∧ __snapshot_1_oldX8_0 ≤ __snapshot_1_oldX8_0
45: __snapshot_1_oldX8_0 ≤ __snapshot_1_oldX8_0 ∧ __snapshot_1_oldX8_0 ≤ __snapshot_1_oldX8_0
52: __snapshot_1_oldX8_0 ≤ __snapshot_1_oldX8_0 ∧ __snapshot_1_oldX8_0 ≤ __snapshot_1_oldX8_0
0: __snapshot_1_oldX8_0 ≤ __snapshot_1_oldX8_0 ∧ __snapshot_1_oldX8_0 ≤ __snapshot_1_oldX8_0
4: __snapshot_1_oldX8_0 ≤ __snapshot_1_oldX8_0 ∧ __snapshot_1_oldX8_0 ≤ __snapshot_1_oldX8_0
7: __snapshot_1_oldX8_0 ≤ __snapshot_1_oldX8_0 ∧ __snapshot_1_oldX8_0 ≤ __snapshot_1_oldX8_0
12: __snapshot_1_oldX8_0 ≤ __snapshot_1_oldX8_0 ∧ __snapshot_1_oldX8_0 ≤ __snapshot_1_oldX8_0
16: __snapshot_1_oldX8_0 ≤ __snapshot_1_oldX8_0 ∧ __snapshot_1_oldX8_0 ≤ __snapshot_1_oldX8_0

9.1.9.1.19 Fresh Variable Addition

The new variable __snapshot_1_oldX7_post is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX7_post ≤ oldX7_post ∧ oldX7_post ≤ __snapshot_1_oldX7_post
40: __snapshot_1_oldX7_post ≤ __snapshot_1_oldX7_post ∧ __snapshot_1_oldX7_post ≤ __snapshot_1_oldX7_post
45: __snapshot_1_oldX7_post ≤ __snapshot_1_oldX7_post ∧ __snapshot_1_oldX7_post ≤ __snapshot_1_oldX7_post
52: __snapshot_1_oldX7_post ≤ __snapshot_1_oldX7_post ∧ __snapshot_1_oldX7_post ≤ __snapshot_1_oldX7_post
0: __snapshot_1_oldX7_post ≤ __snapshot_1_oldX7_post ∧ __snapshot_1_oldX7_post ≤ __snapshot_1_oldX7_post
4: __snapshot_1_oldX7_post ≤ __snapshot_1_oldX7_post ∧ __snapshot_1_oldX7_post ≤ __snapshot_1_oldX7_post
7: __snapshot_1_oldX7_post ≤ __snapshot_1_oldX7_post ∧ __snapshot_1_oldX7_post ≤ __snapshot_1_oldX7_post
12: __snapshot_1_oldX7_post ≤ __snapshot_1_oldX7_post ∧ __snapshot_1_oldX7_post ≤ __snapshot_1_oldX7_post
16: __snapshot_1_oldX7_post ≤ __snapshot_1_oldX7_post ∧ __snapshot_1_oldX7_post ≤ __snapshot_1_oldX7_post

9.1.9.1.20 Fresh Variable Addition

The new variable __snapshot_1_oldX7_0 is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX7_0 ≤ oldX7_0 ∧ oldX7_0 ≤ __snapshot_1_oldX7_0
40: __snapshot_1_oldX7_0 ≤ __snapshot_1_oldX7_0 ∧ __snapshot_1_oldX7_0 ≤ __snapshot_1_oldX7_0
45: __snapshot_1_oldX7_0 ≤ __snapshot_1_oldX7_0 ∧ __snapshot_1_oldX7_0 ≤ __snapshot_1_oldX7_0
52: __snapshot_1_oldX7_0 ≤ __snapshot_1_oldX7_0 ∧ __snapshot_1_oldX7_0 ≤ __snapshot_1_oldX7_0
0: __snapshot_1_oldX7_0 ≤ __snapshot_1_oldX7_0 ∧ __snapshot_1_oldX7_0 ≤ __snapshot_1_oldX7_0
4: __snapshot_1_oldX7_0 ≤ __snapshot_1_oldX7_0 ∧ __snapshot_1_oldX7_0 ≤ __snapshot_1_oldX7_0
7: __snapshot_1_oldX7_0 ≤ __snapshot_1_oldX7_0 ∧ __snapshot_1_oldX7_0 ≤ __snapshot_1_oldX7_0
12: __snapshot_1_oldX7_0 ≤ __snapshot_1_oldX7_0 ∧ __snapshot_1_oldX7_0 ≤ __snapshot_1_oldX7_0
16: __snapshot_1_oldX7_0 ≤ __snapshot_1_oldX7_0 ∧ __snapshot_1_oldX7_0 ≤ __snapshot_1_oldX7_0

9.1.9.1.21 Fresh Variable Addition

The new variable __snapshot_1_oldX6_post is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX6_post ≤ oldX6_post ∧ oldX6_post ≤ __snapshot_1_oldX6_post
40: __snapshot_1_oldX6_post ≤ __snapshot_1_oldX6_post ∧ __snapshot_1_oldX6_post ≤ __snapshot_1_oldX6_post
45: __snapshot_1_oldX6_post ≤ __snapshot_1_oldX6_post ∧ __snapshot_1_oldX6_post ≤ __snapshot_1_oldX6_post
52: __snapshot_1_oldX6_post ≤ __snapshot_1_oldX6_post ∧ __snapshot_1_oldX6_post ≤ __snapshot_1_oldX6_post
0: __snapshot_1_oldX6_post ≤ __snapshot_1_oldX6_post ∧ __snapshot_1_oldX6_post ≤ __snapshot_1_oldX6_post
4: __snapshot_1_oldX6_post ≤ __snapshot_1_oldX6_post ∧ __snapshot_1_oldX6_post ≤ __snapshot_1_oldX6_post
7: __snapshot_1_oldX6_post ≤ __snapshot_1_oldX6_post ∧ __snapshot_1_oldX6_post ≤ __snapshot_1_oldX6_post
12: __snapshot_1_oldX6_post ≤ __snapshot_1_oldX6_post ∧ __snapshot_1_oldX6_post ≤ __snapshot_1_oldX6_post
16: __snapshot_1_oldX6_post ≤ __snapshot_1_oldX6_post ∧ __snapshot_1_oldX6_post ≤ __snapshot_1_oldX6_post

9.1.9.1.22 Fresh Variable Addition

The new variable __snapshot_1_oldX6_0 is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX6_0 ≤ oldX6_0 ∧ oldX6_0 ≤ __snapshot_1_oldX6_0
40: __snapshot_1_oldX6_0 ≤ __snapshot_1_oldX6_0 ∧ __snapshot_1_oldX6_0 ≤ __snapshot_1_oldX6_0
45: __snapshot_1_oldX6_0 ≤ __snapshot_1_oldX6_0 ∧ __snapshot_1_oldX6_0 ≤ __snapshot_1_oldX6_0
52: __snapshot_1_oldX6_0 ≤ __snapshot_1_oldX6_0 ∧ __snapshot_1_oldX6_0 ≤ __snapshot_1_oldX6_0
0: __snapshot_1_oldX6_0 ≤ __snapshot_1_oldX6_0 ∧ __snapshot_1_oldX6_0 ≤ __snapshot_1_oldX6_0
4: __snapshot_1_oldX6_0 ≤ __snapshot_1_oldX6_0 ∧ __snapshot_1_oldX6_0 ≤ __snapshot_1_oldX6_0
7: __snapshot_1_oldX6_0 ≤ __snapshot_1_oldX6_0 ∧ __snapshot_1_oldX6_0 ≤ __snapshot_1_oldX6_0
12: __snapshot_1_oldX6_0 ≤ __snapshot_1_oldX6_0 ∧ __snapshot_1_oldX6_0 ≤ __snapshot_1_oldX6_0
16: __snapshot_1_oldX6_0 ≤ __snapshot_1_oldX6_0 ∧ __snapshot_1_oldX6_0 ≤ __snapshot_1_oldX6_0

9.1.9.1.23 Fresh Variable Addition

The new variable __snapshot_1_oldX5_post is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX5_post ≤ oldX5_post ∧ oldX5_post ≤ __snapshot_1_oldX5_post
40: __snapshot_1_oldX5_post ≤ __snapshot_1_oldX5_post ∧ __snapshot_1_oldX5_post ≤ __snapshot_1_oldX5_post
45: __snapshot_1_oldX5_post ≤ __snapshot_1_oldX5_post ∧ __snapshot_1_oldX5_post ≤ __snapshot_1_oldX5_post
52: __snapshot_1_oldX5_post ≤ __snapshot_1_oldX5_post ∧ __snapshot_1_oldX5_post ≤ __snapshot_1_oldX5_post
0: __snapshot_1_oldX5_post ≤ __snapshot_1_oldX5_post ∧ __snapshot_1_oldX5_post ≤ __snapshot_1_oldX5_post
4: __snapshot_1_oldX5_post ≤ __snapshot_1_oldX5_post ∧ __snapshot_1_oldX5_post ≤ __snapshot_1_oldX5_post
7: __snapshot_1_oldX5_post ≤ __snapshot_1_oldX5_post ∧ __snapshot_1_oldX5_post ≤ __snapshot_1_oldX5_post
12: __snapshot_1_oldX5_post ≤ __snapshot_1_oldX5_post ∧ __snapshot_1_oldX5_post ≤ __snapshot_1_oldX5_post
16: __snapshot_1_oldX5_post ≤ __snapshot_1_oldX5_post ∧ __snapshot_1_oldX5_post ≤ __snapshot_1_oldX5_post

9.1.9.1.24 Fresh Variable Addition

The new variable __snapshot_1_oldX5_0 is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX5_0 ≤ oldX5_0 ∧ oldX5_0 ≤ __snapshot_1_oldX5_0
40: __snapshot_1_oldX5_0 ≤ __snapshot_1_oldX5_0 ∧ __snapshot_1_oldX5_0 ≤ __snapshot_1_oldX5_0
45: __snapshot_1_oldX5_0 ≤ __snapshot_1_oldX5_0 ∧ __snapshot_1_oldX5_0 ≤ __snapshot_1_oldX5_0
52: __snapshot_1_oldX5_0 ≤ __snapshot_1_oldX5_0 ∧ __snapshot_1_oldX5_0 ≤ __snapshot_1_oldX5_0
0: __snapshot_1_oldX5_0 ≤ __snapshot_1_oldX5_0 ∧ __snapshot_1_oldX5_0 ≤ __snapshot_1_oldX5_0
4: __snapshot_1_oldX5_0 ≤ __snapshot_1_oldX5_0 ∧ __snapshot_1_oldX5_0 ≤ __snapshot_1_oldX5_0
7: __snapshot_1_oldX5_0 ≤ __snapshot_1_oldX5_0 ∧ __snapshot_1_oldX5_0 ≤ __snapshot_1_oldX5_0
12: __snapshot_1_oldX5_0 ≤ __snapshot_1_oldX5_0 ∧ __snapshot_1_oldX5_0 ≤ __snapshot_1_oldX5_0
16: __snapshot_1_oldX5_0 ≤ __snapshot_1_oldX5_0 ∧ __snapshot_1_oldX5_0 ≤ __snapshot_1_oldX5_0

9.1.9.1.25 Fresh Variable Addition

The new variable __snapshot_1_oldX4_post is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX4_post ≤ oldX4_post ∧ oldX4_post ≤ __snapshot_1_oldX4_post
40: __snapshot_1_oldX4_post ≤ __snapshot_1_oldX4_post ∧ __snapshot_1_oldX4_post ≤ __snapshot_1_oldX4_post
45: __snapshot_1_oldX4_post ≤ __snapshot_1_oldX4_post ∧ __snapshot_1_oldX4_post ≤ __snapshot_1_oldX4_post
52: __snapshot_1_oldX4_post ≤ __snapshot_1_oldX4_post ∧ __snapshot_1_oldX4_post ≤ __snapshot_1_oldX4_post
0: __snapshot_1_oldX4_post ≤ __snapshot_1_oldX4_post ∧ __snapshot_1_oldX4_post ≤ __snapshot_1_oldX4_post
4: __snapshot_1_oldX4_post ≤ __snapshot_1_oldX4_post ∧ __snapshot_1_oldX4_post ≤ __snapshot_1_oldX4_post
7: __snapshot_1_oldX4_post ≤ __snapshot_1_oldX4_post ∧ __snapshot_1_oldX4_post ≤ __snapshot_1_oldX4_post
12: __snapshot_1_oldX4_post ≤ __snapshot_1_oldX4_post ∧ __snapshot_1_oldX4_post ≤ __snapshot_1_oldX4_post
16: __snapshot_1_oldX4_post ≤ __snapshot_1_oldX4_post ∧ __snapshot_1_oldX4_post ≤ __snapshot_1_oldX4_post

9.1.9.1.26 Fresh Variable Addition

The new variable __snapshot_1_oldX4_0 is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX4_0 ≤ oldX4_0 ∧ oldX4_0 ≤ __snapshot_1_oldX4_0
40: __snapshot_1_oldX4_0 ≤ __snapshot_1_oldX4_0 ∧ __snapshot_1_oldX4_0 ≤ __snapshot_1_oldX4_0
45: __snapshot_1_oldX4_0 ≤ __snapshot_1_oldX4_0 ∧ __snapshot_1_oldX4_0 ≤ __snapshot_1_oldX4_0
52: __snapshot_1_oldX4_0 ≤ __snapshot_1_oldX4_0 ∧ __snapshot_1_oldX4_0 ≤ __snapshot_1_oldX4_0
0: __snapshot_1_oldX4_0 ≤ __snapshot_1_oldX4_0 ∧ __snapshot_1_oldX4_0 ≤ __snapshot_1_oldX4_0
4: __snapshot_1_oldX4_0 ≤ __snapshot_1_oldX4_0 ∧ __snapshot_1_oldX4_0 ≤ __snapshot_1_oldX4_0
7: __snapshot_1_oldX4_0 ≤ __snapshot_1_oldX4_0 ∧ __snapshot_1_oldX4_0 ≤ __snapshot_1_oldX4_0
12: __snapshot_1_oldX4_0 ≤ __snapshot_1_oldX4_0 ∧ __snapshot_1_oldX4_0 ≤ __snapshot_1_oldX4_0
16: __snapshot_1_oldX4_0 ≤ __snapshot_1_oldX4_0 ∧ __snapshot_1_oldX4_0 ≤ __snapshot_1_oldX4_0

9.1.9.1.27 Fresh Variable Addition

The new variable __snapshot_1_oldX3_post is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX3_post ≤ oldX3_post ∧ oldX3_post ≤ __snapshot_1_oldX3_post
40: __snapshot_1_oldX3_post ≤ __snapshot_1_oldX3_post ∧ __snapshot_1_oldX3_post ≤ __snapshot_1_oldX3_post
45: __snapshot_1_oldX3_post ≤ __snapshot_1_oldX3_post ∧ __snapshot_1_oldX3_post ≤ __snapshot_1_oldX3_post
52: __snapshot_1_oldX3_post ≤ __snapshot_1_oldX3_post ∧ __snapshot_1_oldX3_post ≤ __snapshot_1_oldX3_post
0: __snapshot_1_oldX3_post ≤ __snapshot_1_oldX3_post ∧ __snapshot_1_oldX3_post ≤ __snapshot_1_oldX3_post
4: __snapshot_1_oldX3_post ≤ __snapshot_1_oldX3_post ∧ __snapshot_1_oldX3_post ≤ __snapshot_1_oldX3_post
7: __snapshot_1_oldX3_post ≤ __snapshot_1_oldX3_post ∧ __snapshot_1_oldX3_post ≤ __snapshot_1_oldX3_post
12: __snapshot_1_oldX3_post ≤ __snapshot_1_oldX3_post ∧ __snapshot_1_oldX3_post ≤ __snapshot_1_oldX3_post
16: __snapshot_1_oldX3_post ≤ __snapshot_1_oldX3_post ∧ __snapshot_1_oldX3_post ≤ __snapshot_1_oldX3_post

9.1.9.1.28 Fresh Variable Addition

The new variable __snapshot_1_oldX3_0 is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX3_0 ≤ oldX3_0 ∧ oldX3_0 ≤ __snapshot_1_oldX3_0
40: __snapshot_1_oldX3_0 ≤ __snapshot_1_oldX3_0 ∧ __snapshot_1_oldX3_0 ≤ __snapshot_1_oldX3_0
45: __snapshot_1_oldX3_0 ≤ __snapshot_1_oldX3_0 ∧ __snapshot_1_oldX3_0 ≤ __snapshot_1_oldX3_0
52: __snapshot_1_oldX3_0 ≤ __snapshot_1_oldX3_0 ∧ __snapshot_1_oldX3_0 ≤ __snapshot_1_oldX3_0
0: __snapshot_1_oldX3_0 ≤ __snapshot_1_oldX3_0 ∧ __snapshot_1_oldX3_0 ≤ __snapshot_1_oldX3_0
4: __snapshot_1_oldX3_0 ≤ __snapshot_1_oldX3_0 ∧ __snapshot_1_oldX3_0 ≤ __snapshot_1_oldX3_0
7: __snapshot_1_oldX3_0 ≤ __snapshot_1_oldX3_0 ∧ __snapshot_1_oldX3_0 ≤ __snapshot_1_oldX3_0
12: __snapshot_1_oldX3_0 ≤ __snapshot_1_oldX3_0 ∧ __snapshot_1_oldX3_0 ≤ __snapshot_1_oldX3_0
16: __snapshot_1_oldX3_0 ≤ __snapshot_1_oldX3_0 ∧ __snapshot_1_oldX3_0 ≤ __snapshot_1_oldX3_0

9.1.9.1.29 Fresh Variable Addition

The new variable __snapshot_1_oldX2_post is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX2_post ≤ oldX2_post ∧ oldX2_post ≤ __snapshot_1_oldX2_post
40: __snapshot_1_oldX2_post ≤ __snapshot_1_oldX2_post ∧ __snapshot_1_oldX2_post ≤ __snapshot_1_oldX2_post
45: __snapshot_1_oldX2_post ≤ __snapshot_1_oldX2_post ∧ __snapshot_1_oldX2_post ≤ __snapshot_1_oldX2_post
52: __snapshot_1_oldX2_post ≤ __snapshot_1_oldX2_post ∧ __snapshot_1_oldX2_post ≤ __snapshot_1_oldX2_post
0: __snapshot_1_oldX2_post ≤ __snapshot_1_oldX2_post ∧ __snapshot_1_oldX2_post ≤ __snapshot_1_oldX2_post
4: __snapshot_1_oldX2_post ≤ __snapshot_1_oldX2_post ∧ __snapshot_1_oldX2_post ≤ __snapshot_1_oldX2_post
7: __snapshot_1_oldX2_post ≤ __snapshot_1_oldX2_post ∧ __snapshot_1_oldX2_post ≤ __snapshot_1_oldX2_post
12: __snapshot_1_oldX2_post ≤ __snapshot_1_oldX2_post ∧ __snapshot_1_oldX2_post ≤ __snapshot_1_oldX2_post
16: __snapshot_1_oldX2_post ≤ __snapshot_1_oldX2_post ∧ __snapshot_1_oldX2_post ≤ __snapshot_1_oldX2_post

9.1.9.1.30 Fresh Variable Addition

The new variable __snapshot_1_oldX2_0 is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX2_0 ≤ oldX2_0 ∧ oldX2_0 ≤ __snapshot_1_oldX2_0
40: __snapshot_1_oldX2_0 ≤ __snapshot_1_oldX2_0 ∧ __snapshot_1_oldX2_0 ≤ __snapshot_1_oldX2_0
45: __snapshot_1_oldX2_0 ≤ __snapshot_1_oldX2_0 ∧ __snapshot_1_oldX2_0 ≤ __snapshot_1_oldX2_0
52: __snapshot_1_oldX2_0 ≤ __snapshot_1_oldX2_0 ∧ __snapshot_1_oldX2_0 ≤ __snapshot_1_oldX2_0
0: __snapshot_1_oldX2_0 ≤ __snapshot_1_oldX2_0 ∧ __snapshot_1_oldX2_0 ≤ __snapshot_1_oldX2_0
4: __snapshot_1_oldX2_0 ≤ __snapshot_1_oldX2_0 ∧ __snapshot_1_oldX2_0 ≤ __snapshot_1_oldX2_0
7: __snapshot_1_oldX2_0 ≤ __snapshot_1_oldX2_0 ∧ __snapshot_1_oldX2_0 ≤ __snapshot_1_oldX2_0
12: __snapshot_1_oldX2_0 ≤ __snapshot_1_oldX2_0 ∧ __snapshot_1_oldX2_0 ≤ __snapshot_1_oldX2_0
16: __snapshot_1_oldX2_0 ≤ __snapshot_1_oldX2_0 ∧ __snapshot_1_oldX2_0 ≤ __snapshot_1_oldX2_0

9.1.9.1.31 Fresh Variable Addition

The new variable __snapshot_1_oldX1_post is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX1_post ≤ oldX1_post ∧ oldX1_post ≤ __snapshot_1_oldX1_post
40: __snapshot_1_oldX1_post ≤ __snapshot_1_oldX1_post ∧ __snapshot_1_oldX1_post ≤ __snapshot_1_oldX1_post
45: __snapshot_1_oldX1_post ≤ __snapshot_1_oldX1_post ∧ __snapshot_1_oldX1_post ≤ __snapshot_1_oldX1_post
52: __snapshot_1_oldX1_post ≤ __snapshot_1_oldX1_post ∧ __snapshot_1_oldX1_post ≤ __snapshot_1_oldX1_post
0: __snapshot_1_oldX1_post ≤ __snapshot_1_oldX1_post ∧ __snapshot_1_oldX1_post ≤ __snapshot_1_oldX1_post
4: __snapshot_1_oldX1_post ≤ __snapshot_1_oldX1_post ∧ __snapshot_1_oldX1_post ≤ __snapshot_1_oldX1_post
7: __snapshot_1_oldX1_post ≤ __snapshot_1_oldX1_post ∧ __snapshot_1_oldX1_post ≤ __snapshot_1_oldX1_post
12: __snapshot_1_oldX1_post ≤ __snapshot_1_oldX1_post ∧ __snapshot_1_oldX1_post ≤ __snapshot_1_oldX1_post
16: __snapshot_1_oldX1_post ≤ __snapshot_1_oldX1_post ∧ __snapshot_1_oldX1_post ≤ __snapshot_1_oldX1_post

9.1.9.1.32 Fresh Variable Addition

The new variable __snapshot_1_oldX1_0 is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX1_0 ≤ oldX1_0 ∧ oldX1_0 ≤ __snapshot_1_oldX1_0
40: __snapshot_1_oldX1_0 ≤ __snapshot_1_oldX1_0 ∧ __snapshot_1_oldX1_0 ≤ __snapshot_1_oldX1_0
45: __snapshot_1_oldX1_0 ≤ __snapshot_1_oldX1_0 ∧ __snapshot_1_oldX1_0 ≤ __snapshot_1_oldX1_0
52: __snapshot_1_oldX1_0 ≤ __snapshot_1_oldX1_0 ∧ __snapshot_1_oldX1_0 ≤ __snapshot_1_oldX1_0
0: __snapshot_1_oldX1_0 ≤ __snapshot_1_oldX1_0 ∧ __snapshot_1_oldX1_0 ≤ __snapshot_1_oldX1_0
4: __snapshot_1_oldX1_0 ≤ __snapshot_1_oldX1_0 ∧ __snapshot_1_oldX1_0 ≤ __snapshot_1_oldX1_0
7: __snapshot_1_oldX1_0 ≤ __snapshot_1_oldX1_0 ∧ __snapshot_1_oldX1_0 ≤ __snapshot_1_oldX1_0
12: __snapshot_1_oldX1_0 ≤ __snapshot_1_oldX1_0 ∧ __snapshot_1_oldX1_0 ≤ __snapshot_1_oldX1_0
16: __snapshot_1_oldX1_0 ≤ __snapshot_1_oldX1_0 ∧ __snapshot_1_oldX1_0 ≤ __snapshot_1_oldX1_0

9.1.9.1.33 Fresh Variable Addition

The new variable __snapshot_1_oldX13_post is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX13_post ≤ oldX13_post ∧ oldX13_post ≤ __snapshot_1_oldX13_post
40: __snapshot_1_oldX13_post ≤ __snapshot_1_oldX13_post ∧ __snapshot_1_oldX13_post ≤ __snapshot_1_oldX13_post
45: __snapshot_1_oldX13_post ≤ __snapshot_1_oldX13_post ∧ __snapshot_1_oldX13_post ≤ __snapshot_1_oldX13_post
52: __snapshot_1_oldX13_post ≤ __snapshot_1_oldX13_post ∧ __snapshot_1_oldX13_post ≤ __snapshot_1_oldX13_post
0: __snapshot_1_oldX13_post ≤ __snapshot_1_oldX13_post ∧ __snapshot_1_oldX13_post ≤ __snapshot_1_oldX13_post
4: __snapshot_1_oldX13_post ≤ __snapshot_1_oldX13_post ∧ __snapshot_1_oldX13_post ≤ __snapshot_1_oldX13_post
7: __snapshot_1_oldX13_post ≤ __snapshot_1_oldX13_post ∧ __snapshot_1_oldX13_post ≤ __snapshot_1_oldX13_post
12: __snapshot_1_oldX13_post ≤ __snapshot_1_oldX13_post ∧ __snapshot_1_oldX13_post ≤ __snapshot_1_oldX13_post
16: __snapshot_1_oldX13_post ≤ __snapshot_1_oldX13_post ∧ __snapshot_1_oldX13_post ≤ __snapshot_1_oldX13_post

9.1.9.1.34 Fresh Variable Addition

The new variable __snapshot_1_oldX13_0 is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX13_0 ≤ oldX13_0 ∧ oldX13_0 ≤ __snapshot_1_oldX13_0
40: __snapshot_1_oldX13_0 ≤ __snapshot_1_oldX13_0 ∧ __snapshot_1_oldX13_0 ≤ __snapshot_1_oldX13_0
45: __snapshot_1_oldX13_0 ≤ __snapshot_1_oldX13_0 ∧ __snapshot_1_oldX13_0 ≤ __snapshot_1_oldX13_0
52: __snapshot_1_oldX13_0 ≤ __snapshot_1_oldX13_0 ∧ __snapshot_1_oldX13_0 ≤ __snapshot_1_oldX13_0
0: __snapshot_1_oldX13_0 ≤ __snapshot_1_oldX13_0 ∧ __snapshot_1_oldX13_0 ≤ __snapshot_1_oldX13_0
4: __snapshot_1_oldX13_0 ≤ __snapshot_1_oldX13_0 ∧ __snapshot_1_oldX13_0 ≤ __snapshot_1_oldX13_0
7: __snapshot_1_oldX13_0 ≤ __snapshot_1_oldX13_0 ∧ __snapshot_1_oldX13_0 ≤ __snapshot_1_oldX13_0
12: __snapshot_1_oldX13_0 ≤ __snapshot_1_oldX13_0 ∧ __snapshot_1_oldX13_0 ≤ __snapshot_1_oldX13_0
16: __snapshot_1_oldX13_0 ≤ __snapshot_1_oldX13_0 ∧ __snapshot_1_oldX13_0 ≤ __snapshot_1_oldX13_0

9.1.9.1.35 Fresh Variable Addition

The new variable __snapshot_1_oldX12_post is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX12_post ≤ oldX12_post ∧ oldX12_post ≤ __snapshot_1_oldX12_post
40: __snapshot_1_oldX12_post ≤ __snapshot_1_oldX12_post ∧ __snapshot_1_oldX12_post ≤ __snapshot_1_oldX12_post
45: __snapshot_1_oldX12_post ≤ __snapshot_1_oldX12_post ∧ __snapshot_1_oldX12_post ≤ __snapshot_1_oldX12_post
52: __snapshot_1_oldX12_post ≤ __snapshot_1_oldX12_post ∧ __snapshot_1_oldX12_post ≤ __snapshot_1_oldX12_post
0: __snapshot_1_oldX12_post ≤ __snapshot_1_oldX12_post ∧ __snapshot_1_oldX12_post ≤ __snapshot_1_oldX12_post
4: __snapshot_1_oldX12_post ≤ __snapshot_1_oldX12_post ∧ __snapshot_1_oldX12_post ≤ __snapshot_1_oldX12_post
7: __snapshot_1_oldX12_post ≤ __snapshot_1_oldX12_post ∧ __snapshot_1_oldX12_post ≤ __snapshot_1_oldX12_post
12: __snapshot_1_oldX12_post ≤ __snapshot_1_oldX12_post ∧ __snapshot_1_oldX12_post ≤ __snapshot_1_oldX12_post
16: __snapshot_1_oldX12_post ≤ __snapshot_1_oldX12_post ∧ __snapshot_1_oldX12_post ≤ __snapshot_1_oldX12_post

9.1.9.1.36 Fresh Variable Addition

The new variable __snapshot_1_oldX12_0 is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX12_0 ≤ oldX12_0 ∧ oldX12_0 ≤ __snapshot_1_oldX12_0
40: __snapshot_1_oldX12_0 ≤ __snapshot_1_oldX12_0 ∧ __snapshot_1_oldX12_0 ≤ __snapshot_1_oldX12_0
45: __snapshot_1_oldX12_0 ≤ __snapshot_1_oldX12_0 ∧ __snapshot_1_oldX12_0 ≤ __snapshot_1_oldX12_0
52: __snapshot_1_oldX12_0 ≤ __snapshot_1_oldX12_0 ∧ __snapshot_1_oldX12_0 ≤ __snapshot_1_oldX12_0
0: __snapshot_1_oldX12_0 ≤ __snapshot_1_oldX12_0 ∧ __snapshot_1_oldX12_0 ≤ __snapshot_1_oldX12_0
4: __snapshot_1_oldX12_0 ≤ __snapshot_1_oldX12_0 ∧ __snapshot_1_oldX12_0 ≤ __snapshot_1_oldX12_0
7: __snapshot_1_oldX12_0 ≤ __snapshot_1_oldX12_0 ∧ __snapshot_1_oldX12_0 ≤ __snapshot_1_oldX12_0
12: __snapshot_1_oldX12_0 ≤ __snapshot_1_oldX12_0 ∧ __snapshot_1_oldX12_0 ≤ __snapshot_1_oldX12_0
16: __snapshot_1_oldX12_0 ≤ __snapshot_1_oldX12_0 ∧ __snapshot_1_oldX12_0 ≤ __snapshot_1_oldX12_0

9.1.9.1.37 Fresh Variable Addition

The new variable __snapshot_1_oldX11_post is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX11_post ≤ oldX11_post ∧ oldX11_post ≤ __snapshot_1_oldX11_post
40: __snapshot_1_oldX11_post ≤ __snapshot_1_oldX11_post ∧ __snapshot_1_oldX11_post ≤ __snapshot_1_oldX11_post
45: __snapshot_1_oldX11_post ≤ __snapshot_1_oldX11_post ∧ __snapshot_1_oldX11_post ≤ __snapshot_1_oldX11_post
52: __snapshot_1_oldX11_post ≤ __snapshot_1_oldX11_post ∧ __snapshot_1_oldX11_post ≤ __snapshot_1_oldX11_post
0: __snapshot_1_oldX11_post ≤ __snapshot_1_oldX11_post ∧ __snapshot_1_oldX11_post ≤ __snapshot_1_oldX11_post
4: __snapshot_1_oldX11_post ≤ __snapshot_1_oldX11_post ∧ __snapshot_1_oldX11_post ≤ __snapshot_1_oldX11_post
7: __snapshot_1_oldX11_post ≤ __snapshot_1_oldX11_post ∧ __snapshot_1_oldX11_post ≤ __snapshot_1_oldX11_post
12: __snapshot_1_oldX11_post ≤ __snapshot_1_oldX11_post ∧ __snapshot_1_oldX11_post ≤ __snapshot_1_oldX11_post
16: __snapshot_1_oldX11_post ≤ __snapshot_1_oldX11_post ∧ __snapshot_1_oldX11_post ≤ __snapshot_1_oldX11_post

9.1.9.1.38 Fresh Variable Addition

The new variable __snapshot_1_oldX11_0 is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX11_0 ≤ oldX11_0 ∧ oldX11_0 ≤ __snapshot_1_oldX11_0
40: __snapshot_1_oldX11_0 ≤ __snapshot_1_oldX11_0 ∧ __snapshot_1_oldX11_0 ≤ __snapshot_1_oldX11_0
45: __snapshot_1_oldX11_0 ≤ __snapshot_1_oldX11_0 ∧ __snapshot_1_oldX11_0 ≤ __snapshot_1_oldX11_0
52: __snapshot_1_oldX11_0 ≤ __snapshot_1_oldX11_0 ∧ __snapshot_1_oldX11_0 ≤ __snapshot_1_oldX11_0
0: __snapshot_1_oldX11_0 ≤ __snapshot_1_oldX11_0 ∧ __snapshot_1_oldX11_0 ≤ __snapshot_1_oldX11_0
4: __snapshot_1_oldX11_0 ≤ __snapshot_1_oldX11_0 ∧ __snapshot_1_oldX11_0 ≤ __snapshot_1_oldX11_0
7: __snapshot_1_oldX11_0 ≤ __snapshot_1_oldX11_0 ∧ __snapshot_1_oldX11_0 ≤ __snapshot_1_oldX11_0
12: __snapshot_1_oldX11_0 ≤ __snapshot_1_oldX11_0 ∧ __snapshot_1_oldX11_0 ≤ __snapshot_1_oldX11_0
16: __snapshot_1_oldX11_0 ≤ __snapshot_1_oldX11_0 ∧ __snapshot_1_oldX11_0 ≤ __snapshot_1_oldX11_0

9.1.9.1.39 Fresh Variable Addition

The new variable __snapshot_1_oldX10_post is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX10_post ≤ oldX10_post ∧ oldX10_post ≤ __snapshot_1_oldX10_post
40: __snapshot_1_oldX10_post ≤ __snapshot_1_oldX10_post ∧ __snapshot_1_oldX10_post ≤ __snapshot_1_oldX10_post
45: __snapshot_1_oldX10_post ≤ __snapshot_1_oldX10_post ∧ __snapshot_1_oldX10_post ≤ __snapshot_1_oldX10_post
52: __snapshot_1_oldX10_post ≤ __snapshot_1_oldX10_post ∧ __snapshot_1_oldX10_post ≤ __snapshot_1_oldX10_post
0: __snapshot_1_oldX10_post ≤ __snapshot_1_oldX10_post ∧ __snapshot_1_oldX10_post ≤ __snapshot_1_oldX10_post
4: __snapshot_1_oldX10_post ≤ __snapshot_1_oldX10_post ∧ __snapshot_1_oldX10_post ≤ __snapshot_1_oldX10_post
7: __snapshot_1_oldX10_post ≤ __snapshot_1_oldX10_post ∧ __snapshot_1_oldX10_post ≤ __snapshot_1_oldX10_post
12: __snapshot_1_oldX10_post ≤ __snapshot_1_oldX10_post ∧ __snapshot_1_oldX10_post ≤ __snapshot_1_oldX10_post
16: __snapshot_1_oldX10_post ≤ __snapshot_1_oldX10_post ∧ __snapshot_1_oldX10_post ≤ __snapshot_1_oldX10_post

9.1.9.1.40 Fresh Variable Addition

The new variable __snapshot_1_oldX10_0 is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX10_0 ≤ oldX10_0 ∧ oldX10_0 ≤ __snapshot_1_oldX10_0
40: __snapshot_1_oldX10_0 ≤ __snapshot_1_oldX10_0 ∧ __snapshot_1_oldX10_0 ≤ __snapshot_1_oldX10_0
45: __snapshot_1_oldX10_0 ≤ __snapshot_1_oldX10_0 ∧ __snapshot_1_oldX10_0 ≤ __snapshot_1_oldX10_0
52: __snapshot_1_oldX10_0 ≤ __snapshot_1_oldX10_0 ∧ __snapshot_1_oldX10_0 ≤ __snapshot_1_oldX10_0
0: __snapshot_1_oldX10_0 ≤ __snapshot_1_oldX10_0 ∧ __snapshot_1_oldX10_0 ≤ __snapshot_1_oldX10_0
4: __snapshot_1_oldX10_0 ≤ __snapshot_1_oldX10_0 ∧ __snapshot_1_oldX10_0 ≤ __snapshot_1_oldX10_0
7: __snapshot_1_oldX10_0 ≤ __snapshot_1_oldX10_0 ∧ __snapshot_1_oldX10_0 ≤ __snapshot_1_oldX10_0
12: __snapshot_1_oldX10_0 ≤ __snapshot_1_oldX10_0 ∧ __snapshot_1_oldX10_0 ≤ __snapshot_1_oldX10_0
16: __snapshot_1_oldX10_0 ≤ __snapshot_1_oldX10_0 ∧ __snapshot_1_oldX10_0 ≤ __snapshot_1_oldX10_0

9.1.9.1.41 Fresh Variable Addition

The new variable __snapshot_1_oldX0_post is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX0_post ≤ oldX0_post ∧ oldX0_post ≤ __snapshot_1_oldX0_post
40: __snapshot_1_oldX0_post ≤ __snapshot_1_oldX0_post ∧ __snapshot_1_oldX0_post ≤ __snapshot_1_oldX0_post
45: __snapshot_1_oldX0_post ≤ __snapshot_1_oldX0_post ∧ __snapshot_1_oldX0_post ≤ __snapshot_1_oldX0_post
52: __snapshot_1_oldX0_post ≤ __snapshot_1_oldX0_post ∧ __snapshot_1_oldX0_post ≤ __snapshot_1_oldX0_post
0: __snapshot_1_oldX0_post ≤ __snapshot_1_oldX0_post ∧ __snapshot_1_oldX0_post ≤ __snapshot_1_oldX0_post
4: __snapshot_1_oldX0_post ≤ __snapshot_1_oldX0_post ∧ __snapshot_1_oldX0_post ≤ __snapshot_1_oldX0_post
7: __snapshot_1_oldX0_post ≤ __snapshot_1_oldX0_post ∧ __snapshot_1_oldX0_post ≤ __snapshot_1_oldX0_post
12: __snapshot_1_oldX0_post ≤ __snapshot_1_oldX0_post ∧ __snapshot_1_oldX0_post ≤ __snapshot_1_oldX0_post
16: __snapshot_1_oldX0_post ≤ __snapshot_1_oldX0_post ∧ __snapshot_1_oldX0_post ≤ __snapshot_1_oldX0_post

9.1.9.1.42 Fresh Variable Addition

The new variable __snapshot_1_oldX0_0 is introduced. The transition formulas are extended as follows:

38: __snapshot_1_oldX0_0 ≤ oldX0_0 ∧ oldX0_0 ≤ __snapshot_1_oldX0_0
40: __snapshot_1_oldX0_0 ≤ __snapshot_1_oldX0_0 ∧ __snapshot_1_oldX0_0 ≤ __snapshot_1_oldX0_0
45: __snapshot_1_oldX0_0 ≤ __snapshot_1_oldX0_0 ∧ __snapshot_1_oldX0_0 ≤ __snapshot_1_oldX0_0
52: __snapshot_1_oldX0_0 ≤ __snapshot_1_oldX0_0 ∧ __snapshot_1_oldX0_0 ≤ __snapshot_1_oldX0_0
0: __snapshot_1_oldX0_0 ≤ __snapshot_1_oldX0_0 ∧ __snapshot_1_oldX0_0 ≤ __snapshot_1_oldX0_0
4: __snapshot_1_oldX0_0 ≤ __snapshot_1_oldX0_0 ∧ __snapshot_1_oldX0_0 ≤ __snapshot_1_oldX0_0
7: __snapshot_1_oldX0_0 ≤ __snapshot_1_oldX0_0 ∧ __snapshot_1_oldX0_0 ≤ __snapshot_1_oldX0_0
12: __snapshot_1_oldX0_0 ≤ __snapshot_1_oldX0_0 ∧ __snapshot_1_oldX0_0 ≤ __snapshot_1_oldX0_0
16: __snapshot_1_oldX0_0 ≤ __snapshot_1_oldX0_0 ∧ __snapshot_1_oldX0_0 ≤ __snapshot_1_oldX0_0

9.1.9.1.43 Invariant Updates

The following invariants are asserted.

0: TRUE
1: TRUE
2: TRUE
3: TRUE
4: TRUE
5: TRUE
6: TRUE
7: TRUE
8: TRUE
9: TRUE
10: TRUE
11: TRUE
12: TRUE
0: __snapshot_1_x4_0 ≤ 0 ∧ 1 − __snapshot_1_x1_0 + __snapshot_1_x4_0 + __snapshot_1_x5_0 ≤ 0 ∧ 1 − __snapshot_1_x1_0 + __snapshot_1_x4_0 + __snapshot_1_x5_0 + x1_0 − x4_0 − x6_0 ≤ 0
1: TRUE ∨ __snapshot_1_x4_0 ≤ 0 ∧ 1 − __snapshot_1_x1_0 + __snapshot_1_x4_0 + __snapshot_1_x5_0 ≤ 0 ∧ 1 − __snapshot_1_x1_0 + __snapshot_1_x4_0 + __snapshot_1_x5_0 + x1_0 − x4_0 − x5_0 ≤ 0 ∧ 1 + __snapshot_1_x4_0 − x4_0 ≤ 0 ∨ __snapshot_1_x4_0 ≤ 0 ∧ 1 − __snapshot_1_x1_0 + __snapshot_1_x4_0 + __snapshot_1_x5_0 ≤ 0 ∧ 1 − __snapshot_1_x1_0 + __snapshot_1_x4_0 + __snapshot_1_x5_0 + x1_0 − x4_0 − x5_0 ≤ 0
2: 1 ≤ 0
3: FALSE
4: FALSE
5: __snapshot_1_x4_0 ≤ 0 ∧ 1 − __snapshot_1_x1_0 + __snapshot_1_x4_0 + __snapshot_1_x5_0 ≤ 0 ∧ − __snapshot_1_x1_0 + __snapshot_1_x4_0 + __snapshot_1_x5_0 + x1_0 − x4_0 − x5_0 ≤ 0 ∧ − __snapshot_1_x1_0 + __snapshot_1_x4_0 + __snapshot_1_x5_0 + x1_0 − x5_0 ≤ 0
8: 1 ≤ 0
9: 1 ≤ 0
1_var_snapshot: − __snapshot_1_x1_0 + __snapshot_1_x4_0 + __snapshot_1_x5_0 + x1_0 − x4_0 − x5_0 ≤ 0 ∧ __snapshot_1_x4_0 − x4_0 ≤ 0
1*: __snapshot_1_x4_0 ≤ 0 ∧ 1 − __snapshot_1_x1_0 + __snapshot_1_x4_0 + __snapshot_1_x5_0 ≤ 0 ∧ 1 − __snapshot_1_x1_0 + __snapshot_1_x4_0 + __snapshot_1_x5_0 + x1_0 − x4_0 − x5_0 ≤ 0 ∧ 1 + __snapshot_1_x4_0 − x4_0 ≤ 0 ∨ __snapshot_1_x4_0 ≤ 0 ∧ 1 − __snapshot_1_x1_0 + __snapshot_1_x4_0 + __snapshot_1_x5_0 ≤ 0 ∧ 1 − __snapshot_1_x1_0 + __snapshot_1_x4_0 + __snapshot_1_x5_0 + x1_0 − x4_0 − x5_0 ≤ 0
3_var_snapshot: 1 ≤ 0
3*: 1 ≤ 0
4_var_snapshot: 1 ≤ 0
4*: 1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

9.1.9.1.44 Transition Removal

We remove transition 40 using the following lexicographic ranking functions, which are bounded by [−1, −2].

0: [__snapshot_1_x1_0 − __snapshot_1_x4_0 − __snapshot_1_x5_0, − __snapshot_1_x4_0]
1: [x1_0 − x4_0 − x5_0, − x4_0]
2: [__snapshot_1_x1_0 − __snapshot_1_x4_0 − __snapshot_1_x5_0, − __snapshot_1_x4_0]
3: [__snapshot_1_x1_0 − __snapshot_1_x4_0 − __snapshot_1_x5_0, − __snapshot_1_x4_0]
4: [__snapshot_1_x1_0 − __snapshot_1_x4_0 − __snapshot_1_x5_0, − __snapshot_1_x4_0]
5: [__snapshot_1_x1_0 − __snapshot_1_x4_0 − __snapshot_1_x5_0, − __snapshot_1_x4_0]
8: [__snapshot_1_x1_0 − __snapshot_1_x4_0 − __snapshot_1_x5_0, − __snapshot_1_x4_0]
9: [__snapshot_1_x1_0 − __snapshot_1_x4_0 − __snapshot_1_x5_0, − __snapshot_1_x4_0]
1_var_snapshot: [__snapshot_1_x1_0 − __snapshot_1_x4_0 − __snapshot_1_x5_0, − __snapshot_1_x4_0]
1*: [__snapshot_1_x1_0 − __snapshot_1_x4_0 − __snapshot_1_x5_0, − __snapshot_1_x4_0]
3_var_snapshot: [__snapshot_1_x1_0 − __snapshot_1_x4_0 − __snapshot_1_x5_0, − __snapshot_1_x4_0]
3*: [__snapshot_1_x1_0 − __snapshot_1_x4_0 − __snapshot_1_x5_0, − __snapshot_1_x4_0]
4_var_snapshot: [__snapshot_1_x1_0 − __snapshot_1_x4_0 − __snapshot_1_x5_0, − __snapshot_1_x4_0]
4*: [__snapshot_1_x1_0 − __snapshot_1_x4_0 − __snapshot_1_x5_0, − __snapshot_1_x4_0]

9.1.9.1.45 Transition Removal

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

1: −1
2: −2
3: −3
4: −4
8: −5
9: −6
1_var_snapshot: −7
5: −8
0: −9
1*: −10
3_var_snapshot: −11
3*: −12
4_var_snapshot: −13
4*: −14

9.1.9.1.46 Splitting Cut-Point Transitions

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

9.1.9.2 Cut-Point Subproblem 2/3

Here we consider cut-point transition 44.

9.1.9.2.1 Splitting Cut-Point Transitions

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

9.1.9.3 Cut-Point Subproblem 3/3

Here we consider cut-point transition 51.

9.1.9.3.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert