LTS Termination Proof

by T2Cert

Input

Integer Transition System

Initial Location: 8

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
0	1	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 ∧ 1 − oldX0_post + x0_post ≤ 0 ∧ −1 + 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 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0
0	2	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 ∧ − 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	3	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
3	4	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 ∧ 1 − oldX0_post + x0_post ≤ 0 ∧ −1 + oldX0_post − x0_post ≤ 0 ∧ −1 + x1_post ≤ 0 ∧ 1 − 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 ∧ − 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	5	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 ≤ 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 ∧ − 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	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 ∧ 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 ∧ − 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
5	7	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
6	8	4:	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 ∧ − 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	9	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 ∧ 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 ∧ − 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
2	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 ∧ − 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 ∧ − 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	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 ∧ − 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
7	12	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 ∧ − 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
7	13	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 ∧ − 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
7	14	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 ∧ − 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
7	15	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 ∧ − 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
7	16	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 ∧ − 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
7	17	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 ∧ − 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
8	18	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 ∧ − 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 ∧ − 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, 3, 7, 9, 11, 12, 13, 14, 15, 16, 17, 18 using the following ranking functions, which are bounded by −15.

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

3 Location Addition

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

2* 22 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 ∧ − 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 20 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 ∧ − 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, 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 19.

5.1.1.1.1 Fresh Variable Addition

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

20:	__snapshot_2_x1_post ≤ x1_post ∧ x1_post ≤ __snapshot_2_x1_post
22:	__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
4:	__snapshot_2_x1_post ≤ __snapshot_2_x1_post ∧ __snapshot_2_x1_post ≤ __snapshot_2_x1_post
5:	__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
8:	__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

5.1.1.1.2 Fresh Variable Addition

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

20:	__snapshot_2_x1_0 ≤ x1_0 ∧ x1_0 ≤ __snapshot_2_x1_0
22:	__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
4:	__snapshot_2_x1_0 ≤ __snapshot_2_x1_0 ∧ __snapshot_2_x1_0 ≤ __snapshot_2_x1_0
5:	__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
8:	__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

5.1.1.1.3 Fresh Variable Addition

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

20:	__snapshot_2_x0_post ≤ x0_post ∧ x0_post ≤ __snapshot_2_x0_post
22:	__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
4:	__snapshot_2_x0_post ≤ __snapshot_2_x0_post ∧ __snapshot_2_x0_post ≤ __snapshot_2_x0_post
5:	__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
8:	__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

5.1.1.1.4 Fresh Variable Addition

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

20:	__snapshot_2_x0_0 ≤ x0_0 ∧ x0_0 ≤ __snapshot_2_x0_0
22:	__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
4:	__snapshot_2_x0_0 ≤ __snapshot_2_x0_0 ∧ __snapshot_2_x0_0 ≤ __snapshot_2_x0_0
5:	__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
8:	__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

5.1.1.1.5 Fresh Variable Addition

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

20:	__snapshot_2_oldX3_post ≤ oldX3_post ∧ oldX3_post ≤ __snapshot_2_oldX3_post
22:	__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
4:	__snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post ∧ __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post
5:	__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
8:	__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

5.1.1.1.6 Fresh Variable Addition

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

20:	__snapshot_2_oldX3_0 ≤ oldX3_0 ∧ oldX3_0 ≤ __snapshot_2_oldX3_0
22:	__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
4:	__snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 ∧ __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0
5:	__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
8:	__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

5.1.1.1.7 Fresh Variable Addition

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

20:	__snapshot_2_oldX2_post ≤ oldX2_post ∧ oldX2_post ≤ __snapshot_2_oldX2_post
22:	__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
4:	__snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post ∧ __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post
5:	__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
8:	__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

5.1.1.1.8 Fresh Variable Addition

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

20:	__snapshot_2_oldX2_0 ≤ oldX2_0 ∧ oldX2_0 ≤ __snapshot_2_oldX2_0
22:	__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
4:	__snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 ∧ __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0
5:	__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
8:	__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

5.1.1.1.9 Fresh Variable Addition

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

