LTS Termination Proof

by T2Cert

Input

Integer Transition System

Initial Location: 11

Transitions: (pre-variables and post-variables)

0	0	1:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ − oldX2_post + x0_post ≤ 0 ∧ oldX2_post − x0_post ≤ 0 ∧ − oldX3_post + x1_post ≤ 0 ∧ oldX3_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ oldX2_0 − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_post ≤ 0 ∧ oldX3_0 − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0
0	1	2:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ 1 − oldX1_post + x1_post ≤ 0 ∧ −1 + oldX1_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 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
3	2	4:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ 2 − oldX2_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ oldX2_0 − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 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
3	3	4:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ oldX2_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ oldX2_0 − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 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
3	4	0:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ −1 + oldX2_post ≤ 0 ∧ 1 − oldX2_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ oldX2_0 − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 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
5	5	1:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ − oldX2_post + x0_post ≤ 0 ∧ oldX2_post − x0_post ≤ 0 ∧ − oldX3_post + x1_post ≤ 0 ∧ oldX3_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ oldX2_0 − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_post ≤ 0 ∧ oldX3_0 − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0
6	6	3:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ 3 − oldX0_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 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
6	7	3:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ −1 + oldX0_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 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
6	8	5:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ −2 + oldX0_post ≤ 0 ∧ 2 − oldX0_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 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
7	9	6:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ 2 − oldX1_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 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
7	10	6:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ oldX1_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 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
7	11	8:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ −1 + oldX1_post ≤ 0 ∧ 1 − oldX1_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 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
8	12	1:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ − oldX2_post + x0_post ≤ 0 ∧ oldX2_post − x0_post ≤ 0 ∧ − oldX3_post + x1_post ≤ 0 ∧ oldX3_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ oldX2_0 − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_post ≤ 0 ∧ oldX3_0 − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0
9	13	7:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ 1 − oldX1_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 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
9	14	8:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ oldX1_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 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
4	15	1:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ 2 − oldX1_post + 2⋅oldX4_post ≤ 0 ∧ − oldX2_post + x0_post ≤ 0 ∧ oldX2_post − x0_post ≤ 0 ∧ − oldX3_post + x1_post ≤ 0 ∧ oldX3_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ oldX2_0 − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_post ≤ 0 ∧ oldX3_0 − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_post ≤ 0 ∧ oldX4_0 − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0
4	16	1:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ 1 + oldX1_post − 2⋅oldX4_post ≤ 0 ∧ − oldX2_post + x0_post ≤ 0 ∧ oldX2_post − x0_post ≤ 0 ∧ − oldX3_post + x1_post ≤ 0 ∧ oldX3_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ oldX2_0 − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_post ≤ 0 ∧ oldX3_0 − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_post ≤ 0 ∧ oldX4_0 − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0
4	17	1:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ − oldX1_post + 2⋅oldX4_post ≤ 0 ∧ −1 + oldX1_post − 2⋅oldX4_post ≤ 0 ∧ − oldX2_post + x0_post ≤ 0 ∧ oldX2_post − x0_post ≤ 0 ∧ − oldX3_post + x1_post ≤ 0 ∧ oldX3_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ oldX2_0 − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_post ≤ 0 ∧ oldX3_0 − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_post ≤ 0 ∧ oldX4_0 − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0
4	18	2:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ − oldX1_post + 2⋅oldX2_post ≤ 0 ∧ −1 + oldX1_post − 2⋅oldX2_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX2_post + x1_post ≤ 0 ∧ oldX2_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ oldX2_0 − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 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
2	19	9:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 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
10	20	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 ∧ − 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 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0
10	21	3:	− 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 ∧ − 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 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0
10	22	5:	− 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 ∧ − 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 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0
10	23	1:	− 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 ∧ − 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 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0
10	24	6:	− 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 ∧ − 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 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0
10	25	7:	− 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 ∧ − 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 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0
10	26	8:	− 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 ∧ − 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 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0
10	27	9:	− 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 ∧ − 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 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0
10	28	4:	− 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 ∧ − 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 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0
10	29	2:	− 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 ∧ − 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 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0
11	30	10:	− 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 ∧ − 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 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:

