LTS Termination Proof

by T2Cert

Input

Integer Transition System

Initial Location: 3

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 ∧ 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 ∧ 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 ∧ 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − m_0 ≤ 0 ∧ − c1_1 ≤ 0 ∧ −1 + c1_1 ≤ 0 ∧ z_0 ≤ 0 ∧ 1 − pos_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ 1 − c1_1 ≤ 0 ∧ −1 − wpos_0 + wpos_1 ≤ 0 ∧ 1 + wpos_0 − wpos_1 ≤ 0 ∧ 1 − c1_1 ≤ 0 ∧ − c2_1 ≤ 0 ∧ −1 + c2_1 ≤ 0 ∧ z_0 ≤ 0 ∧ 1 − pos_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − wpos_1 ≤ 0 ∧ −1 + wpos_1 ≤ 0 ∧ 1 − pi_0 ≤ 0 ∧ c2_1 ≤ 0 ∧ wpos_2 ≤ 0 ∧ − wpos_2 ≤ 0 ∧ 1 − pi_0 + pi_1 ≤ 0 ∧ −1 + pi_0 − pi_1 ≤ 0 ∧ c2_1 ≤ 0 ∧ 1 − m_0 + m_1 ≤ 0 ∧ −1 + m_0 − m_1 ≤ 0 ∧ 1 − m_1 ≤ 0 ∧ − c1_2 ≤ 0 ∧ −1 + c1_2 ≤ 0 ∧ z_0 ≤ 0 ∧ 1 − pos_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ wpos_2 ≤ 0 ∧ 1 − c1_2 ≤ 0 ∧ −1 − wpos_2 + wpos_3 ≤ 0 ∧ 1 + wpos_2 − wpos_3 ≤ 0 ∧ 1 − c1_2 ≤ 0 ∧ − c2_2 ≤ 0 ∧ −1 + c2_2 ≤ 0 ∧ z_0 ≤ 0 ∧ 1 − pos_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − wpos_3 ≤ 0 ∧ −1 + wpos_3 ≤ 0 ∧ pi_1 ≤ 0 ∧ −1 − seq_0 + seq_post ≤ 0 ∧ 1 + seq_0 − seq_post ≤ 0 ∧ wpos_4 ≤ 0 ∧ − wpos_4 ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ pi_2 − seq_post ≤ 0 ∧ − pi_2 + seq_post ≤ 0 ∧ − z_1 ≤ 0 ∧ 1 − c2_2 ≤ 0 ∧ 1 + m_1 − max_0 ≤ 0 ∧ −1 − m_1 + m_2 ≤ 0 ∧ 1 + m_1 − m_2 ≤ 0 ∧ 1 − m_2 ≤ 0 ∧ − c1_3 ≤ 0 ∧ −1 + c1_3 ≤ 0 ∧ 1 − z_1 ≤ 0 ∧ 1 − z_1 + z_2 ≤ 0 ∧ −1 + z_1 − z_2 ≤ 0 ∧ 1 − c1_3 ≤ 0 ∧ − c2_3 ≤ 0 ∧ −1 + c2_3 ≤ 0 ∧ 1 − z_2 ≤ 0 ∧ 1 − z_2 + z_post ≤ 0 ∧ −1 + z_2 − z_post ≤ 0 ∧ 1 − c2_3 ≤ 0 ∧ 1 + m_2 − max_0 ≤ 0 ∧ −1 − m_2 + m_3 ≤ 0 ∧ 1 + m_2 − m_3 ≤ 0 ∧ 1 − m_3 ≤ 0 ∧ − c1_4 ≤ 0 ∧ −1 + c1_4 ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ c1_4 ≤ 0 ∧ −1 − pos_1 + pos_post ≤ 0 ∧ 1 + pos_1 − pos_post ≤ 0 ∧ c1_4 ≤ 0 ∧ 1 − m_3 ≤ 0 ∧ − c1_post ≤ 0 ∧ −1 + c1_post ≤ 0 ∧ z_post ≤ 0 ∧ 1 − pos_post ≤ 0 ∧ −1 + pos_post ≤ 0 ∧ wpos_4 ≤ 0 ∧ 1 − c1_post ≤ 0 ∧ −1 − wpos_4 + wpos_5 ≤ 0 ∧ 1 + wpos_4 − wpos_5 ≤ 0 ∧ 1 − c1_post ≤ 0 ∧ − c2_post ≤ 0 ∧ −1 + c2_post ≤ 0 ∧ z_post ≤ 0 ∧ 1 − pos_post ≤ 0 ∧ −1 + pos_post ≤ 0 ∧ 1 − wpos_5 ≤ 0 ∧ −1 + wpos_5 ≤ 0 ∧ 1 − pi_2 ≤ 0 ∧ c2_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ 1 − pi_2 + pi_post ≤ 0 ∧ −1 + pi_2 − pi_post ≤ 0 ∧ c2_post ≤ 0 ∧ 1 − m_3 + m_post ≤ 0 ∧ −1 + m_3 − m_post ≤ 0 ∧ c1_0 − c1_post ≤ 0 ∧ − c1_0 + c1_post ≤ 0 ∧ c2_0 − c2_post ≤ 0 ∧ − c2_0 + c2_post ≤ 0 ∧ m_0 − m_post ≤ 0 ∧ − m_0 + m_post ≤ 0 ∧ pi_0 − pi_post ≤ 0 ∧ − pi_0 + pi_post ≤ 0 ∧ pos_0 − pos_post ≤ 0 ∧ − pos_0 + pos_post ≤ 0 ∧ seq_0 − seq_post ≤ 0 ∧ − seq_0 + seq_post ≤ 0 ∧ wpos_0 − wpos_post ≤ 0 ∧ − wpos_0 + wpos_post ≤ 0 ∧ z_0 − z_post ≤ 0 ∧ − z_0 + z_post ≤ 0 ∧ − n_post + n_post ≤ 0 ∧ n_post − n_post ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − max_post + max_post ≤ 0 ∧ max_post − max_post ≤ 0 ∧ − max_0 + max_0 ≤ 0 ∧ max_0 − max_0 ≤ 0
1	1	0:	− z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_2 + z_2 ≤ 0 ∧ z_2 − z_2 ≤ 0 ∧ − z_1 + z_1 ≤ 0 ∧ z_1 − z_1 ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − wpos_post + wpos_post ≤ 0 ∧ wpos_post − wpos_post ≤ 0 ∧ − wpos_5 + wpos_5 ≤ 0 ∧ wpos_5 − wpos_5 ≤ 0 ∧ − wpos_4 + wpos_4 ≤ 0 ∧ wpos_4 − wpos_4 ≤ 0 ∧ − wpos_3 + wpos_3 ≤ 0 ∧ wpos_3 − wpos_3 ≤ 0 ∧ − wpos_2 + wpos_2 ≤ 0 ∧ wpos_2 − wpos_2 ≤ 0 ∧ − wpos_1 + wpos_1 ≤ 0 ∧ wpos_1 − wpos_1 ≤ 0 ∧ − wpos_0 + wpos_0 ≤ 0 ∧ wpos_0 − wpos_0 ≤ 0 ∧ − seq_post + seq_post ≤ 0 ∧ seq_post − seq_post ≤ 0 ∧ − seq_0 + seq_0 ≤ 0 ∧ seq_0 − seq_0 ≤ 0 ∧ − pos_post + pos_post ≤ 0 ∧ pos_post − pos_post ≤ 0 ∧ − pos_1 + pos_1 ≤ 0 ∧ pos_1 − pos_1 ≤ 0 ∧ − pos_0 + pos_0 ≤ 0 ∧ pos_0 − pos_0 ≤ 0 ∧ − pi_post + pi_post ≤ 0 ∧ pi_post − pi_post ≤ 0 ∧ − pi_2 + pi_2 ≤ 0 ∧ pi_2 − pi_2 ≤ 0 ∧ − pi_1 + pi_1 ≤ 0 ∧ pi_1 − pi_1 ≤ 0 ∧ − pi_0 + pi_0 ≤ 0 ∧ pi_0 − pi_0 ≤ 0 ∧ − n_post + n_post ≤ 0 ∧ n_post − n_post ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − max_post + max_post ≤ 0 ∧ max_post − max_post ≤ 0 ∧ − max_0 + max_0 ≤ 0 ∧ max_0 − max_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_3 + m_3 ≤ 0 ∧ m_3 − m_3 ≤ 0 ∧ − m_2 + m_2 ≤ 0 ∧ m_2 − m_2 ≤ 0 ∧ − m_1 + m_1 ≤ 0 ∧ m_1 − m_1 ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − c2_post + c2_post ≤ 0 ∧ c2_post − c2_post ≤ 0 ∧ − c2_3 + c2_3 ≤ 0 ∧ c2_3 − c2_3 ≤ 0 ∧ − c2_2 + c2_2 ≤ 0 ∧ c2_2 − c2_2 ≤ 0 ∧ − c2_1 + c2_1 ≤ 0 ∧ c2_1 − c2_1 ≤ 0 ∧ − c2_0 + c2_0 ≤ 0 ∧ c2_0 − c2_0 ≤ 0 ∧ − c1_post + c1_post ≤ 0 ∧ c1_post − c1_post ≤ 0 ∧ − c1_4 + c1_4 ≤ 0 ∧ c1_4 − c1_4 ≤ 0 ∧ − c1_3 + c1_3 ≤ 0 ∧ c1_3 − c1_3 ≤ 0 ∧ − c1_2 + c1_2 ≤ 0 ∧ c1_2 − c1_2 ≤ 0 ∧ − c1_1 + c1_1 ≤ 0 ∧ c1_1 − c1_1 ≤ 0 ∧ − c1_0 + c1_0 ≤ 0 ∧ c1_0 − c1_0 ≤ 0
2	2	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 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 + seq_post ≤ 0 ∧ 1 − seq_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ pi_post − seq_post ≤ 0 ∧ − pi_post + seq_post ≤ 0 ∧ − z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ − n_post ≤ 0 ∧ − max_post ≤ 0 ∧ max_post − n_post ≤ 0 ∧ m_post − max_post ≤ 0 ∧ − m_post ≤ 0 ∧ 1 − m_post ≤ 0 ∧ − c1_post ≤ 0 ∧ −1 + c1_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ c1_post ≤ 0 ∧ −1 − pos_1 + pos_post ≤ 0 ∧ 1 + pos_1 − pos_post ≤ 0 ∧ c1_post ≤ 0 ∧ c1_0 − c1_post ≤ 0 ∧ − c1_0 + c1_post ≤ 0 ∧ m_0 − m_post ≤ 0 ∧ − m_0 + m_post ≤ 0 ∧ max_0 − max_post ≤ 0 ∧ − max_0 + max_post ≤ 0 ∧ n_0 − n_post ≤ 0 ∧ − n_0 + n_post ≤ 0 ∧ pi_0 − pi_post ≤ 0 ∧ − pi_0 + pi_post ≤ 0 ∧ pos_0 − pos_post ≤ 0 ∧ − pos_0 + pos_post ≤ 0 ∧ seq_0 − seq_post ≤ 0 ∧ − seq_0 + seq_post ≤ 0 ∧ wpos_0 − wpos_post ≤ 0 ∧ − wpos_0 + wpos_post ≤ 0 ∧ z_0 − z_post ≤ 0 ∧ − z_0 + z_post ≤ 0 ∧ − z_2 + z_2 ≤ 0 ∧ z_2 − z_2 ≤ 0 ∧ − z_1 + z_1 ≤ 0 ∧ z_1 − z_1 ≤ 0 ∧ − wpos_5 + wpos_5 ≤ 0 ∧ wpos_5 − wpos_5 ≤ 0 ∧ − wpos_4 + wpos_4 ≤ 0 ∧ wpos_4 − wpos_4 ≤ 0 ∧ − wpos_3 + wpos_3 ≤ 0 ∧ wpos_3 − wpos_3 ≤ 0 ∧ − wpos_2 + wpos_2 ≤ 0 ∧ wpos_2 − wpos_2 ≤ 0 ∧ − wpos_1 + wpos_1 ≤ 0 ∧ wpos_1 − wpos_1 ≤ 0 ∧ − pi_2 + pi_2 ≤ 0 ∧ pi_2 − pi_2 ≤ 0 ∧ − pi_1 + pi_1 ≤ 0 ∧ pi_1 − pi_1 ≤ 0 ∧ − m_3 + m_3 ≤ 0 ∧ m_3 − m_3 ≤ 0 ∧ − m_2 + m_2 ≤ 0 ∧ m_2 − m_2 ≤ 0 ∧ − m_1 + m_1 ≤ 0 ∧ m_1 − m_1 ≤ 0 ∧ − c2_post + c2_post ≤ 0 ∧ c2_post − c2_post ≤ 0 ∧ − c2_3 + c2_3 ≤ 0 ∧ c2_3 − c2_3 ≤ 0 ∧ − c2_2 + c2_2 ≤ 0 ∧ c2_2 − c2_2 ≤ 0 ∧ − c2_1 + c2_1 ≤ 0 ∧ c2_1 − c2_1 ≤ 0 ∧ − c2_0 + c2_0 ≤ 0 ∧ c2_0 − c2_0 ≤ 0 ∧ − c1_4 + c1_4 ≤ 0 ∧ c1_4 − c1_4 ≤ 0 ∧ − c1_3 + c1_3 ≤ 0 ∧ c1_3 − c1_3 ≤ 0 ∧ − c1_2 + c1_2 ≤ 0 ∧ c1_2 − c1_2 ≤ 0 ∧ − c1_1 + c1_1 ≤ 0 ∧ c1_1 − c1_1 ≤ 0
3	3	2:	− z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_2 + z_2 ≤ 0 ∧ z_2 − z_2 ≤ 0 ∧ − z_1 + z_1 ≤ 0 ∧ z_1 − z_1 ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − wpos_post + wpos_post ≤ 0 ∧ wpos_post − wpos_post ≤ 0 ∧ − wpos_5 + wpos_5 ≤ 0 ∧ wpos_5 − wpos_5 ≤ 0 ∧ − wpos_4 + wpos_4 ≤ 0 ∧ wpos_4 − wpos_4 ≤ 0 ∧ − wpos_3 + wpos_3 ≤ 0 ∧ wpos_3 − wpos_3 ≤ 0 ∧ − wpos_2 + wpos_2 ≤ 0 ∧ wpos_2 − wpos_2 ≤ 0 ∧ − wpos_1 + wpos_1 ≤ 0 ∧ wpos_1 − wpos_1 ≤ 0 ∧ − wpos_0 + wpos_0 ≤ 0 ∧ wpos_0 − wpos_0 ≤ 0 ∧ − seq_post + seq_post ≤ 0 ∧ seq_post − seq_post ≤ 0 ∧ − seq_0 + seq_0 ≤ 0 ∧ seq_0 − seq_0 ≤ 0 ∧ − pos_post + pos_post ≤ 0 ∧ pos_post − pos_post ≤ 0 ∧ − pos_1 + pos_1 ≤ 0 ∧ pos_1 − pos_1 ≤ 0 ∧ − pos_0 + pos_0 ≤ 0 ∧ pos_0 − pos_0 ≤ 0 ∧ − pi_post + pi_post ≤ 0 ∧ pi_post − pi_post ≤ 0 ∧ − pi_2 + pi_2 ≤ 0 ∧ pi_2 − pi_2 ≤ 0 ∧ − pi_1 + pi_1 ≤ 0 ∧ pi_1 − pi_1 ≤ 0 ∧ − pi_0 + pi_0 ≤ 0 ∧ pi_0 − pi_0 ≤ 0 ∧ − n_post + n_post ≤ 0 ∧ n_post − n_post ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − max_post + max_post ≤ 0 ∧ max_post − max_post ≤ 0 ∧ − max_0 + max_0 ≤ 0 ∧ max_0 − max_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_3 + m_3 ≤ 0 ∧ m_3 − m_3 ≤ 0 ∧ − m_2 + m_2 ≤ 0 ∧ m_2 − m_2 ≤ 0 ∧ − m_1 + m_1 ≤ 0 ∧ m_1 − m_1 ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − c2_post + c2_post ≤ 0 ∧ c2_post − c2_post ≤ 0 ∧ − c2_3 + c2_3 ≤ 0 ∧ c2_3 − c2_3 ≤ 0 ∧ − c2_2 + c2_2 ≤ 0 ∧ c2_2 − c2_2 ≤ 0 ∧ − c2_1 + c2_1 ≤ 0 ∧ c2_1 − c2_1 ≤ 0 ∧ − c2_0 + c2_0 ≤ 0 ∧ c2_0 − c2_0 ≤ 0 ∧ − c1_post + c1_post ≤ 0 ∧ c1_post − c1_post ≤ 0 ∧ − c1_4 + c1_4 ≤ 0 ∧ c1_4 − c1_4 ≤ 0 ∧ − c1_3 + c1_3 ≤ 0 ∧ c1_3 − c1_3 ≤ 0 ∧ − c1_2 + c1_2 ≤ 0 ∧ c1_2 − c1_2 ≤ 0 ∧ − c1_1 + c1_1 ≤ 0 ∧ c1_1 − c1_1 ≤ 0 ∧ − c1_0 + c1_0 ≤ 0 ∧ c1_0 − c1_0 ≤ 0