20:	__snapshot_2_oldX1_post ≤ oldX1_post ∧ oldX1_post ≤ __snapshot_2_oldX1_post
22:	__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
4:	__snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post ∧ __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post
5:	__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
8:	__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

5.1.1.1.10 Fresh Variable Addition

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

20:	__snapshot_2_oldX1_0 ≤ oldX1_0 ∧ oldX1_0 ≤ __snapshot_2_oldX1_0
22:	__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
4:	__snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 ∧ __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0
5:	__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
8:	__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

5.1.1.1.11 Fresh Variable Addition

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

20:	__snapshot_2_oldX0_post ≤ oldX0_post ∧ oldX0_post ≤ __snapshot_2_oldX0_post
22:	__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
4:	__snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post ∧ __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post
5:	__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
8:	__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

5.1.1.1.12 Fresh Variable Addition

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

20:	__snapshot_2_oldX0_0 ≤ oldX0_0 ∧ oldX0_0 ≤ __snapshot_2_oldX0_0
22:	__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
4:	__snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 ∧ __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0
5:	__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
8:	__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

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

The invariants are proved as follows.

IMPACT Invariant Proof

nodes (location) invariant:

0	(8)	TRUE
1	(7)	TRUE
2	(0)	TRUE
3	(3)	TRUE
4	(1)	TRUE
5	(4)	TRUE
6	(5)	TRUE
7	(6)	TRUE
8	(2)	TRUE
9	(6)	TRUE
10	(2)	TRUE
11	(2_var_snapshot)	− __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ − __snapshot_2_x1_0 + x1_0 ≤ 0
16	(1)	TRUE
17	(2)	TRUE
18	(2)	TRUE
19	(1)	TRUE
20	(2)	TRUE
21	(0)	TRUE
22	(3)	TRUE
23	(4)	TRUE
24	(5)	TRUE
25	(6)	− __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ − __snapshot_2_x1_0 + x1_0 ≤ 0
26	(4)	− __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ − __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0
27	(0)	− __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ − __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0
28	(3)	− __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0
29	(2*)	1 − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0
30	(2)	1 − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0
31	(2_var_snapshot)	− __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ − __snapshot_2_x1_0 + x1_0 ≤ 0
36	(1)	TRUE
37	(2*)	1 − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0
38	(2*)	− __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0
43	(2)	− __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0
44	(2_var_snapshot)	− __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ − __snapshot_2_x1_0 + x1_0 ≤ 0

initial node: 0
cover edges:

4 → 36

6 → 24

9 → 7

16 → 36

17 → 8

18 → 8

19 → 36

20 → 8

21 → 2

22 → 3

23 → 5

31 → 11

37 → 29

44 → 11

transition edges:

0	18 1
1	11 2
1	12 3
1	13 4
1	14 5
1	15 6
1	16 7
1	17 8
2	0 16
2	1 17
2	2 18
3	3 19
3	4 20
5	5 21
5	6 22
7	8 23
7	9 24
8	10 9
8	19 10
10	20 11
11	10 25
24	7 36
25	8 26
26	5 27
26	6 28
27	1 37
27	2 38
28	4 29
29	22 30
30	20 31
38	22 43
43	20 44

5.1.1.1.14 Transition Removal

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

0:	[__snapshot_2_x0_0, __snapshot_2_x1_0]
2:	[x0_0, x1_0]
3:	[__snapshot_2_x0_0, __snapshot_2_x1_0]
4:	[__snapshot_2_x0_0, __snapshot_2_x1_0]
6:	[__snapshot_2_x0_0, __snapshot_2_x1_0]
2_var_snapshot:	[__snapshot_2_x0_0, __snapshot_2_x1_0]
2*:	[__snapshot_2_x0_0, __snapshot_2_x1_0]

5.1.1.1.15 Transition Removal

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

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

5.1.1.1.16 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert

version: 1.0

4	→ 36
6	→ 24
9	→ 7
16	→ 36
17	→ 8
18	→ 8
19	→ 36
20	→ 8
21	→ 2
22	→ 3
23	→ 5
31	→ 11
37	→ 29
44	→ 11