− 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 ∧ − 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 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0

and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 0, 5, 8, 11, 12, 14, 15, 16, 17, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30 using the following ranking functions, which are bounded by −17.

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

3 Location Addition

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

2* 34 2: − 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 ∧ − 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 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0

4 Location Addition

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

2 32 2_var_snapshot: − 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 ∧ − 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 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0

5 SCC Decomposition

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

5.1 SCC Subproblem 1/1

Here we consider the SCC { 0, 2, 3, 4, 6, 7, 9, 2_var_snapshot, 2* }.

5.1.1 Splitting Cut-Point Transitions

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

5.1.1.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 31.

5.1.1.1.1 Fresh Variable Addition

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

32:	__snapshot_2_x1_post ≤ x1_post ∧ x1_post ≤ __snapshot_2_x1_post
34:	__snapshot_2_x1_post ≤ __snapshot_2_x1_post ∧ __snapshot_2_x1_post ≤ __snapshot_2_x1_post
1:	__snapshot_2_x1_post ≤ __snapshot_2_x1_post ∧ __snapshot_2_x1_post ≤ __snapshot_2_x1_post
2:	__snapshot_2_x1_post ≤ __snapshot_2_x1_post ∧ __snapshot_2_x1_post ≤ __snapshot_2_x1_post
3:	__snapshot_2_x1_post ≤ __snapshot_2_x1_post ∧ __snapshot_2_x1_post ≤ __snapshot_2_x1_post
4:	__snapshot_2_x1_post ≤ __snapshot_2_x1_post ∧ __snapshot_2_x1_post ≤ __snapshot_2_x1_post
6:	__snapshot_2_x1_post ≤ __snapshot_2_x1_post ∧ __snapshot_2_x1_post ≤ __snapshot_2_x1_post
7:	__snapshot_2_x1_post ≤ __snapshot_2_x1_post ∧ __snapshot_2_x1_post ≤ __snapshot_2_x1_post
9:	__snapshot_2_x1_post ≤ __snapshot_2_x1_post ∧ __snapshot_2_x1_post ≤ __snapshot_2_x1_post
10:	__snapshot_2_x1_post ≤ __snapshot_2_x1_post ∧ __snapshot_2_x1_post ≤ __snapshot_2_x1_post
13:	__snapshot_2_x1_post ≤ __snapshot_2_x1_post ∧ __snapshot_2_x1_post ≤ __snapshot_2_x1_post
18:	__snapshot_2_x1_post ≤ __snapshot_2_x1_post ∧ __snapshot_2_x1_post ≤ __snapshot_2_x1_post
19:	__snapshot_2_x1_post ≤ __snapshot_2_x1_post ∧ __snapshot_2_x1_post ≤ __snapshot_2_x1_post

5.1.1.1.2 Fresh Variable Addition

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

32:	__snapshot_2_x1_0 ≤ x1_0 ∧ x1_0 ≤ __snapshot_2_x1_0
34:	__snapshot_2_x1_0 ≤ __snapshot_2_x1_0 ∧ __snapshot_2_x1_0 ≤ __snapshot_2_x1_0
1:	__snapshot_2_x1_0 ≤ __snapshot_2_x1_0 ∧ __snapshot_2_x1_0 ≤ __snapshot_2_x1_0
2:	__snapshot_2_x1_0 ≤ __snapshot_2_x1_0 ∧ __snapshot_2_x1_0 ≤ __snapshot_2_x1_0
3:	__snapshot_2_x1_0 ≤ __snapshot_2_x1_0 ∧ __snapshot_2_x1_0 ≤ __snapshot_2_x1_0
4:	__snapshot_2_x1_0 ≤ __snapshot_2_x1_0 ∧ __snapshot_2_x1_0 ≤ __snapshot_2_x1_0
6:	__snapshot_2_x1_0 ≤ __snapshot_2_x1_0 ∧ __snapshot_2_x1_0 ≤ __snapshot_2_x1_0
7:	__snapshot_2_x1_0 ≤ __snapshot_2_x1_0 ∧ __snapshot_2_x1_0 ≤ __snapshot_2_x1_0
9:	__snapshot_2_x1_0 ≤ __snapshot_2_x1_0 ∧ __snapshot_2_x1_0 ≤ __snapshot_2_x1_0
10:	__snapshot_2_x1_0 ≤ __snapshot_2_x1_0 ∧ __snapshot_2_x1_0 ≤ __snapshot_2_x1_0
13:	__snapshot_2_x1_0 ≤ __snapshot_2_x1_0 ∧ __snapshot_2_x1_0 ≤ __snapshot_2_x1_0
18:	__snapshot_2_x1_0 ≤ __snapshot_2_x1_0 ∧ __snapshot_2_x1_0 ≤ __snapshot_2_x1_0
19:	__snapshot_2_x1_0 ≤ __snapshot_2_x1_0 ∧ __snapshot_2_x1_0 ≤ __snapshot_2_x1_0