Proof

1 Invariant Updates

The following invariants are asserted.

0:	− c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0
1:	−1 + c1_post ≤ 0 ∧ 1 − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ −1 + pos_post ≤ 0 ∧ 1 − pos_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ −1 + c1_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − pos_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0 ∧ c2_post ≤ 0 ∧ − c2_post ≤ 0 ∧ −1 + c1_1 ≤ 0 ∧ 1 − c1_1 ≤ 0 ∧ −1 + c1_2 ≤ 0 ∧ 1 − c1_2 ≤ 0 ∧ −1 + c1_3 ≤ 0 ∧ 1 − c1_3 ≤ 0 ∧ c1_4 ≤ 0 ∧ − c1_4 ≤ 0 ∧ c2_1 ≤ 0 ∧ − c2_1 ≤ 0 ∧ −1 + c2_2 ≤ 0 ∧ 1 − c2_2 ≤ 0 ∧ −1 + c2_3 ≤ 0 ∧ 1 − c2_3 ≤ 0 ∧ 1 − m_1 ≤ 0 ∧ 1 − m_2 ≤ 0 ∧ 1 − m_3 ≤ 0 ∧ pi_1 ≤ 0 ∧ 1 − pi_2 ≤ 0 ∧ −1 + wpos_1 ≤ 0 ∧ 1 − wpos_1 ≤ 0 ∧ wpos_2 ≤ 0 ∧ − wpos_2 ≤ 0 ∧ −1 + wpos_3 ≤ 0 ∧ 1 − wpos_3 ≤ 0 ∧ wpos_4 ≤ 0 ∧ − wpos_4 ≤ 0 ∧ −1 + wpos_5 ≤ 0 ∧ 1 − wpos_5 ≤ 0 ∧ 1 − z_1 ≤ 0 ∧ 1 − z_2 ≤ 0 ∧ c2_0 ≤ 0 ∧ − c2_0 ≤ 0
2:	TRUE
3:	TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

nodes (location) invariant:

0	(0)	− c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0
1	(1)	−1 + c1_post ≤ 0 ∧ 1 − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ −1 + pos_post ≤ 0 ∧ 1 − pos_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ −1 + c1_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − pos_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0 ∧ c2_post ≤ 0 ∧ − c2_post ≤ 0 ∧ −1 + c1_1 ≤ 0 ∧ 1 − c1_1 ≤ 0 ∧ −1 + c1_2 ≤ 0 ∧ 1 − c1_2 ≤ 0 ∧ −1 + c1_3 ≤ 0 ∧ 1 − c1_3 ≤ 0 ∧ c1_4 ≤ 0 ∧ − c1_4 ≤ 0 ∧ c2_1 ≤ 0 ∧ − c2_1 ≤ 0 ∧ −1 + c2_2 ≤ 0 ∧ 1 − c2_2 ≤ 0 ∧ −1 + c2_3 ≤ 0 ∧ 1 − c2_3 ≤ 0 ∧ 1 − m_1 ≤ 0 ∧ 1 − m_2 ≤ 0 ∧ 1 − m_3 ≤ 0 ∧ pi_1 ≤ 0 ∧ 1 − pi_2 ≤ 0 ∧ −1 + wpos_1 ≤ 0 ∧ 1 − wpos_1 ≤ 0 ∧ wpos_2 ≤ 0 ∧ − wpos_2 ≤ 0 ∧ −1 + wpos_3 ≤ 0 ∧ 1 − wpos_3 ≤ 0 ∧ wpos_4 ≤ 0 ∧ − wpos_4 ≤ 0 ∧ −1 + wpos_5 ≤ 0 ∧ 1 − wpos_5 ≤ 0 ∧ 1 − z_1 ≤ 0 ∧ 1 − z_2 ≤ 0 ∧ c2_0 ≤ 0 ∧ − c2_0 ≤ 0
2	(2)	TRUE
3	(3)	TRUE

initial node: 3
cover edges:
transition edges:

0 0 1

1 1 0

2 2 0

3 3 2

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:

− z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_2 + z_2 ≤ 0 ∧ z_2 − z_2 ≤ 0 ∧ − z_1 + z_1 ≤ 0 ∧ z_1 − z_1 ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − wpos_post + wpos_post ≤ 0 ∧ wpos_post − wpos_post ≤ 0 ∧ − wpos_5 + wpos_5 ≤ 0 ∧ wpos_5 − wpos_5 ≤ 0 ∧ − wpos_4 + wpos_4 ≤ 0 ∧ wpos_4 − wpos_4 ≤ 0 ∧ − wpos_3 + wpos_3 ≤ 0 ∧ wpos_3 − wpos_3 ≤ 0 ∧ − wpos_2 + wpos_2 ≤ 0 ∧ wpos_2 − wpos_2 ≤ 0 ∧ − wpos_1 + wpos_1 ≤ 0 ∧ wpos_1 − wpos_1 ≤ 0 ∧ − wpos_0 + wpos_0 ≤ 0 ∧ wpos_0 − wpos_0 ≤ 0 ∧ − seq_post + seq_post ≤ 0 ∧ seq_post − seq_post ≤ 0 ∧ − seq_0 + seq_0 ≤ 0 ∧ seq_0 − seq_0 ≤ 0 ∧ − pos_post + pos_post ≤ 0 ∧ pos_post − pos_post ≤ 0 ∧ − pos_1 + pos_1 ≤ 0 ∧ pos_1 − pos_1 ≤ 0 ∧ − pos_0 + pos_0 ≤ 0 ∧ pos_0 − pos_0 ≤ 0 ∧ − pi_post + pi_post ≤ 0 ∧ pi_post − pi_post ≤ 0 ∧ − pi_2 + pi_2 ≤ 0 ∧ pi_2 − pi_2 ≤ 0 ∧ − pi_1 + pi_1 ≤ 0 ∧ pi_1 − pi_1 ≤ 0 ∧ − pi_0 + pi_0 ≤ 0 ∧ pi_0 − pi_0 ≤ 0 ∧ − n_post + n_post ≤ 0 ∧ n_post − n_post ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − max_post + max_post ≤ 0 ∧ max_post − max_post ≤ 0 ∧ − max_0 + max_0 ≤ 0 ∧ max_0 − max_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_3 + m_3 ≤ 0 ∧ m_3 − m_3 ≤ 0 ∧ − m_2 + m_2 ≤ 0 ∧ m_2 − m_2 ≤ 0 ∧ − m_1 + m_1 ≤ 0 ∧ m_1 − m_1 ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − c2_post + c2_post ≤ 0 ∧ c2_post − c2_post ≤ 0 ∧ − c2_3 + c2_3 ≤ 0 ∧ c2_3 − c2_3 ≤ 0 ∧ − c2_2 + c2_2 ≤ 0 ∧ c2_2 − c2_2 ≤ 0 ∧ − c2_1 + c2_1 ≤ 0 ∧ c2_1 − c2_1 ≤ 0 ∧ − c2_0 + c2_0 ≤ 0 ∧ c2_0 − c2_0 ≤ 0 ∧ − c1_post + c1_post ≤ 0 ∧ c1_post − c1_post ≤ 0 ∧ − c1_4 + c1_4 ≤ 0 ∧ c1_4 − c1_4 ≤ 0 ∧ − c1_3 + c1_3 ≤ 0 ∧ c1_3 − c1_3 ≤ 0 ∧ − c1_2 + c1_2 ≤ 0 ∧ c1_2 − c1_2 ≤ 0 ∧ − c1_1 + c1_1 ≤ 0 ∧ c1_1 − c1_1 ≤ 0 ∧ − c1_0 + c1_0 ≤ 0 ∧ c1_0 − c1_0 ≤ 0

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

3 Transition Removal

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

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

4 Location Addition

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

0* 7 0: − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_2 + z_2 ≤ 0 ∧ z_2 − z_2 ≤ 0 ∧ − z_1 + z_1 ≤ 0 ∧ z_1 − z_1 ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − wpos_post + wpos_post ≤ 0 ∧ wpos_post − wpos_post ≤ 0 ∧ − wpos_5 + wpos_5 ≤ 0 ∧ wpos_5 − wpos_5 ≤ 0 ∧ − wpos_4 + wpos_4 ≤ 0 ∧ wpos_4 − wpos_4 ≤ 0 ∧ − wpos_3 + wpos_3 ≤ 0 ∧ wpos_3 − wpos_3 ≤ 0 ∧ − wpos_2 + wpos_2 ≤ 0 ∧ wpos_2 − wpos_2 ≤ 0 ∧ − wpos_1 + wpos_1 ≤ 0 ∧ wpos_1 − wpos_1 ≤ 0 ∧ − wpos_0 + wpos_0 ≤ 0 ∧ wpos_0 − wpos_0 ≤ 0 ∧ − seq_post + seq_post ≤ 0 ∧ seq_post − seq_post ≤ 0 ∧ − seq_0 + seq_0 ≤ 0 ∧ seq_0 − seq_0 ≤ 0 ∧ − pos_post + pos_post ≤ 0 ∧ pos_post − pos_post ≤ 0 ∧ − pos_1 + pos_1 ≤ 0 ∧ pos_1 − pos_1 ≤ 0 ∧ − pos_0 + pos_0 ≤ 0 ∧ pos_0 − pos_0 ≤ 0 ∧ − pi_post + pi_post ≤ 0 ∧ pi_post − pi_post ≤ 0 ∧ − pi_2 + pi_2 ≤ 0 ∧ pi_2 − pi_2 ≤ 0 ∧ − pi_1 + pi_1 ≤ 0 ∧ pi_1 − pi_1 ≤ 0 ∧ − pi_0 + pi_0 ≤ 0 ∧ pi_0 − pi_0 ≤ 0 ∧ − n_post + n_post ≤ 0 ∧ n_post − n_post ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − max_post + max_post ≤ 0 ∧ max_post − max_post ≤ 0 ∧ − max_0 + max_0 ≤ 0 ∧ max_0 − max_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_3 + m_3 ≤ 0 ∧ m_3 − m_3 ≤ 0 ∧ − m_2 + m_2 ≤ 0 ∧ m_2 − m_2 ≤ 0 ∧ − m_1 + m_1 ≤ 0 ∧ m_1 − m_1 ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − c2_post + c2_post ≤ 0 ∧ c2_post − c2_post ≤ 0 ∧ − c2_3 + c2_3 ≤ 0 ∧ c2_3 − c2_3 ≤ 0 ∧ − c2_2 + c2_2 ≤ 0 ∧ c2_2 − c2_2 ≤ 0 ∧ − c2_1 + c2_1 ≤ 0 ∧ c2_1 − c2_1 ≤ 0 ∧ − c2_0 + c2_0 ≤ 0 ∧ c2_0 − c2_0 ≤ 0 ∧ − c1_post + c1_post ≤ 0 ∧ c1_post − c1_post ≤ 0 ∧ − c1_4 + c1_4 ≤ 0 ∧ c1_4 − c1_4 ≤ 0 ∧ − c1_3 + c1_3 ≤ 0 ∧ c1_3 − c1_3 ≤ 0 ∧ − c1_2 + c1_2 ≤ 0 ∧ c1_2 − c1_2 ≤ 0 ∧ − c1_1 + c1_1 ≤ 0 ∧ c1_1 − c1_1 ≤ 0 ∧ − c1_0 + c1_0 ≤ 0 ∧ c1_0 − c1_0 ≤ 0

5 Location Addition

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

