# 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

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:
 0 4 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
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

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

0* 7 0: z_post + z_post ≤ 0z_postz_post ≤ 0z_2 + z_2 ≤ 0z_2z_2 ≤ 0z_1 + z_1 ≤ 0z_1z_1 ≤ 0z_0 + z_0 ≤ 0z_0z_0 ≤ 0wpos_post + wpos_post ≤ 0wpos_postwpos_post ≤ 0wpos_5 + wpos_5 ≤ 0wpos_5wpos_5 ≤ 0wpos_4 + wpos_4 ≤ 0wpos_4wpos_4 ≤ 0wpos_3 + wpos_3 ≤ 0wpos_3wpos_3 ≤ 0wpos_2 + wpos_2 ≤ 0wpos_2wpos_2 ≤ 0wpos_1 + wpos_1 ≤ 0wpos_1wpos_1 ≤ 0wpos_0 + wpos_0 ≤ 0wpos_0wpos_0 ≤ 0seq_post + seq_post ≤ 0seq_postseq_post ≤ 0seq_0 + seq_0 ≤ 0seq_0seq_0 ≤ 0pos_post + pos_post ≤ 0pos_postpos_post ≤ 0pos_1 + pos_1 ≤ 0pos_1pos_1 ≤ 0pos_0 + pos_0 ≤ 0pos_0pos_0 ≤ 0pi_post + pi_post ≤ 0pi_postpi_post ≤ 0pi_2 + pi_2 ≤ 0pi_2pi_2 ≤ 0pi_1 + pi_1 ≤ 0pi_1pi_1 ≤ 0pi_0 + pi_0 ≤ 0pi_0pi_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0max_post + max_post ≤ 0max_postmax_post ≤ 0max_0 + max_0 ≤ 0max_0max_0 ≤ 0m_post + m_post ≤ 0m_postm_post ≤ 0m_3 + m_3 ≤ 0m_3m_3 ≤ 0m_2 + m_2 ≤ 0m_2m_2 ≤ 0m_1 + m_1 ≤ 0m_1m_1 ≤ 0m_0 + m_0 ≤ 0m_0m_0 ≤ 0c2_post + c2_post ≤ 0c2_postc2_post ≤ 0c2_3 + c2_3 ≤ 0c2_3c2_3 ≤ 0c2_2 + c2_2 ≤ 0c2_2c2_2 ≤ 0c2_1 + c2_1 ≤ 0c2_1c2_1 ≤ 0c2_0 + c2_0 ≤ 0c2_0c2_0 ≤ 0c1_post + c1_post ≤ 0c1_postc1_post ≤ 0c1_4 + c1_4 ≤ 0c1_4c1_4 ≤ 0c1_3 + c1_3 ≤ 0c1_3c1_3 ≤ 0c1_2 + c1_2 ≤ 0c1_2c1_2 ≤ 0c1_1 + c1_1 ≤ 0c1_1c1_1 ≤ 0c1_0 + c1_0 ≤ 0c1_0c1_0 ≤ 0

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 ≤ 0z_postz_post ≤ 0z_2 + z_2 ≤ 0z_2z_2 ≤ 0z_1 + z_1 ≤ 0z_1z_1 ≤ 0z_0 + z_0 ≤ 0z_0z_0 ≤ 0wpos_post + wpos_post ≤ 0wpos_postwpos_post ≤ 0wpos_5 + wpos_5 ≤ 0wpos_5wpos_5 ≤ 0wpos_4 + wpos_4 ≤ 0wpos_4wpos_4 ≤ 0wpos_3 + wpos_3 ≤ 0wpos_3wpos_3 ≤ 0wpos_2 + wpos_2 ≤ 0wpos_2wpos_2 ≤ 0wpos_1 + wpos_1 ≤ 0wpos_1wpos_1 ≤ 0wpos_0 + wpos_0 ≤ 0wpos_0wpos_0 ≤ 0seq_post + seq_post ≤ 0seq_postseq_post ≤ 0seq_0 + seq_0 ≤ 0seq_0seq_0 ≤ 0pos_post + pos_post ≤ 0pos_postpos_post ≤ 0pos_1 + pos_1 ≤ 0pos_1pos_1 ≤ 0pos_0 + pos_0 ≤ 0pos_0pos_0 ≤ 0pi_post + pi_post ≤ 0pi_postpi_post ≤ 0pi_2 + pi_2 ≤ 0pi_2pi_2 ≤ 0pi_1 + pi_1 ≤ 0pi_1pi_1 ≤ 0pi_0 + pi_0 ≤ 0pi_0pi_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0max_post + max_post ≤ 0max_postmax_post ≤ 0max_0 + max_0 ≤ 0max_0max_0 ≤ 0m_post + m_post ≤ 0m_postm_post ≤ 0m_3 + m_3 ≤ 0m_3m_3 ≤ 0m_2 + m_2 ≤ 0m_2m_2 ≤ 0m_1 + m_1 ≤ 0m_1m_1 ≤ 0m_0 + m_0 ≤ 0m_0m_0 ≤ 0c2_post + c2_post ≤ 0c2_postc2_post ≤ 0c2_3 + c2_3 ≤ 0c2_3c2_3 ≤ 0c2_2 + c2_2 ≤ 0c2_2c2_2 ≤ 0c2_1 + c2_1 ≤ 0c2_1c2_1 ≤ 0c2_0 + c2_0 ≤ 0c2_0c2_0 ≤ 0c1_post + c1_post ≤ 0c1_postc1_post ≤ 0c1_4 + c1_4 ≤ 0c1_4c1_4 ≤ 0c1_3 + c1_3 ≤ 0c1_3c1_3 ≤ 0c1_2 + c1_2 ≤ 0c1_2c1_2 ≤ 0c1_1 + c1_1 ≤ 0c1_1c1_1 ≤ 0c1_0 + c1_0 ≤ 0c1_0c1_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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

T2Cert

• version: 1.0