5.1.1.1.3 Fresh Variable Addition

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

32:	__snapshot_2_x0_post ≤ x0_post ∧ x0_post ≤ __snapshot_2_x0_post
34:	__snapshot_2_x0_post ≤ __snapshot_2_x0_post ∧ __snapshot_2_x0_post ≤ __snapshot_2_x0_post
1:	__snapshot_2_x0_post ≤ __snapshot_2_x0_post ∧ __snapshot_2_x0_post ≤ __snapshot_2_x0_post
2:	__snapshot_2_x0_post ≤ __snapshot_2_x0_post ∧ __snapshot_2_x0_post ≤ __snapshot_2_x0_post
3:	__snapshot_2_x0_post ≤ __snapshot_2_x0_post ∧ __snapshot_2_x0_post ≤ __snapshot_2_x0_post
4:	__snapshot_2_x0_post ≤ __snapshot_2_x0_post ∧ __snapshot_2_x0_post ≤ __snapshot_2_x0_post
6:	__snapshot_2_x0_post ≤ __snapshot_2_x0_post ∧ __snapshot_2_x0_post ≤ __snapshot_2_x0_post
7:	__snapshot_2_x0_post ≤ __snapshot_2_x0_post ∧ __snapshot_2_x0_post ≤ __snapshot_2_x0_post
9:	__snapshot_2_x0_post ≤ __snapshot_2_x0_post ∧ __snapshot_2_x0_post ≤ __snapshot_2_x0_post
10:	__snapshot_2_x0_post ≤ __snapshot_2_x0_post ∧ __snapshot_2_x0_post ≤ __snapshot_2_x0_post
13:	__snapshot_2_x0_post ≤ __snapshot_2_x0_post ∧ __snapshot_2_x0_post ≤ __snapshot_2_x0_post
18:	__snapshot_2_x0_post ≤ __snapshot_2_x0_post ∧ __snapshot_2_x0_post ≤ __snapshot_2_x0_post
19:	__snapshot_2_x0_post ≤ __snapshot_2_x0_post ∧ __snapshot_2_x0_post ≤ __snapshot_2_x0_post

5.1.1.1.4 Fresh Variable Addition

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