0 5 0_var_snapshot: − z_post + z_post ≤ 0 ∧ z_post − z_post ≤ 0 ∧ − z_2 + z_2 ≤ 0 ∧ z_2 − z_2 ≤ 0 ∧ − z_1 + z_1 ≤ 0 ∧ z_1 − z_1 ≤ 0 ∧ − z_0 + z_0 ≤ 0 ∧ z_0 − z_0 ≤ 0 ∧ − wpos_post + wpos_post ≤ 0 ∧ wpos_post − wpos_post ≤ 0 ∧ − wpos_5 + wpos_5 ≤ 0 ∧ wpos_5 − wpos_5 ≤ 0 ∧ − wpos_4 + wpos_4 ≤ 0 ∧ wpos_4 − wpos_4 ≤ 0 ∧ − wpos_3 + wpos_3 ≤ 0 ∧ wpos_3 − wpos_3 ≤ 0 ∧ − wpos_2 + wpos_2 ≤ 0 ∧ wpos_2 − wpos_2 ≤ 0 ∧ − wpos_1 + wpos_1 ≤ 0 ∧ wpos_1 − wpos_1 ≤ 0 ∧ − wpos_0 + wpos_0 ≤ 0 ∧ wpos_0 − wpos_0 ≤ 0 ∧ − seq_post + seq_post ≤ 0 ∧ seq_post − seq_post ≤ 0 ∧ − seq_0 + seq_0 ≤ 0 ∧ seq_0 − seq_0 ≤ 0 ∧ − pos_post + pos_post ≤ 0 ∧ pos_post − pos_post ≤ 0 ∧ − pos_1 + pos_1 ≤ 0 ∧ pos_1 − pos_1 ≤ 0 ∧ − pos_0 + pos_0 ≤ 0 ∧ pos_0 − pos_0 ≤ 0 ∧ − pi_post + pi_post ≤ 0 ∧ pi_post − pi_post ≤ 0 ∧ − pi_2 + pi_2 ≤ 0 ∧ pi_2 − pi_2 ≤ 0 ∧ − pi_1 + pi_1 ≤ 0 ∧ pi_1 − pi_1 ≤ 0 ∧ − pi_0 + pi_0 ≤ 0 ∧ pi_0 − pi_0 ≤ 0 ∧ − n_post + n_post ≤ 0 ∧ n_post − n_post ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − max_post + max_post ≤ 0 ∧ max_post − max_post ≤ 0 ∧ − max_0 + max_0 ≤ 0 ∧ max_0 − max_0 ≤ 0 ∧ − m_post + m_post ≤ 0 ∧ m_post − m_post ≤ 0 ∧ − m_3 + m_3 ≤ 0 ∧ m_3 − m_3 ≤ 0 ∧ − m_2 + m_2 ≤ 0 ∧ m_2 − m_2 ≤ 0 ∧ − m_1 + m_1 ≤ 0 ∧ m_1 − m_1 ≤ 0 ∧ − m_0 + m_0 ≤ 0 ∧ m_0 − m_0 ≤ 0 ∧ − c2_post + c2_post ≤ 0 ∧ c2_post − c2_post ≤ 0 ∧ − c2_3 + c2_3 ≤ 0 ∧ c2_3 − c2_3 ≤ 0 ∧ − c2_2 + c2_2 ≤ 0 ∧ c2_2 − c2_2 ≤ 0 ∧ − c2_1 + c2_1 ≤ 0 ∧ c2_1 − c2_1 ≤ 0 ∧ − c2_0 + c2_0 ≤ 0 ∧ c2_0 − c2_0 ≤ 0 ∧ − c1_post + c1_post ≤ 0 ∧ c1_post − c1_post ≤ 0 ∧ − c1_4 + c1_4 ≤ 0 ∧ c1_4 − c1_4 ≤ 0 ∧ − c1_3 + c1_3 ≤ 0 ∧ c1_3 − c1_3 ≤ 0 ∧ − c1_2 + c1_2 ≤ 0 ∧ c1_2 − c1_2 ≤ 0 ∧ − c1_1 + c1_1 ≤ 0 ∧ c1_1 − c1_1 ≤ 0 ∧ − c1_0 + c1_0 ≤ 0 ∧ c1_0 − c1_0 ≤ 0

6 SCC Decomposition

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

6.1 SCC Subproblem 1/1

Here we consider the SCC { 0, 1, 0_var_snapshot, 0* }.

6.1.1 Splitting Cut-Point Transitions

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

6.1.1.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 4.

6.1.1.1.1 Fresh Variable Addition

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

5:	__snapshot_0_z_post ≤ z_post ∧ z_post ≤ __snapshot_0_z_post
7:	__snapshot_0_z_post ≤ __snapshot_0_z_post ∧ __snapshot_0_z_post ≤ __snapshot_0_z_post
0:	__snapshot_0_z_post ≤ __snapshot_0_z_post ∧ __snapshot_0_z_post ≤ __snapshot_0_z_post
1:	__snapshot_0_z_post ≤ __snapshot_0_z_post ∧ __snapshot_0_z_post ≤ __snapshot_0_z_post

6.1.1.1.2 Fresh Variable Addition

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

5:	__snapshot_0_z_2 ≤ z_2 ∧ z_2 ≤ __snapshot_0_z_2
7:	__snapshot_0_z_2 ≤ __snapshot_0_z_2 ∧ __snapshot_0_z_2 ≤ __snapshot_0_z_2
0:	__snapshot_0_z_2 ≤ __snapshot_0_z_2 ∧ __snapshot_0_z_2 ≤ __snapshot_0_z_2
1:	__snapshot_0_z_2 ≤ __snapshot_0_z_2 ∧ __snapshot_0_z_2 ≤ __snapshot_0_z_2

6.1.1.1.3 Fresh Variable Addition

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

5:	__snapshot_0_z_1 ≤ z_1 ∧ z_1 ≤ __snapshot_0_z_1
7:	__snapshot_0_z_1 ≤ __snapshot_0_z_1 ∧ __snapshot_0_z_1 ≤ __snapshot_0_z_1
0:	__snapshot_0_z_1 ≤ __snapshot_0_z_1 ∧ __snapshot_0_z_1 ≤ __snapshot_0_z_1
1:	__snapshot_0_z_1 ≤ __snapshot_0_z_1 ∧ __snapshot_0_z_1 ≤ __snapshot_0_z_1

6.1.1.1.4 Fresh Variable Addition

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

5:	__snapshot_0_z_0 ≤ z_0 ∧ z_0 ≤ __snapshot_0_z_0
7:	__snapshot_0_z_0 ≤ __snapshot_0_z_0 ∧ __snapshot_0_z_0 ≤ __snapshot_0_z_0
0:	__snapshot_0_z_0 ≤ __snapshot_0_z_0 ∧ __snapshot_0_z_0 ≤ __snapshot_0_z_0
1:	__snapshot_0_z_0 ≤ __snapshot_0_z_0 ∧ __snapshot_0_z_0 ≤ __snapshot_0_z_0

6.1.1.1.5 Fresh Variable Addition

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

5:	__snapshot_0_wpos_post ≤ wpos_post ∧ wpos_post ≤ __snapshot_0_wpos_post
7:	__snapshot_0_wpos_post ≤ __snapshot_0_wpos_post ∧ __snapshot_0_wpos_post ≤ __snapshot_0_wpos_post
0:	__snapshot_0_wpos_post ≤ __snapshot_0_wpos_post ∧ __snapshot_0_wpos_post ≤ __snapshot_0_wpos_post
1:	__snapshot_0_wpos_post ≤ __snapshot_0_wpos_post ∧ __snapshot_0_wpos_post ≤ __snapshot_0_wpos_post

6.1.1.1.6 Fresh Variable Addition

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

5:	__snapshot_0_wpos_5 ≤ wpos_5 ∧ wpos_5 ≤ __snapshot_0_wpos_5
7:	__snapshot_0_wpos_5 ≤ __snapshot_0_wpos_5 ∧ __snapshot_0_wpos_5 ≤ __snapshot_0_wpos_5
0:	__snapshot_0_wpos_5 ≤ __snapshot_0_wpos_5 ∧ __snapshot_0_wpos_5 ≤ __snapshot_0_wpos_5
1:	__snapshot_0_wpos_5 ≤ __snapshot_0_wpos_5 ∧ __snapshot_0_wpos_5 ≤ __snapshot_0_wpos_5

6.1.1.1.7 Fresh Variable Addition

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

5:	__snapshot_0_wpos_4 ≤ wpos_4 ∧ wpos_4 ≤ __snapshot_0_wpos_4
7:	__snapshot_0_wpos_4 ≤ __snapshot_0_wpos_4 ∧ __snapshot_0_wpos_4 ≤ __snapshot_0_wpos_4
0:	__snapshot_0_wpos_4 ≤ __snapshot_0_wpos_4 ∧ __snapshot_0_wpos_4 ≤ __snapshot_0_wpos_4
1:	__snapshot_0_wpos_4 ≤ __snapshot_0_wpos_4 ∧ __snapshot_0_wpos_4 ≤ __snapshot_0_wpos_4

6.1.1.1.8 Fresh Variable Addition

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

5:	__snapshot_0_wpos_3 ≤ wpos_3 ∧ wpos_3 ≤ __snapshot_0_wpos_3
7:	__snapshot_0_wpos_3 ≤ __snapshot_0_wpos_3 ∧ __snapshot_0_wpos_3 ≤ __snapshot_0_wpos_3
0:	__snapshot_0_wpos_3 ≤ __snapshot_0_wpos_3 ∧ __snapshot_0_wpos_3 ≤ __snapshot_0_wpos_3
1:	__snapshot_0_wpos_3 ≤ __snapshot_0_wpos_3 ∧ __snapshot_0_wpos_3 ≤ __snapshot_0_wpos_3

6.1.1.1.9 Fresh Variable Addition

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

5:	__snapshot_0_wpos_2 ≤ wpos_2 ∧ wpos_2 ≤ __snapshot_0_wpos_2
7:	__snapshot_0_wpos_2 ≤ __snapshot_0_wpos_2 ∧ __snapshot_0_wpos_2 ≤ __snapshot_0_wpos_2
0:	__snapshot_0_wpos_2 ≤ __snapshot_0_wpos_2 ∧ __snapshot_0_wpos_2 ≤ __snapshot_0_wpos_2
1:	__snapshot_0_wpos_2 ≤ __snapshot_0_wpos_2 ∧ __snapshot_0_wpos_2 ≤ __snapshot_0_wpos_2

