LTS Termination Proof

by T2Cert

Input

Integer Transition System

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

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
Hints:
5 lexWeak[ [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 lexWeak[ [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, 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 lexWeak[ [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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
2 lexStrict[ [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, 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] ]
3 lexStrict[ [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, 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] ]

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: −1 + c1_0 ≤ 0 ∧ c1_0 + pi_0 − seq_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 + c1_0 ≤ 0 ∧ c1_0 + pi_0 − seq_0 ≤ 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: −1 + c1_0 ≤ 0 ∧ c1_0 + pi_0 − seq_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 + c1_0 ≤ 0 ∧ −2 + __snapshot_0_c1_0 + __snapshot_0_pi_0 ≤ 0 ∧ 1 + __snapshot_0_c1_0 + __snapshot_0_pi_0 − c1_0 − pi_0 ≤ 0 ∧ c1_0 + pi_0 − seq_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: −2 + __snapshot_0_c1_0 + __snapshot_0_pi_0 ≤ 0 ∧ __snapshot_0_c1_0 + __snapshot_0_pi_0 − c1_0 + c1_post − pi_0 ≤ 0 ∧ 1 + c1_0 − c1_post + pi_0 − seq_0 ≤ 0 ∧ c1_0 + pi_0 − seq_0 ≤ 0 ∧ c1_0 − c1_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: −1 + __snapshot_0_c1_0 + __snapshot_0_pi_0 − pi_0 ≤ 0 ∧ __snapshot_0_c1_0 + __snapshot_0_pi_0 − seq_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
0*: −1 + c1_0 ≤ 0 ∧ −2 + __snapshot_0_c1_0 + __snapshot_0_pi_0 ≤ 0 ∧ 1 + __snapshot_0_c1_0 + __snapshot_0_pi_0 − c1_0 − pi_0 ≤ 0 ∧ c1_0 + pi_0 − seq_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

The invariants are proved as follows.

IMPACT Invariant Proof

6.1.1.1.42 Transition Removal

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

0: − c1_0 − pi_0
1: − __snapshot_0_c1_0 − __snapshot_0_pi_0
0_var_snapshot: − __snapshot_0_c1_0 − __snapshot_0_pi_0
0*: − __snapshot_0_c1_0 − __snapshot_0_pi_0
Hints:
5 distribute assertion
lexWeak[ [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, 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, 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, 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] ]
lexWeak[ [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, 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, 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, 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] ]
7 lexStrict[ [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, 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, 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, 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, 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 lexWeak[ [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, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 1] ]
1 lexWeak[ [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, 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, 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] ]

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
Hints:
5 distribute assertion
lexStrict[ [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, 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, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
lexStrict[ [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, 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, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
0 lexWeak[ [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, 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, 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 lexWeak[ [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, 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] ]

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