32:	__snapshot_2_x0_0 ≤ x0_0 ∧ x0_0 ≤ __snapshot_2_x0_0
34:	__snapshot_2_x0_0 ≤ __snapshot_2_x0_0 ∧ __snapshot_2_x0_0 ≤ __snapshot_2_x0_0
1:	__snapshot_2_x0_0 ≤ __snapshot_2_x0_0 ∧ __snapshot_2_x0_0 ≤ __snapshot_2_x0_0
2:	__snapshot_2_x0_0 ≤ __snapshot_2_x0_0 ∧ __snapshot_2_x0_0 ≤ __snapshot_2_x0_0
3:	__snapshot_2_x0_0 ≤ __snapshot_2_x0_0 ∧ __snapshot_2_x0_0 ≤ __snapshot_2_x0_0
4:	__snapshot_2_x0_0 ≤ __snapshot_2_x0_0 ∧ __snapshot_2_x0_0 ≤ __snapshot_2_x0_0
6:	__snapshot_2_x0_0 ≤ __snapshot_2_x0_0 ∧ __snapshot_2_x0_0 ≤ __snapshot_2_x0_0
7:	__snapshot_2_x0_0 ≤ __snapshot_2_x0_0 ∧ __snapshot_2_x0_0 ≤ __snapshot_2_x0_0
9:	__snapshot_2_x0_0 ≤ __snapshot_2_x0_0 ∧ __snapshot_2_x0_0 ≤ __snapshot_2_x0_0
10:	__snapshot_2_x0_0 ≤ __snapshot_2_x0_0 ∧ __snapshot_2_x0_0 ≤ __snapshot_2_x0_0
13:	__snapshot_2_x0_0 ≤ __snapshot_2_x0_0 ∧ __snapshot_2_x0_0 ≤ __snapshot_2_x0_0
18:	__snapshot_2_x0_0 ≤ __snapshot_2_x0_0 ∧ __snapshot_2_x0_0 ≤ __snapshot_2_x0_0
19:	__snapshot_2_x0_0 ≤ __snapshot_2_x0_0 ∧ __snapshot_2_x0_0 ≤ __snapshot_2_x0_0

5.1.1.1.5 Fresh Variable Addition

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

32:	__snapshot_2_oldX4_post ≤ oldX4_post ∧ oldX4_post ≤ __snapshot_2_oldX4_post
34:	__snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post ∧ __snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post
1:	__snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post ∧ __snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post
2:	__snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post ∧ __snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post
3:	__snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post ∧ __snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post
4:	__snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post ∧ __snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post
6:	__snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post ∧ __snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post
7:	__snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post ∧ __snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post
9:	__snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post ∧ __snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post
10:	__snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post ∧ __snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post
13:	__snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post ∧ __snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post
18:	__snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post ∧ __snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post
19:	__snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post ∧ __snapshot_2_oldX4_post ≤ __snapshot_2_oldX4_post

5.1.1.1.6 Fresh Variable Addition

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

32:	__snapshot_2_oldX4_0 ≤ oldX4_0 ∧ oldX4_0 ≤ __snapshot_2_oldX4_0
34:	__snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0 ∧ __snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0
1:	__snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0 ∧ __snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0
2:	__snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0 ∧ __snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0
3:	__snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0 ∧ __snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0
4:	__snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0 ∧ __snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0
6:	__snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0 ∧ __snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0
7:	__snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0 ∧ __snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0
9:	__snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0 ∧ __snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0
10:	__snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0 ∧ __snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0
13:	__snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0 ∧ __snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0
18:	__snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0 ∧ __snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0
19:	__snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0 ∧ __snapshot_2_oldX4_0 ≤ __snapshot_2_oldX4_0

5.1.1.1.7 Fresh Variable Addition

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

32:	__snapshot_2_oldX3_post ≤ oldX3_post ∧ oldX3_post ≤ __snapshot_2_oldX3_post
34:	__snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post ∧ __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post
1:	__snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post ∧ __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post
2:	__snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post ∧ __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post
3:	__snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post ∧ __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post
4:	__snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post ∧ __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post
6:	__snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post ∧ __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post
7:	__snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post ∧ __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post
9:	__snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post ∧ __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post
10:	__snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post ∧ __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post
13:	__snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post ∧ __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post
18:	__snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post ∧ __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post
19:	__snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post ∧ __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post

5.1.1.1.8 Fresh Variable Addition

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

32:	__snapshot_2_oldX3_0 ≤ oldX3_0 ∧ oldX3_0 ≤ __snapshot_2_oldX3_0
34:	__snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 ∧ __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0
1:	__snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 ∧ __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0
2:	__snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 ∧ __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0
3:	__snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 ∧ __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0
4:	__snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 ∧ __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0
6:	__snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 ∧ __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0
7:	__snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 ∧ __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0
9:	__snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 ∧ __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0
10:	__snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 ∧ __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0
13:	__snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 ∧ __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0
18:	__snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 ∧ __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0
19:	__snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 ∧ __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0