6.1.1.1.10 Fresh Variable Addition

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

5:	__snapshot_0_wpos_1 ≤ wpos_1 ∧ wpos_1 ≤ __snapshot_0_wpos_1
7:	__snapshot_0_wpos_1 ≤ __snapshot_0_wpos_1 ∧ __snapshot_0_wpos_1 ≤ __snapshot_0_wpos_1
0:	__snapshot_0_wpos_1 ≤ __snapshot_0_wpos_1 ∧ __snapshot_0_wpos_1 ≤ __snapshot_0_wpos_1
1:	__snapshot_0_wpos_1 ≤ __snapshot_0_wpos_1 ∧ __snapshot_0_wpos_1 ≤ __snapshot_0_wpos_1

6.1.1.1.11 Fresh Variable Addition

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

5:	__snapshot_0_wpos_0 ≤ wpos_0 ∧ wpos_0 ≤ __snapshot_0_wpos_0
7:	__snapshot_0_wpos_0 ≤ __snapshot_0_wpos_0 ∧ __snapshot_0_wpos_0 ≤ __snapshot_0_wpos_0
0:	__snapshot_0_wpos_0 ≤ __snapshot_0_wpos_0 ∧ __snapshot_0_wpos_0 ≤ __snapshot_0_wpos_0
1:	__snapshot_0_wpos_0 ≤ __snapshot_0_wpos_0 ∧ __snapshot_0_wpos_0 ≤ __snapshot_0_wpos_0

6.1.1.1.12 Fresh Variable Addition

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

5:	__snapshot_0_seq_post ≤ seq_post ∧ seq_post ≤ __snapshot_0_seq_post
7:	__snapshot_0_seq_post ≤ __snapshot_0_seq_post ∧ __snapshot_0_seq_post ≤ __snapshot_0_seq_post
0:	__snapshot_0_seq_post ≤ __snapshot_0_seq_post ∧ __snapshot_0_seq_post ≤ __snapshot_0_seq_post
1:	__snapshot_0_seq_post ≤ __snapshot_0_seq_post ∧ __snapshot_0_seq_post ≤ __snapshot_0_seq_post

6.1.1.1.13 Fresh Variable Addition

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

5:	__snapshot_0_seq_0 ≤ seq_0 ∧ seq_0 ≤ __snapshot_0_seq_0
7:	__snapshot_0_seq_0 ≤ __snapshot_0_seq_0 ∧ __snapshot_0_seq_0 ≤ __snapshot_0_seq_0
0:	__snapshot_0_seq_0 ≤ __snapshot_0_seq_0 ∧ __snapshot_0_seq_0 ≤ __snapshot_0_seq_0
1:	__snapshot_0_seq_0 ≤ __snapshot_0_seq_0 ∧ __snapshot_0_seq_0 ≤ __snapshot_0_seq_0

6.1.1.1.14 Fresh Variable Addition

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

5:	__snapshot_0_pos_post ≤ pos_post ∧ pos_post ≤ __snapshot_0_pos_post
7:	__snapshot_0_pos_post ≤ __snapshot_0_pos_post ∧ __snapshot_0_pos_post ≤ __snapshot_0_pos_post
0:	__snapshot_0_pos_post ≤ __snapshot_0_pos_post ∧ __snapshot_0_pos_post ≤ __snapshot_0_pos_post
1:	__snapshot_0_pos_post ≤ __snapshot_0_pos_post ∧ __snapshot_0_pos_post ≤ __snapshot_0_pos_post

6.1.1.1.15 Fresh Variable Addition

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

5:	__snapshot_0_pos_1 ≤ pos_1 ∧ pos_1 ≤ __snapshot_0_pos_1
7:	__snapshot_0_pos_1 ≤ __snapshot_0_pos_1 ∧ __snapshot_0_pos_1 ≤ __snapshot_0_pos_1
0:	__snapshot_0_pos_1 ≤ __snapshot_0_pos_1 ∧ __snapshot_0_pos_1 ≤ __snapshot_0_pos_1
1:	__snapshot_0_pos_1 ≤ __snapshot_0_pos_1 ∧ __snapshot_0_pos_1 ≤ __snapshot_0_pos_1

6.1.1.1.16 Fresh Variable Addition

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

5:	__snapshot_0_pos_0 ≤ pos_0 ∧ pos_0 ≤ __snapshot_0_pos_0
7:	__snapshot_0_pos_0 ≤ __snapshot_0_pos_0 ∧ __snapshot_0_pos_0 ≤ __snapshot_0_pos_0
0:	__snapshot_0_pos_0 ≤ __snapshot_0_pos_0 ∧ __snapshot_0_pos_0 ≤ __snapshot_0_pos_0
1:	__snapshot_0_pos_0 ≤ __snapshot_0_pos_0 ∧ __snapshot_0_pos_0 ≤ __snapshot_0_pos_0

6.1.1.1.17 Fresh Variable Addition

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

5:	__snapshot_0_pi_post ≤ pi_post ∧ pi_post ≤ __snapshot_0_pi_post
7:	__snapshot_0_pi_post ≤ __snapshot_0_pi_post ∧ __snapshot_0_pi_post ≤ __snapshot_0_pi_post
0:	__snapshot_0_pi_post ≤ __snapshot_0_pi_post ∧ __snapshot_0_pi_post ≤ __snapshot_0_pi_post
1:	__snapshot_0_pi_post ≤ __snapshot_0_pi_post ∧ __snapshot_0_pi_post ≤ __snapshot_0_pi_post

6.1.1.1.18 Fresh Variable Addition

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

5:	__snapshot_0_pi_2 ≤ pi_2 ∧ pi_2 ≤ __snapshot_0_pi_2
7:	__snapshot_0_pi_2 ≤ __snapshot_0_pi_2 ∧ __snapshot_0_pi_2 ≤ __snapshot_0_pi_2
0:	__snapshot_0_pi_2 ≤ __snapshot_0_pi_2 ∧ __snapshot_0_pi_2 ≤ __snapshot_0_pi_2
1:	__snapshot_0_pi_2 ≤ __snapshot_0_pi_2 ∧ __snapshot_0_pi_2 ≤ __snapshot_0_pi_2

6.1.1.1.19 Fresh Variable Addition

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

5:	__snapshot_0_pi_1 ≤ pi_1 ∧ pi_1 ≤ __snapshot_0_pi_1
7:	__snapshot_0_pi_1 ≤ __snapshot_0_pi_1 ∧ __snapshot_0_pi_1 ≤ __snapshot_0_pi_1
0:	__snapshot_0_pi_1 ≤ __snapshot_0_pi_1 ∧ __snapshot_0_pi_1 ≤ __snapshot_0_pi_1
1:	__snapshot_0_pi_1 ≤ __snapshot_0_pi_1 ∧ __snapshot_0_pi_1 ≤ __snapshot_0_pi_1

6.1.1.1.20 Fresh Variable Addition

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

5:	__snapshot_0_pi_0 ≤ pi_0 ∧ pi_0 ≤ __snapshot_0_pi_0
7:	__snapshot_0_pi_0 ≤ __snapshot_0_pi_0 ∧ __snapshot_0_pi_0 ≤ __snapshot_0_pi_0
0:	__snapshot_0_pi_0 ≤ __snapshot_0_pi_0 ∧ __snapshot_0_pi_0 ≤ __snapshot_0_pi_0
1:	__snapshot_0_pi_0 ≤ __snapshot_0_pi_0 ∧ __snapshot_0_pi_0 ≤ __snapshot_0_pi_0

6.1.1.1.21 Fresh Variable Addition

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

5:	__snapshot_0_n_post ≤ n_post ∧ n_post ≤ __snapshot_0_n_post
7:	__snapshot_0_n_post ≤ __snapshot_0_n_post ∧ __snapshot_0_n_post ≤ __snapshot_0_n_post
0:	__snapshot_0_n_post ≤ __snapshot_0_n_post ∧ __snapshot_0_n_post ≤ __snapshot_0_n_post
1:	__snapshot_0_n_post ≤ __snapshot_0_n_post ∧ __snapshot_0_n_post ≤ __snapshot_0_n_post

6.1.1.1.22 Fresh Variable Addition

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

5:	__snapshot_0_n_0 ≤ n_0 ∧ n_0 ≤ __snapshot_0_n_0
7:	__snapshot_0_n_0 ≤ __snapshot_0_n_0 ∧ __snapshot_0_n_0 ≤ __snapshot_0_n_0
0:	__snapshot_0_n_0 ≤ __snapshot_0_n_0 ∧ __snapshot_0_n_0 ≤ __snapshot_0_n_0
1:	__snapshot_0_n_0 ≤ __snapshot_0_n_0 ∧ __snapshot_0_n_0 ≤ __snapshot_0_n_0

6.1.1.1.23 Fresh Variable Addition

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

5:	__snapshot_0_max_post ≤ max_post ∧ max_post ≤ __snapshot_0_max_post
7:	__snapshot_0_max_post ≤ __snapshot_0_max_post ∧ __snapshot_0_max_post ≤ __snapshot_0_max_post
0:	__snapshot_0_max_post ≤ __snapshot_0_max_post ∧ __snapshot_0_max_post ≤ __snapshot_0_max_post
1:	__snapshot_0_max_post ≤ __snapshot_0_max_post ∧ __snapshot_0_max_post ≤ __snapshot_0_max_post

6.1.1.1.24 Fresh Variable Addition

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