5.1.1.1.9 Fresh Variable Addition

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

32:	__snapshot_2_oldX2_post ≤ oldX2_post ∧ oldX2_post ≤ __snapshot_2_oldX2_post
34:	__snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post ∧ __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post
1:	__snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post ∧ __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post
2:	__snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post ∧ __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post
3:	__snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post ∧ __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post
4:	__snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post ∧ __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post
6:	__snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post ∧ __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post
7:	__snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post ∧ __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post
9:	__snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post ∧ __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post
10:	__snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post ∧ __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post
13:	__snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post ∧ __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post
18:	__snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post ∧ __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post
19:	__snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post ∧ __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post

5.1.1.1.10 Fresh Variable Addition

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

32:	__snapshot_2_oldX2_0 ≤ oldX2_0 ∧ oldX2_0 ≤ __snapshot_2_oldX2_0
34:	__snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 ∧ __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0
1:	__snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 ∧ __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0
2:	__snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 ∧ __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0
3:	__snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 ∧ __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0
4:	__snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 ∧ __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0
6:	__snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 ∧ __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0
7:	__snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 ∧ __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0
9:	__snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 ∧ __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0
10:	__snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 ∧ __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0
13:	__snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 ∧ __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0
18:	__snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 ∧ __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0
19:	__snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 ∧ __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0

5.1.1.1.11 Fresh Variable Addition

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

32:	__snapshot_2_oldX1_post ≤ oldX1_post ∧ oldX1_post ≤ __snapshot_2_oldX1_post
34:	__snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post ∧ __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post
1:	__snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post ∧ __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post
2:	__snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post ∧ __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post
3:	__snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post ∧ __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post
4:	__snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post ∧ __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post
6:	__snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post ∧ __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post
7:	__snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post ∧ __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post
9:	__snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post ∧ __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post
10:	__snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post ∧ __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post
13:	__snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post ∧ __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post
18:	__snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post ∧ __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post
19:	__snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post ∧ __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post

5.1.1.1.12 Fresh Variable Addition

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

32:	__snapshot_2_oldX1_0 ≤ oldX1_0 ∧ oldX1_0 ≤ __snapshot_2_oldX1_0
34:	__snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 ∧ __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0
1:	__snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 ∧ __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0
2:	__snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 ∧ __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0
3:	__snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 ∧ __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0
4:	__snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 ∧ __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0
6:	__snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 ∧ __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0
7:	__snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 ∧ __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0
9:	__snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 ∧ __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0
10:	__snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 ∧ __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0
13:	__snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 ∧ __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0
18:	__snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 ∧ __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0
19:	__snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 ∧ __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0

5.1.1.1.13 Fresh Variable Addition

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

32:	__snapshot_2_oldX0_post ≤ oldX0_post ∧ oldX0_post ≤ __snapshot_2_oldX0_post
34:	__snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post ∧ __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post
1:	__snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post ∧ __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post
2:	__snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post ∧ __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post
3:	__snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post ∧ __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post
4:	__snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post ∧ __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post
6:	__snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post ∧ __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post
7:	__snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post ∧ __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post
9:	__snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post ∧ __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post
10:	__snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post ∧ __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post
13:	__snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post ∧ __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post
18:	__snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post ∧ __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post
19:	__snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post ∧ __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post

5.1.1.1.14 Fresh Variable Addition

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

32:	__snapshot_2_oldX0_0 ≤ oldX0_0 ∧ oldX0_0 ≤ __snapshot_2_oldX0_0
34:	__snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 ∧ __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0
1:	__snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 ∧ __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0
2:	__snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 ∧ __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0
3:	__snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 ∧ __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0
4:	__snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 ∧ __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0
6:	__snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 ∧ __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0
7:	__snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 ∧ __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0
9:	__snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 ∧ __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0
10:	__snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 ∧ __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0
13:	__snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 ∧ __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0
18:	__snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 ∧ __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0
19:	__snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 ∧ __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0

5.1.1.1.15 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
0:	− __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0
2:	TRUE ∨ 1 − __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0
3:	− __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0
4:	1 − 2⋅__snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0
6:	− __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0 ∨ 1 ≤ 0
7:	− __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0 ∧ 1 − x1_0 ≤ 0
9:	− __snapshot_2_x1_0 + x1_0 ≤ 0
2_var_snapshot:	− __snapshot_2_x1_0 + x1_0 ≤ 0
2*:	1 − __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0 ∨ 1 − 2⋅__snapshot_2_x1_0 + 2⋅x1_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

nodes (location) invariant:

0	(11)	TRUE
1	(10)	TRUE
2	(0)	TRUE
3	(3)	TRUE
4	(5)	TRUE
5	(1)	TRUE
6	(6)	TRUE
7	(7)	TRUE
8	(8)	TRUE
9	(9)	TRUE
10	(4)	TRUE
11	(2)	TRUE
12	(9)	TRUE
13	(2)	TRUE
14	(2_var_snapshot)	− __snapshot_2_x1_0 + x1_0 ≤ 0
19	(1)	TRUE
20	(2)	TRUE
21	(1)	TRUE
22	(1)	TRUE
23	(1)	TRUE
24	(2)	TRUE
25	(4)	TRUE
26	(4)	TRUE
27	(0)	TRUE
28	(3)	TRUE
29	(3)	TRUE
30	(5)	TRUE
31	(6)	TRUE
32	(6)	TRUE
33	(8)	TRUE
34	(7)	TRUE
35	(8)	TRUE
36	(9)	− __snapshot_2_x1_0 + x1_0 ≤ 0
37	(7)	− __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0 ∧ 1 − x1_0 ≤ 0
38	(6)	− __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0
39	(6)	1 ≤ 0
47	(3)	− __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0
48	(3)	− __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0
49	(4)	1 − 2⋅__snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0
50	(4)	1 − 2⋅__snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0
51	(0)	− __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0
52	(2*)	1 − __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0
53	(2)	1 − __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0
54	(2_var_snapshot)	− __snapshot_2_x1_0 + x1_0 ≤ 0
59	(2*)	1 − 2⋅__snapshot_2_x1_0 + 2⋅x1_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0
60	(1)	TRUE
61	(1)	TRUE

initial node: 0

cover edges:

4	→ 30
5	→ 60
8	→ 35
9	→ 12
19	→ 60
20	→ 11
21	→ 60
22	→ 60
23	→ 60
24	→ 11
25	→ 10
26	→ 10
27	→ 2
28	→ 3
29	→ 3
31	→ 6
32	→ 6
33	→ 35
34	→ 7
47	→ 48
49	→ 50
54	→ 14
59	→ 52
61	→ 60

transition edges:

0	30 1
1	20 2
1	21 3
1	22 4
1	23 5
1	24 6
1	25 7
1	26 8
1	27 9
1	28 10
1	29 11
2	0 19
2	1 20
3	2 25
3	3 26
3	4 27
6	6 28
6	7 29
6	8 30
7	9 31
7	10 32
7	11 33
10	15 21
10	16 22
10	17 23
10	18 24
11	19 12
11	31 13
12	13 34
12	14 35
13	32 14
14	19 36
30	5 61
35	12 60
36	13 37
37	9 38
37	10 39
38	6 47
38	7 48
48	2 49
48	3 50
48	4 51
50	18 59
51	1 52
52	34 53
53	32 54

5.1.1.1.16 Transition Removal

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

0:	__snapshot_2_x1_0
2:	x1_0
3:	__snapshot_2_x1_0
4:	__snapshot_2_x1_0
6:	__snapshot_2_x1_0
7:	__snapshot_2_x1_0
9:	__snapshot_2_x1_0
2_var_snapshot:	__snapshot_2_x1_0
2*:	__snapshot_2_x1_0

5.1.1.1.17 Transition Removal

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

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

5.1.1.1.18 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert

version: 1.0