5:	__snapshot_0_max_0 ≤ max_0 ∧ max_0 ≤ __snapshot_0_max_0
7:	__snapshot_0_max_0 ≤ __snapshot_0_max_0 ∧ __snapshot_0_max_0 ≤ __snapshot_0_max_0
0:	__snapshot_0_max_0 ≤ __snapshot_0_max_0 ∧ __snapshot_0_max_0 ≤ __snapshot_0_max_0
1:	__snapshot_0_max_0 ≤ __snapshot_0_max_0 ∧ __snapshot_0_max_0 ≤ __snapshot_0_max_0

6.1.1.1.25 Fresh Variable Addition

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

5:	__snapshot_0_m_post ≤ m_post ∧ m_post ≤ __snapshot_0_m_post
7:	__snapshot_0_m_post ≤ __snapshot_0_m_post ∧ __snapshot_0_m_post ≤ __snapshot_0_m_post
0:	__snapshot_0_m_post ≤ __snapshot_0_m_post ∧ __snapshot_0_m_post ≤ __snapshot_0_m_post
1:	__snapshot_0_m_post ≤ __snapshot_0_m_post ∧ __snapshot_0_m_post ≤ __snapshot_0_m_post

6.1.1.1.26 Fresh Variable Addition

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

5:	__snapshot_0_m_3 ≤ m_3 ∧ m_3 ≤ __snapshot_0_m_3
7:	__snapshot_0_m_3 ≤ __snapshot_0_m_3 ∧ __snapshot_0_m_3 ≤ __snapshot_0_m_3
0:	__snapshot_0_m_3 ≤ __snapshot_0_m_3 ∧ __snapshot_0_m_3 ≤ __snapshot_0_m_3
1:	__snapshot_0_m_3 ≤ __snapshot_0_m_3 ∧ __snapshot_0_m_3 ≤ __snapshot_0_m_3

6.1.1.1.27 Fresh Variable Addition

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

5:	__snapshot_0_m_2 ≤ m_2 ∧ m_2 ≤ __snapshot_0_m_2
7:	__snapshot_0_m_2 ≤ __snapshot_0_m_2 ∧ __snapshot_0_m_2 ≤ __snapshot_0_m_2
0:	__snapshot_0_m_2 ≤ __snapshot_0_m_2 ∧ __snapshot_0_m_2 ≤ __snapshot_0_m_2
1:	__snapshot_0_m_2 ≤ __snapshot_0_m_2 ∧ __snapshot_0_m_2 ≤ __snapshot_0_m_2

6.1.1.1.28 Fresh Variable Addition

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

5:	__snapshot_0_m_1 ≤ m_1 ∧ m_1 ≤ __snapshot_0_m_1
7:	__snapshot_0_m_1 ≤ __snapshot_0_m_1 ∧ __snapshot_0_m_1 ≤ __snapshot_0_m_1
0:	__snapshot_0_m_1 ≤ __snapshot_0_m_1 ∧ __snapshot_0_m_1 ≤ __snapshot_0_m_1
1:	__snapshot_0_m_1 ≤ __snapshot_0_m_1 ∧ __snapshot_0_m_1 ≤ __snapshot_0_m_1

6.1.1.1.29 Fresh Variable Addition

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

5:	__snapshot_0_m_0 ≤ m_0 ∧ m_0 ≤ __snapshot_0_m_0
7:	__snapshot_0_m_0 ≤ __snapshot_0_m_0 ∧ __snapshot_0_m_0 ≤ __snapshot_0_m_0
0:	__snapshot_0_m_0 ≤ __snapshot_0_m_0 ∧ __snapshot_0_m_0 ≤ __snapshot_0_m_0
1:	__snapshot_0_m_0 ≤ __snapshot_0_m_0 ∧ __snapshot_0_m_0 ≤ __snapshot_0_m_0

6.1.1.1.30 Fresh Variable Addition

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

5:	__snapshot_0_c2_post ≤ c2_post ∧ c2_post ≤ __snapshot_0_c2_post
7:	__snapshot_0_c2_post ≤ __snapshot_0_c2_post ∧ __snapshot_0_c2_post ≤ __snapshot_0_c2_post
0:	__snapshot_0_c2_post ≤ __snapshot_0_c2_post ∧ __snapshot_0_c2_post ≤ __snapshot_0_c2_post
1:	__snapshot_0_c2_post ≤ __snapshot_0_c2_post ∧ __snapshot_0_c2_post ≤ __snapshot_0_c2_post

6.1.1.1.31 Fresh Variable Addition

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

5:	__snapshot_0_c2_3 ≤ c2_3 ∧ c2_3 ≤ __snapshot_0_c2_3
7:	__snapshot_0_c2_3 ≤ __snapshot_0_c2_3 ∧ __snapshot_0_c2_3 ≤ __snapshot_0_c2_3
0:	__snapshot_0_c2_3 ≤ __snapshot_0_c2_3 ∧ __snapshot_0_c2_3 ≤ __snapshot_0_c2_3
1:	__snapshot_0_c2_3 ≤ __snapshot_0_c2_3 ∧ __snapshot_0_c2_3 ≤ __snapshot_0_c2_3

6.1.1.1.32 Fresh Variable Addition

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

5:	__snapshot_0_c2_2 ≤ c2_2 ∧ c2_2 ≤ __snapshot_0_c2_2
7:	__snapshot_0_c2_2 ≤ __snapshot_0_c2_2 ∧ __snapshot_0_c2_2 ≤ __snapshot_0_c2_2
0:	__snapshot_0_c2_2 ≤ __snapshot_0_c2_2 ∧ __snapshot_0_c2_2 ≤ __snapshot_0_c2_2
1:	__snapshot_0_c2_2 ≤ __snapshot_0_c2_2 ∧ __snapshot_0_c2_2 ≤ __snapshot_0_c2_2

6.1.1.1.33 Fresh Variable Addition

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

5:	__snapshot_0_c2_1 ≤ c2_1 ∧ c2_1 ≤ __snapshot_0_c2_1
7:	__snapshot_0_c2_1 ≤ __snapshot_0_c2_1 ∧ __snapshot_0_c2_1 ≤ __snapshot_0_c2_1
0:	__snapshot_0_c2_1 ≤ __snapshot_0_c2_1 ∧ __snapshot_0_c2_1 ≤ __snapshot_0_c2_1
1:	__snapshot_0_c2_1 ≤ __snapshot_0_c2_1 ∧ __snapshot_0_c2_1 ≤ __snapshot_0_c2_1

6.1.1.1.34 Fresh Variable Addition

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

5:	__snapshot_0_c2_0 ≤ c2_0 ∧ c2_0 ≤ __snapshot_0_c2_0
7:	__snapshot_0_c2_0 ≤ __snapshot_0_c2_0 ∧ __snapshot_0_c2_0 ≤ __snapshot_0_c2_0
0:	__snapshot_0_c2_0 ≤ __snapshot_0_c2_0 ∧ __snapshot_0_c2_0 ≤ __snapshot_0_c2_0
1:	__snapshot_0_c2_0 ≤ __snapshot_0_c2_0 ∧ __snapshot_0_c2_0 ≤ __snapshot_0_c2_0

6.1.1.1.35 Fresh Variable Addition

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

5:	__snapshot_0_c1_post ≤ c1_post ∧ c1_post ≤ __snapshot_0_c1_post
7:	__snapshot_0_c1_post ≤ __snapshot_0_c1_post ∧ __snapshot_0_c1_post ≤ __snapshot_0_c1_post
0:	__snapshot_0_c1_post ≤ __snapshot_0_c1_post ∧ __snapshot_0_c1_post ≤ __snapshot_0_c1_post
1:	__snapshot_0_c1_post ≤ __snapshot_0_c1_post ∧ __snapshot_0_c1_post ≤ __snapshot_0_c1_post

6.1.1.1.36 Fresh Variable Addition

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

5:	__snapshot_0_c1_4 ≤ c1_4 ∧ c1_4 ≤ __snapshot_0_c1_4
7:	__snapshot_0_c1_4 ≤ __snapshot_0_c1_4 ∧ __snapshot_0_c1_4 ≤ __snapshot_0_c1_4
0:	__snapshot_0_c1_4 ≤ __snapshot_0_c1_4 ∧ __snapshot_0_c1_4 ≤ __snapshot_0_c1_4
1:	__snapshot_0_c1_4 ≤ __snapshot_0_c1_4 ∧ __snapshot_0_c1_4 ≤ __snapshot_0_c1_4

6.1.1.1.37 Fresh Variable Addition

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

5:	__snapshot_0_c1_3 ≤ c1_3 ∧ c1_3 ≤ __snapshot_0_c1_3
7:	__snapshot_0_c1_3 ≤ __snapshot_0_c1_3 ∧ __snapshot_0_c1_3 ≤ __snapshot_0_c1_3
0:	__snapshot_0_c1_3 ≤ __snapshot_0_c1_3 ∧ __snapshot_0_c1_3 ≤ __snapshot_0_c1_3
1:	__snapshot_0_c1_3 ≤ __snapshot_0_c1_3 ∧ __snapshot_0_c1_3 ≤ __snapshot_0_c1_3

6.1.1.1.38 Fresh Variable Addition

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

5:	__snapshot_0_c1_2 ≤ c1_2 ∧ c1_2 ≤ __snapshot_0_c1_2
7:	__snapshot_0_c1_2 ≤ __snapshot_0_c1_2 ∧ __snapshot_0_c1_2 ≤ __snapshot_0_c1_2
0:	__snapshot_0_c1_2 ≤ __snapshot_0_c1_2 ∧ __snapshot_0_c1_2 ≤ __snapshot_0_c1_2
1:	__snapshot_0_c1_2 ≤ __snapshot_0_c1_2 ∧ __snapshot_0_c1_2 ≤ __snapshot_0_c1_2

6.1.1.1.39 Fresh Variable Addition

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

5:	__snapshot_0_c1_1 ≤ c1_1 ∧ c1_1 ≤ __snapshot_0_c1_1
7:	__snapshot_0_c1_1 ≤ __snapshot_0_c1_1 ∧ __snapshot_0_c1_1 ≤ __snapshot_0_c1_1
0:	__snapshot_0_c1_1 ≤ __snapshot_0_c1_1 ∧ __snapshot_0_c1_1 ≤ __snapshot_0_c1_1
1:	__snapshot_0_c1_1 ≤ __snapshot_0_c1_1 ∧ __snapshot_0_c1_1 ≤ __snapshot_0_c1_1

6.1.1.1.40 Fresh Variable Addition

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

5:	__snapshot_0_c1_0 ≤ c1_0 ∧ c1_0 ≤ __snapshot_0_c1_0
7:	__snapshot_0_c1_0 ≤ __snapshot_0_c1_0 ∧ __snapshot_0_c1_0 ≤ __snapshot_0_c1_0
0:	__snapshot_0_c1_0 ≤ __snapshot_0_c1_0 ∧ __snapshot_0_c1_0 ≤ __snapshot_0_c1_0
1:	__snapshot_0_c1_0 ≤ __snapshot_0_c1_0 ∧ __snapshot_0_c1_0 ≤ __snapshot_0_c1_0

6.1.1.1.41 Invariant Updates

The following invariants are asserted.

0:	c1_post ≤ 0 ∧ c1_post + pi_0 − seq_0 ≤ 0 ∧ max_0 − n_post ≤ 0 ∧ − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0 ∨ c1_post + pi_0 − seq_0 ≤ 0 ∧ c1_post − n_post ≤ 0 ∧ max_0 − n_post ≤ 0 ∧ − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0
1:	− c1_0 + c1_post + 2⋅c2_1 + m_1 − n_post ≤ 0 ∧ 1 − c1_0 + c1_post + pi_0 − seq_0 ≤ 0 ∧ 1 + pi_0 − seq_0 ≤ 0 ∧ m_3 − n_post ≤ 0 ∧ max_0 − n_post ≤ 0 ∧ −1 + c1_post ≤ 0 ∧ 1 − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ −1 + pos_post ≤ 0 ∧ 1 − pos_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ −1 + c1_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − pos_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0 ∧ c2_post ≤ 0 ∧ − c2_post ≤ 0 ∧ −1 + c1_1 ≤ 0 ∧ 1 − c1_1 ≤ 0 ∧ −1 + c1_2 ≤ 0 ∧ 1 − c1_2 ≤ 0 ∧ −1 + c1_3 ≤ 0 ∧ 1 − c1_3 ≤ 0 ∧ c1_4 ≤ 0 ∧ − c1_4 ≤ 0 ∧ c2_1 ≤ 0 ∧ − c2_1 ≤ 0 ∧ −1 + c2_2 ≤ 0 ∧ 1 − c2_2 ≤ 0 ∧ −1 + c2_3 ≤ 0 ∧ 1 − c2_3 ≤ 0 ∧ 1 − m_1 ≤ 0 ∧ 1 − m_2 ≤ 0 ∧ 1 − m_3 ≤ 0 ∧ pi_1 ≤ 0 ∧ 1 − pi_2 ≤ 0 ∧ −1 + wpos_1 ≤ 0 ∧ 1 − wpos_1 ≤ 0 ∧ wpos_2 ≤ 0 ∧ − wpos_2 ≤ 0 ∧ −1 + wpos_3 ≤ 0 ∧ 1 − wpos_3 ≤ 0 ∧ wpos_4 ≤ 0 ∧ − wpos_4 ≤ 0 ∧ −1 + wpos_5 ≤ 0 ∧ 1 − wpos_5 ≤ 0 ∧ 1 − z_1 ≤ 0 ∧ 1 − z_2 ≤ 0 ∧ c2_0 ≤ 0 ∧ − c2_0 ≤ 0
2:	TRUE
3:	TRUE
0:	c1_post ≤ 0 ∧ c1_post + pi_0 − seq_0 ≤ 0 ∧ max_0 − n_post ≤ 0 ∧ − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0 ∨ −1 + __snapshot_0_c1_post − __snapshot_0_n_post + __snapshot_0_pi_0 ≤ 0 ∧ 1 + __snapshot_0_c1_post − __snapshot_0_n_post + __snapshot_0_pi_0 − c1_post + n_post − pi_0 ≤ 0 ∧ −3 + c1_post + max_0 − n_post ≤ 0 ∧ c1_post + pi_0 − seq_0 ≤ 0 ∧ c1_post − n_post ≤ 0 ∧ max_0 − n_post ≤ 0 ∧ − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0 ∨ c1_post + pi_0 − seq_0 ≤ 0 ∧ c1_post − n_post ≤ 0 ∧ max_0 − n_post ≤ 0 ∧ − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0
1:	−1 + __snapshot_0_c1_post − __snapshot_0_n_post + __snapshot_0_pi_0 ≤ 0 ∧ 2 − c1_0 + c1_post + m_1 − n_post ≤ 0 ∧ −3 + 2⋅c1_4 + c1_post + max_0 − n_post ≤ 0 ∧ __snapshot_0_c1_post − __snapshot_0_n_post + __snapshot_0_pi_0 + n_post − pi_0 ≤ 0 ∧ 1 + pi_0 − seq_0 ≤ 0 ∧ c1_post + pi_0 − seq_0 ≤ 0 ∧ m_2 − n_post ≤ 0 ∧ max_0 − n_post ≤ 0 ∧ −1 + c1_post ≤ 0 ∧ 1 − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ −1 + pos_post ≤ 0 ∧ 1 − pos_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ −1 + c1_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − pos_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0 ∧ c2_post ≤ 0 ∧ − c2_post ≤ 0 ∧ −1 + c1_1 ≤ 0 ∧ 1 − c1_1 ≤ 0 ∧ −1 + c1_2 ≤ 0 ∧ 1 − c1_2 ≤ 0 ∧ −1 + c1_3 ≤ 0 ∧ 1 − c1_3 ≤ 0 ∧ c1_4 ≤ 0 ∧ − c1_4 ≤ 0 ∧ c2_1 ≤ 0 ∧ − c2_1 ≤ 0 ∧ −1 + c2_2 ≤ 0 ∧ 1 − c2_2 ≤ 0 ∧ −1 + c2_3 ≤ 0 ∧ 1 − c2_3 ≤ 0 ∧ 1 − m_1 ≤ 0 ∧ 1 − m_2 ≤ 0 ∧ 1 − m_3 ≤ 0 ∧ pi_1 ≤ 0 ∧ 1 − pi_2 ≤ 0 ∧ −1 + wpos_1 ≤ 0 ∧ 1 − wpos_1 ≤ 0 ∧ wpos_2 ≤ 0 ∧ − wpos_2 ≤ 0 ∧ −1 + wpos_3 ≤ 0 ∧ 1 − wpos_3 ≤ 0 ∧ wpos_4 ≤ 0 ∧ − wpos_4 ≤ 0 ∧ −1 + wpos_5 ≤ 0 ∧ 1 − wpos_5 ≤ 0 ∧ 1 − z_1 ≤ 0 ∧ 1 − z_2 ≤ 0 ∧ c2_0 ≤ 0 ∧ − c2_0 ≤ 0
0_var_snapshot:	__snapshot_0_c1_post − __snapshot_0_n_post + __snapshot_0_pi_0 + n_post − seq_0 ≤ 0 ∧ __snapshot_0_c1_post − __snapshot_0_n_post + __snapshot_0_pi_0 − pi_0 ≤ 0 ∧ max_0 − n_post ≤ 0 ∧ − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0
0*:	−1 + __snapshot_0_c1_post − __snapshot_0_n_post + __snapshot_0_pi_0 ≤ 0 ∧ 1 + __snapshot_0_c1_post − __snapshot_0_n_post + __snapshot_0_pi_0 − c1_post + n_post − pi_0 ≤ 0 ∧ −3 + c1_post + max_0 − n_post ≤ 0 ∧ 2⋅c1_0 + c1_post − n_post ≤ 0 ∧ c1_post + pi_0 − seq_0 ≤ 0 ∧ c1_post − n_post ≤ 0 ∧ max_0 − n_post ≤ 0 ∧ − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

nodes (location) invariant:

0	(3)	TRUE
1	(2)	TRUE
2	(0)	c1_post ≤ 0 ∧ c1_post + pi_0 − seq_0 ≤ 0 ∧ max_0 − n_post ≤ 0 ∧ − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0
3	(1)	− c1_0 + c1_post + 2⋅c2_1 + m_1 − n_post ≤ 0 ∧ 1 − c1_0 + c1_post + pi_0 − seq_0 ≤ 0 ∧ 1 + pi_0 − seq_0 ≤ 0 ∧ m_3 − n_post ≤ 0 ∧ max_0 − n_post ≤ 0 ∧ −1 + c1_post ≤ 0 ∧ 1 − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ −1 + pos_post ≤ 0 ∧ 1 − pos_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ −1 + c1_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − pos_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0 ∧ c2_post ≤ 0 ∧ − c2_post ≤ 0 ∧ −1 + c1_1 ≤ 0 ∧ 1 − c1_1 ≤ 0 ∧ −1 + c1_2 ≤ 0 ∧ 1 − c1_2 ≤ 0 ∧ −1 + c1_3 ≤ 0 ∧ 1 − c1_3 ≤ 0 ∧ c1_4 ≤ 0 ∧ − c1_4 ≤ 0 ∧ c2_1 ≤ 0 ∧ − c2_1 ≤ 0 ∧ −1 + c2_2 ≤ 0 ∧ 1 − c2_2 ≤ 0 ∧ −1 + c2_3 ≤ 0 ∧ 1 − c2_3 ≤ 0 ∧ 1 − m_1 ≤ 0 ∧ 1 − m_2 ≤ 0 ∧ 1 − m_3 ≤ 0 ∧ pi_1 ≤ 0 ∧ 1 − pi_2 ≤ 0 ∧ −1 + wpos_1 ≤ 0 ∧ 1 − wpos_1 ≤ 0 ∧ wpos_2 ≤ 0 ∧ − wpos_2 ≤ 0 ∧ −1 + wpos_3 ≤ 0 ∧ 1 − wpos_3 ≤ 0 ∧ wpos_4 ≤ 0 ∧ − wpos_4 ≤ 0 ∧ −1 + wpos_5 ≤ 0 ∧ 1 − wpos_5 ≤ 0 ∧ 1 − z_1 ≤ 0 ∧ 1 − z_2 ≤ 0 ∧ c2_0 ≤ 0 ∧ − c2_0 ≤ 0
4	(0)	c1_post ≤ 0 ∧ c1_post + pi_0 − seq_0 ≤ 0 ∧ max_0 − n_post ≤ 0 ∧ − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0
5	(0_var_snapshot)	__snapshot_0_c1_post − __snapshot_0_n_post + __snapshot_0_pi_0 + n_post − seq_0 ≤ 0 ∧ __snapshot_0_c1_post − __snapshot_0_n_post + __snapshot_0_pi_0 − pi_0 ≤ 0 ∧ max_0 − n_post ≤ 0 ∧ − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0
10	(0)	c1_post + pi_0 − seq_0 ≤ 0 ∧ c1_post − n_post ≤ 0 ∧ max_0 − n_post ≤ 0 ∧ − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0
14	(1)	−1 + __snapshot_0_c1_post − __snapshot_0_n_post + __snapshot_0_pi_0 ≤ 0 ∧ 2 − c1_0 + c1_post + m_1 − n_post ≤ 0 ∧ −3 + 2⋅c1_4 + c1_post + max_0 − n_post ≤ 0 ∧ __snapshot_0_c1_post − __snapshot_0_n_post + __snapshot_0_pi_0 + n_post − pi_0 ≤ 0 ∧ 1 + pi_0 − seq_0 ≤ 0 ∧ c1_post + pi_0 − seq_0 ≤ 0 ∧ m_2 − n_post ≤ 0 ∧ max_0 − n_post ≤ 0 ∧ −1 + c1_post ≤ 0 ∧ 1 − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ −1 + pos_post ≤ 0 ∧ 1 − pos_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ −1 + c1_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − pos_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0 ∧ c2_post ≤ 0 ∧ − c2_post ≤ 0 ∧ −1 + c1_1 ≤ 0 ∧ 1 − c1_1 ≤ 0 ∧ −1 + c1_2 ≤ 0 ∧ 1 − c1_2 ≤ 0 ∧ −1 + c1_3 ≤ 0 ∧ 1 − c1_3 ≤ 0 ∧ c1_4 ≤ 0 ∧ − c1_4 ≤ 0 ∧ c2_1 ≤ 0 ∧ − c2_1 ≤ 0 ∧ −1 + c2_2 ≤ 0 ∧ 1 − c2_2 ≤ 0 ∧ −1 + c2_3 ≤ 0 ∧ 1 − c2_3 ≤ 0 ∧ 1 − m_1 ≤ 0 ∧ 1 − m_2 ≤ 0 ∧ 1 − m_3 ≤ 0 ∧ pi_1 ≤ 0 ∧ 1 − pi_2 ≤ 0 ∧ −1 + wpos_1 ≤ 0 ∧ 1 − wpos_1 ≤ 0 ∧ wpos_2 ≤ 0 ∧ − wpos_2 ≤ 0 ∧ −1 + wpos_3 ≤ 0 ∧ 1 − wpos_3 ≤ 0 ∧ wpos_4 ≤ 0 ∧ − wpos_4 ≤ 0 ∧ −1 + wpos_5 ≤ 0 ∧ 1 − wpos_5 ≤ 0 ∧ 1 − z_1 ≤ 0 ∧ 1 − z_2 ≤ 0 ∧ c2_0 ≤ 0 ∧ − c2_0 ≤ 0
15	(0*)	−1 + __snapshot_0_c1_post − __snapshot_0_n_post + __snapshot_0_pi_0 ≤ 0 ∧ 1 + __snapshot_0_c1_post − __snapshot_0_n_post + __snapshot_0_pi_0 − c1_post + n_post − pi_0 ≤ 0 ∧ −3 + c1_post + max_0 − n_post ≤ 0 ∧ 2⋅c1_0 + c1_post − n_post ≤ 0 ∧ c1_post + pi_0 − seq_0 ≤ 0 ∧ c1_post − n_post ≤ 0 ∧ max_0 − n_post ≤ 0 ∧ − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0
16	(0)	−1 + __snapshot_0_c1_post − __snapshot_0_n_post + __snapshot_0_pi_0 ≤ 0 ∧ 1 + __snapshot_0_c1_post − __snapshot_0_n_post + __snapshot_0_pi_0 − c1_post + n_post − pi_0 ≤ 0 ∧ −3 + c1_post + max_0 − n_post ≤ 0 ∧ c1_post + pi_0 − seq_0 ≤ 0 ∧ c1_post − n_post ≤ 0 ∧ max_0 − n_post ≤ 0 ∧ − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0
17	(0_var_snapshot)	__snapshot_0_c1_post − __snapshot_0_n_post + __snapshot_0_pi_0 + n_post − seq_0 ≤ 0 ∧ __snapshot_0_c1_post − __snapshot_0_n_post + __snapshot_0_pi_0 − pi_0 ≤ 0 ∧ max_0 − n_post ≤ 0 ∧ − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0
26	(1)	− c1_0 + c1_post + 2⋅c2_1 + m_1 − n_post ≤ 0 ∧ 1 − c1_0 + c1_post + pi_0 − seq_0 ≤ 0 ∧ 1 + pi_0 − seq_0 ≤ 0 ∧ m_3 − n_post ≤ 0 ∧ max_0 − n_post ≤ 0 ∧ −1 + c1_post ≤ 0 ∧ 1 − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ −1 + pos_post ≤ 0 ∧ 1 − pos_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ −1 + c1_0 ≤ 0 ∧ 1 − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ −1 + pos_0 ≤ 0 ∧ 1 − pos_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0 ∧ c2_post ≤ 0 ∧ − c2_post ≤ 0 ∧ −1 + c1_1 ≤ 0 ∧ 1 − c1_1 ≤ 0 ∧ −1 + c1_2 ≤ 0 ∧ 1 − c1_2 ≤ 0 ∧ −1 + c1_3 ≤ 0 ∧ 1 − c1_3 ≤ 0 ∧ c1_4 ≤ 0 ∧ − c1_4 ≤ 0 ∧ c2_1 ≤ 0 ∧ − c2_1 ≤ 0 ∧ −1 + c2_2 ≤ 0 ∧ 1 − c2_2 ≤ 0 ∧ −1 + c2_3 ≤ 0 ∧ 1 − c2_3 ≤ 0 ∧ 1 − m_1 ≤ 0 ∧ 1 − m_2 ≤ 0 ∧ 1 − m_3 ≤ 0 ∧ pi_1 ≤ 0 ∧ 1 − pi_2 ≤ 0 ∧ −1 + wpos_1 ≤ 0 ∧ 1 − wpos_1 ≤ 0 ∧ wpos_2 ≤ 0 ∧ − wpos_2 ≤ 0 ∧ −1 + wpos_3 ≤ 0 ∧ 1 − wpos_3 ≤ 0 ∧ wpos_4 ≤ 0 ∧ − wpos_4 ≤ 0 ∧ −1 + wpos_5 ≤ 0 ∧ 1 − wpos_5 ≤ 0 ∧ 1 − z_1 ≤ 0 ∧ 1 − z_2 ≤ 0 ∧ c2_0 ≤ 0 ∧ − c2_0 ≤ 0
27	(0)	c1_post + pi_0 − seq_0 ≤ 0 ∧ c1_post − n_post ≤ 0 ∧ max_0 − n_post ≤ 0 ∧ − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0
40	(0_var_snapshot)	__snapshot_0_c1_post − __snapshot_0_n_post + __snapshot_0_pi_0 + n_post − seq_0 ≤ 0 ∧ __snapshot_0_c1_post − __snapshot_0_n_post + __snapshot_0_pi_0 − pi_0 ≤ 0 ∧ max_0 − n_post ≤ 0 ∧ − c1_post ≤ 0 ∧ − max_post ≤ 0 ∧ − n_post ≤ 0 ∧ wpos_post ≤ 0 ∧ − wpos_post ≤ 0 ∧ z_post ≤ 0 ∧ pos_1 ≤ 0 ∧ − pos_1 ≤ 0 ∧ − c1_0 ≤ 0 ∧ − max_0 ≤ 0 ∧ − n_0 ≤ 0 ∧ wpos_0 ≤ 0 ∧ − wpos_0 ≤ 0 ∧ z_0 ≤ 0

initial node: 0
cover edges:

17 → 5

26 → 3

40 → 5
transition edges:

0 3 1

1 2 2

2 0 3

2 4 4

3 1 10

4 5 5

5 0 14

10 0 26

10 4 27

14 1 15

15 7 16

16 5 17

27 5 40

6.1.1.1.42 Transition Removal

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

0:	− c1_post + n_post − pi_0
1:	− __snapshot_0_c1_post + __snapshot_0_n_post − __snapshot_0_pi_0
0_var_snapshot:	− __snapshot_0_c1_post + __snapshot_0_n_post − __snapshot_0_pi_0
0*:	− __snapshot_0_c1_post + __snapshot_0_n_post − __snapshot_0_pi_0

6.1.1.1.43 Transition Removal

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

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

6.1.1.1.44 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert

version: 1.0

0	3 1
1	2 2
2	0 3
2	4 4
3	1 10
4	5 5
5	0 14
10	0 26
10	4 27
14	1 15
15	7 16
16	5 17
27	5 40