# LTS Termination Proof

by T2Cert

## Input

Integer Transition System
• Initial Location: 6
• Transitions: (pre-variables and post-variables)  0 0 1: − ___retres1_9_post + ___retres1_9_post ≤ 0 ∧ ___retres1_9_post − ___retres1_9_post ≤ 0 ∧ − ___retres1_9_0 + ___retres1_9_0 ≤ 0 ∧ ___retres1_9_0 − ___retres1_9_0 ≤ 0 ∧ − ___cil_tmp2_10_post + ___cil_tmp2_10_post ≤ 0 ∧ ___cil_tmp2_10_post − ___cil_tmp2_10_post ≤ 0 ∧ − ___cil_tmp2_10_0 + ___cil_tmp2_10_0 ≤ 0 ∧ ___cil_tmp2_10_0 − ___cil_tmp2_10_0 ≤ 0 ∧ − i_5_post + i_5_post ≤ 0 ∧ i_5_post − i_5_post ≤ 0 ∧ − d_6_0 + d_6_0 ≤ 0 ∧ d_6_0 − d_6_0 ≤ 0 ∧ − i_5_0 + i_5_0 ≤ 0 ∧ i_5_0 − i_5_0 ≤ 0 ∧ − ___retres3_7_post + ___retres3_7_post ≤ 0 ∧ ___retres3_7_post − ___retres3_7_post ≤ 0 ∧ − ___retres3_7_0 + ___retres3_7_0 ≤ 0 ∧ ___retres3_7_0 − ___retres3_7_0 ≤ 0 ∧ − ___cil_tmp4_8_post + ___cil_tmp4_8_post ≤ 0 ∧ ___cil_tmp4_8_post − ___cil_tmp4_8_post ≤ 0 ∧ − ___cil_tmp4_8_0 + ___cil_tmp4_8_0 ≤ 0 ∧ ___cil_tmp4_8_0 − ___cil_tmp4_8_0 ≤ 0 ∧ − Result_4_post + Result_4_post ≤ 0 ∧ Result_4_post − Result_4_post ≤ 0 ∧ − Result_4_0 + Result_4_0 ≤ 0 ∧ Result_4_0 − Result_4_0 ≤ 0 2 1 3: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + i_5_0 ≤ 0 ∧ ___retres3_7_post ≤ 0 ∧ − ___retres3_7_post ≤ 0 ∧ ___cil_tmp4_8_post − ___retres3_7_post ≤ 0 ∧ − ___cil_tmp4_8_post + ___retres3_7_post ≤ 0 ∧ Result_4_post − ___cil_tmp4_8_post ≤ 0 ∧ − Result_4_post + ___cil_tmp4_8_post ≤ 0 ∧ Result_4_0 − Result_4_post ≤ 0 ∧ − Result_4_0 + Result_4_post ≤ 0 ∧ ___cil_tmp4_8_0 − ___cil_tmp4_8_post ≤ 0 ∧ − ___cil_tmp4_8_0 + ___cil_tmp4_8_post ≤ 0 ∧ ___retres3_7_0 − ___retres3_7_post ≤ 0 ∧ − ___retres3_7_0 + ___retres3_7_post ≤ 0 ∧ − ___retres1_9_post + ___retres1_9_post ≤ 0 ∧ ___retres1_9_post − ___retres1_9_post ≤ 0 ∧ − ___retres1_9_0 + ___retres1_9_0 ≤ 0 ∧ ___retres1_9_0 − ___retres1_9_0 ≤ 0 ∧ − ___cil_tmp2_10_post + ___cil_tmp2_10_post ≤ 0 ∧ ___cil_tmp2_10_post − ___cil_tmp2_10_post ≤ 0 ∧ − ___cil_tmp2_10_0 + ___cil_tmp2_10_0 ≤ 0 ∧ ___cil_tmp2_10_0 − ___cil_tmp2_10_0 ≤ 0 ∧ − i_5_post + i_5_post ≤ 0 ∧ i_5_post − i_5_post ≤ 0 ∧ − d_6_0 + d_6_0 ≤ 0 ∧ d_6_0 − d_6_0 ≤ 0 ∧ − i_5_0 + i_5_0 ≤ 0 ∧ i_5_0 − i_5_0 ≤ 0 2 2 4: 0 ≤ 0 ∧ 0 ≤ 0 ∧ − i_5_0 ≤ 0 ∧ − d_6_0 − i_5_0 + i_5_post ≤ 0 ∧ d_6_0 + i_5_0 − i_5_post ≤ 0 ∧ i_5_0 − i_5_post ≤ 0 ∧ − i_5_0 + i_5_post ≤ 0 ∧ − ___retres1_9_post + ___retres1_9_post ≤ 0 ∧ ___retres1_9_post − ___retres1_9_post ≤ 0 ∧ − ___retres1_9_0 + ___retres1_9_0 ≤ 0 ∧ ___retres1_9_0 − ___retres1_9_0 ≤ 0 ∧ − ___cil_tmp2_10_post + ___cil_tmp2_10_post ≤ 0 ∧ ___cil_tmp2_10_post − ___cil_tmp2_10_post ≤ 0 ∧ − ___cil_tmp2_10_0 + ___cil_tmp2_10_0 ≤ 0 ∧ ___cil_tmp2_10_0 − ___cil_tmp2_10_0 ≤ 0 ∧ − d_6_0 + d_6_0 ≤ 0 ∧ d_6_0 − d_6_0 ≤ 0 ∧ − ___retres3_7_post + ___retres3_7_post ≤ 0 ∧ ___retres3_7_post − ___retres3_7_post ≤ 0 ∧ − ___retres3_7_0 + ___retres3_7_0 ≤ 0 ∧ ___retres3_7_0 − ___retres3_7_0 ≤ 0 ∧ − ___cil_tmp4_8_post + ___cil_tmp4_8_post ≤ 0 ∧ ___cil_tmp4_8_post − ___cil_tmp4_8_post ≤ 0 ∧ − ___cil_tmp4_8_0 + ___cil_tmp4_8_0 ≤ 0 ∧ ___cil_tmp4_8_0 − ___cil_tmp4_8_0 ≤ 0 ∧ − Result_4_post + Result_4_post ≤ 0 ∧ Result_4_post − Result_4_post ≤ 0 ∧ − Result_4_0 + Result_4_0 ≤ 0 ∧ Result_4_0 − Result_4_0 ≤ 0 4 3 2: − ___retres1_9_post + ___retres1_9_post ≤ 0 ∧ ___retres1_9_post − ___retres1_9_post ≤ 0 ∧ − ___retres1_9_0 + ___retres1_9_0 ≤ 0 ∧ ___retres1_9_0 − ___retres1_9_0 ≤ 0 ∧ − ___cil_tmp2_10_post + ___cil_tmp2_10_post ≤ 0 ∧ ___cil_tmp2_10_post − ___cil_tmp2_10_post ≤ 0 ∧ − ___cil_tmp2_10_0 + ___cil_tmp2_10_0 ≤ 0 ∧ ___cil_tmp2_10_0 − ___cil_tmp2_10_0 ≤ 0 ∧ − i_5_post + i_5_post ≤ 0 ∧ i_5_post − i_5_post ≤ 0 ∧ − d_6_0 + d_6_0 ≤ 0 ∧ d_6_0 − d_6_0 ≤ 0 ∧ − i_5_0 + i_5_0 ≤ 0 ∧ i_5_0 − i_5_0 ≤ 0 ∧ − ___retres3_7_post + ___retres3_7_post ≤ 0 ∧ ___retres3_7_post − ___retres3_7_post ≤ 0 ∧ − ___retres3_7_0 + ___retres3_7_0 ≤ 0 ∧ ___retres3_7_0 − ___retres3_7_0 ≤ 0 ∧ − ___cil_tmp4_8_post + ___cil_tmp4_8_post ≤ 0 ∧ ___cil_tmp4_8_post − ___cil_tmp4_8_post ≤ 0 ∧ − ___cil_tmp4_8_0 + ___cil_tmp4_8_0 ≤ 0 ∧ ___cil_tmp4_8_0 − ___cil_tmp4_8_0 ≤ 0 ∧ − Result_4_post + Result_4_post ≤ 0 ∧ Result_4_post − Result_4_post ≤ 0 ∧ − Result_4_0 + Result_4_0 ≤ 0 ∧ Result_4_0 − Result_4_0 ≤ 0 1 4 3: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − d_6_0 ≤ 0 ∧ ___retres3_7_post ≤ 0 ∧ − ___retres3_7_post ≤ 0 ∧ ___cil_tmp4_8_post − ___retres3_7_post ≤ 0 ∧ − ___cil_tmp4_8_post + ___retres3_7_post ≤ 0 ∧ Result_4_post − ___cil_tmp4_8_post ≤ 0 ∧ − Result_4_post + ___cil_tmp4_8_post ≤ 0 ∧ Result_4_0 − Result_4_post ≤ 0 ∧ − Result_4_0 + Result_4_post ≤ 0 ∧ ___cil_tmp4_8_0 − ___cil_tmp4_8_post ≤ 0 ∧ − ___cil_tmp4_8_0 + ___cil_tmp4_8_post ≤ 0 ∧ ___retres3_7_0 − ___retres3_7_post ≤ 0 ∧ − ___retres3_7_0 + ___retres3_7_post ≤ 0 ∧ − ___retres1_9_post + ___retres1_9_post ≤ 0 ∧ ___retres1_9_post − ___retres1_9_post ≤ 0 ∧ − ___retres1_9_0 + ___retres1_9_0 ≤ 0 ∧ ___retres1_9_0 − ___retres1_9_0 ≤ 0 ∧ − ___cil_tmp2_10_post + ___cil_tmp2_10_post ≤ 0 ∧ ___cil_tmp2_10_post − ___cil_tmp2_10_post ≤ 0 ∧ − ___cil_tmp2_10_0 + ___cil_tmp2_10_0 ≤ 0 ∧ ___cil_tmp2_10_0 − ___cil_tmp2_10_0 ≤ 0 ∧ − i_5_post + i_5_post ≤ 0 ∧ i_5_post − i_5_post ≤ 0 ∧ − d_6_0 + d_6_0 ≤ 0 ∧ d_6_0 − d_6_0 ≤ 0 ∧ − i_5_0 + i_5_0 ≤ 0 ∧ i_5_0 − i_5_0 ≤ 0 1 5 2: 1 + d_6_0 ≤ 0 ∧ − ___retres1_9_post + ___retres1_9_post ≤ 0 ∧ ___retres1_9_post − ___retres1_9_post ≤ 0 ∧ − ___retres1_9_0 + ___retres1_9_0 ≤ 0 ∧ ___retres1_9_0 − ___retres1_9_0 ≤ 0 ∧ − ___cil_tmp2_10_post + ___cil_tmp2_10_post ≤ 0 ∧ ___cil_tmp2_10_post − ___cil_tmp2_10_post ≤ 0 ∧ − ___cil_tmp2_10_0 + ___cil_tmp2_10_0 ≤ 0 ∧ ___cil_tmp2_10_0 − ___cil_tmp2_10_0 ≤ 0 ∧ − i_5_post + i_5_post ≤ 0 ∧ i_5_post − i_5_post ≤ 0 ∧ − d_6_0 + d_6_0 ≤ 0 ∧ d_6_0 − d_6_0 ≤ 0 ∧ − i_5_0 + i_5_0 ≤ 0 ∧ i_5_0 − i_5_0 ≤ 0 ∧ − ___retres3_7_post + ___retres3_7_post ≤ 0 ∧ ___retres3_7_post − ___retres3_7_post ≤ 0 ∧ − ___retres3_7_0 + ___retres3_7_0 ≤ 0 ∧ ___retres3_7_0 − ___retres3_7_0 ≤ 0 ∧ − ___cil_tmp4_8_post + ___cil_tmp4_8_post ≤ 0 ∧ ___cil_tmp4_8_post − ___cil_tmp4_8_post ≤ 0 ∧ − ___cil_tmp4_8_0 + ___cil_tmp4_8_0 ≤ 0 ∧ ___cil_tmp4_8_0 − ___cil_tmp4_8_0 ≤ 0 ∧ − Result_4_post + Result_4_post ≤ 0 ∧ Result_4_post − Result_4_post ≤ 0 ∧ − Result_4_0 + Result_4_0 ≤ 0 ∧ Result_4_0 − Result_4_0 ≤ 0 3 6 5: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ ___retres1_9_post ≤ 0 ∧ − ___retres1_9_post ≤ 0 ∧ ___cil_tmp2_10_post − ___retres1_9_post ≤ 0 ∧ − ___cil_tmp2_10_post + ___retres1_9_post ≤ 0 ∧ Result_4_post − ___cil_tmp2_10_post ≤ 0 ∧ − Result_4_post + ___cil_tmp2_10_post ≤ 0 ∧ Result_4_0 − Result_4_post ≤ 0 ∧ − Result_4_0 + Result_4_post ≤ 0 ∧ ___cil_tmp2_10_0 − ___cil_tmp2_10_post ≤ 0 ∧ − ___cil_tmp2_10_0 + ___cil_tmp2_10_post ≤ 0 ∧ ___retres1_9_0 − ___retres1_9_post ≤ 0 ∧ − ___retres1_9_0 + ___retres1_9_post ≤ 0 ∧ − i_5_post + i_5_post ≤ 0 ∧ i_5_post − i_5_post ≤ 0 ∧ − d_6_0 + d_6_0 ≤ 0 ∧ d_6_0 − d_6_0 ≤ 0 ∧ − i_5_0 + i_5_0 ≤ 0 ∧ i_5_0 − i_5_0 ≤ 0 ∧ − ___retres3_7_post + ___retres3_7_post ≤ 0 ∧ ___retres3_7_post − ___retres3_7_post ≤ 0 ∧ − ___retres3_7_0 + ___retres3_7_0 ≤ 0 ∧ ___retres3_7_0 − ___retres3_7_0 ≤ 0 ∧ − ___cil_tmp4_8_post + ___cil_tmp4_8_post ≤ 0 ∧ ___cil_tmp4_8_post − ___cil_tmp4_8_post ≤ 0 ∧ − ___cil_tmp4_8_0 + ___cil_tmp4_8_0 ≤ 0 ∧ ___cil_tmp4_8_0 − ___cil_tmp4_8_0 ≤ 0 6 7 0: − ___retres1_9_post + ___retres1_9_post ≤ 0 ∧ ___retres1_9_post − ___retres1_9_post ≤ 0 ∧ − ___retres1_9_0 + ___retres1_9_0 ≤ 0 ∧ ___retres1_9_0 − ___retres1_9_0 ≤ 0 ∧ − ___cil_tmp2_10_post + ___cil_tmp2_10_post ≤ 0 ∧ ___cil_tmp2_10_post − ___cil_tmp2_10_post ≤ 0 ∧ − ___cil_tmp2_10_0 + ___cil_tmp2_10_0 ≤ 0 ∧ ___cil_tmp2_10_0 − ___cil_tmp2_10_0 ≤ 0 ∧ − i_5_post + i_5_post ≤ 0 ∧ i_5_post − i_5_post ≤ 0 ∧ − d_6_0 + d_6_0 ≤ 0 ∧ d_6_0 − d_6_0 ≤ 0 ∧ − i_5_0 + i_5_0 ≤ 0 ∧ i_5_0 − i_5_0 ≤ 0 ∧ − ___retres3_7_post + ___retres3_7_post ≤ 0 ∧ ___retres3_7_post − ___retres3_7_post ≤ 0 ∧ − ___retres3_7_0 + ___retres3_7_0 ≤ 0 ∧ ___retres3_7_0 − ___retres3_7_0 ≤ 0 ∧ − ___cil_tmp4_8_post + ___cil_tmp4_8_post ≤ 0 ∧ ___cil_tmp4_8_post − ___cil_tmp4_8_post ≤ 0 ∧ − ___cil_tmp4_8_0 + ___cil_tmp4_8_0 ≤ 0 ∧ ___cil_tmp4_8_0 − ___cil_tmp4_8_0 ≤ 0 ∧ − Result_4_post + Result_4_post ≤ 0 ∧ Result_4_post − Result_4_post ≤ 0 ∧ − Result_4_0 + Result_4_0 ≤ 0 ∧ Result_4_0 − Result_4_0 ≤ 0

## Proof

The following invariants are asserted.

 0: TRUE 1: TRUE 2: TRUE 3: Result_4_post ≤ 0 ∧ ___cil_tmp4_8_post ≤ 0 ∧ ___retres3_7_post ≤ 0 ∧ − ___retres3_7_post ≤ 0 ∧ Result_4_0 ≤ 0 ∧ ___cil_tmp4_8_0 ≤ 0 ∧ ___retres3_7_0 ≤ 0 ∧ − ___retres3_7_0 ≤ 0 4: TRUE 5: Result_4_post ≤ 0 ∧ ___cil_tmp4_8_post ≤ 0 ∧ ___retres3_7_post ≤ 0 ∧ − ___retres3_7_post ≤ 0 ∧ Result_4_0 ≤ 0 ∧ ___cil_tmp4_8_0 ≤ 0 ∧ ___retres3_7_0 ≤ 0 ∧ − ___retres3_7_0 ≤ 0 ∧ ___cil_tmp2_10_post ≤ 0 ∧ ___retres1_9_post ≤ 0 ∧ − ___retres1_9_post ≤ 0 ∧ ___cil_tmp2_10_0 ≤ 0 ∧ ___retres1_9_0 ≤ 0 ∧ − ___retres1_9_0 ≤ 0 6: TRUE

The invariants are proved as follows.

### IMPACT Invariant Proof

• nodes (location) invariant:  0 (0) TRUE 1 (1) TRUE 2 (2) TRUE 3 (3) Result_4_post ≤ 0 ∧ ___cil_tmp4_8_post ≤ 0 ∧ ___retres3_7_post ≤ 0 ∧ − ___retres3_7_post ≤ 0 ∧ Result_4_0 ≤ 0 ∧ ___cil_tmp4_8_0 ≤ 0 ∧ ___retres3_7_0 ≤ 0 ∧ − ___retres3_7_0 ≤ 0 4 (4) TRUE 5 (5) Result_4_post ≤ 0 ∧ ___cil_tmp4_8_post ≤ 0 ∧ ___retres3_7_post ≤ 0 ∧ − ___retres3_7_post ≤ 0 ∧ Result_4_0 ≤ 0 ∧ ___cil_tmp4_8_0 ≤ 0 ∧ ___retres3_7_0 ≤ 0 ∧ − ___retres3_7_0 ≤ 0 ∧ ___cil_tmp2_10_post ≤ 0 ∧ ___retres1_9_post ≤ 0 ∧ − ___retres1_9_post ≤ 0 ∧ ___cil_tmp2_10_0 ≤ 0 ∧ ___retres1_9_0 ≤ 0 ∧ − ___retres1_9_0 ≤ 0 6 (6) TRUE
• initial node: 6
• cover edges:
• transition edges:  0 0 1 1 4 3 1 5 2 2 1 3 2 2 4 3 6 5 4 3 2 6 7 0

### 2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 2 8 2: − ___retres1_9_post + ___retres1_9_post ≤ 0 ∧ ___retres1_9_post − ___retres1_9_post ≤ 0 ∧ − ___retres1_9_0 + ___retres1_9_0 ≤ 0 ∧ ___retres1_9_0 − ___retres1_9_0 ≤ 0 ∧ − ___cil_tmp2_10_post + ___cil_tmp2_10_post ≤ 0 ∧ ___cil_tmp2_10_post − ___cil_tmp2_10_post ≤ 0 ∧ − ___cil_tmp2_10_0 + ___cil_tmp2_10_0 ≤ 0 ∧ ___cil_tmp2_10_0 − ___cil_tmp2_10_0 ≤ 0 ∧ − i_5_post + i_5_post ≤ 0 ∧ i_5_post − i_5_post ≤ 0 ∧ − d_6_0 + d_6_0 ≤ 0 ∧ d_6_0 − d_6_0 ≤ 0 ∧ − i_5_0 + i_5_0 ≤ 0 ∧ i_5_0 − i_5_0 ≤ 0 ∧ − ___retres3_7_post + ___retres3_7_post ≤ 0 ∧ ___retres3_7_post − ___retres3_7_post ≤ 0 ∧ − ___retres3_7_0 + ___retres3_7_0 ≤ 0 ∧ ___retres3_7_0 − ___retres3_7_0 ≤ 0 ∧ − ___cil_tmp4_8_post + ___cil_tmp4_8_post ≤ 0 ∧ ___cil_tmp4_8_post − ___cil_tmp4_8_post ≤ 0 ∧ − ___cil_tmp4_8_0 + ___cil_tmp4_8_0 ≤ 0 ∧ ___cil_tmp4_8_0 − ___cil_tmp4_8_0 ≤ 0 ∧ − Result_4_post + Result_4_post ≤ 0 ∧ Result_4_post − Result_4_post ≤ 0 ∧ − Result_4_0 + Result_4_0 ≤ 0 ∧ Result_4_0 − Result_4_0 ≤ 0
and for every transition t, a duplicate t is considered.

### 3 Transition Removal

We remove transitions 0, 1, 4, 5, 6, 7 using the following ranking functions, which are bounded by −17.

 6: 0 0: 0 1: 0 2: 0 4: 0 3: 0 5: 0 6: −7 0: −8 1: −9 2: −10 4: −10 2_var_snapshot: −10 2*: −10 3: −14 5: −15
Hints:
 9 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] ] 2 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] ] 3 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 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] ] 1 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] ] 4 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] ] 5 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] ] 6 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] ] 7 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] ]

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

2* 11 2: ___retres1_9_post + ___retres1_9_post ≤ 0___retres1_9_post___retres1_9_post ≤ 0___retres1_9_0 + ___retres1_9_0 ≤ 0___retres1_9_0___retres1_9_0 ≤ 0___cil_tmp2_10_post + ___cil_tmp2_10_post ≤ 0___cil_tmp2_10_post___cil_tmp2_10_post ≤ 0___cil_tmp2_10_0 + ___cil_tmp2_10_0 ≤ 0___cil_tmp2_10_0___cil_tmp2_10_0 ≤ 0i_5_post + i_5_post ≤ 0i_5_posti_5_post ≤ 0d_6_0 + d_6_0 ≤ 0d_6_0d_6_0 ≤ 0i_5_0 + i_5_0 ≤ 0i_5_0i_5_0 ≤ 0___retres3_7_post + ___retres3_7_post ≤ 0___retres3_7_post___retres3_7_post ≤ 0___retres3_7_0 + ___retres3_7_0 ≤ 0___retres3_7_0___retres3_7_0 ≤ 0___cil_tmp4_8_post + ___cil_tmp4_8_post ≤ 0___cil_tmp4_8_post___cil_tmp4_8_post ≤ 0___cil_tmp4_8_0 + ___cil_tmp4_8_0 ≤ 0___cil_tmp4_8_0___cil_tmp4_8_0 ≤ 0Result_4_post + Result_4_post ≤ 0Result_4_postResult_4_post ≤ 0Result_4_0 + Result_4_0 ≤ 0Result_4_0Result_4_0 ≤ 0

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

2 9 2_var_snapshot: ___retres1_9_post + ___retres1_9_post ≤ 0___retres1_9_post___retres1_9_post ≤ 0___retres1_9_0 + ___retres1_9_0 ≤ 0___retres1_9_0___retres1_9_0 ≤ 0___cil_tmp2_10_post + ___cil_tmp2_10_post ≤ 0___cil_tmp2_10_post___cil_tmp2_10_post ≤ 0___cil_tmp2_10_0 + ___cil_tmp2_10_0 ≤ 0___cil_tmp2_10_0___cil_tmp2_10_0 ≤ 0i_5_post + i_5_post ≤ 0i_5_posti_5_post ≤ 0d_6_0 + d_6_0 ≤ 0d_6_0d_6_0 ≤ 0i_5_0 + i_5_0 ≤ 0i_5_0i_5_0 ≤ 0___retres3_7_post + ___retres3_7_post ≤ 0___retres3_7_post___retres3_7_post ≤ 0___retres3_7_0 + ___retres3_7_0 ≤ 0___retres3_7_0___retres3_7_0 ≤ 0___cil_tmp4_8_post + ___cil_tmp4_8_post ≤ 0___cil_tmp4_8_post___cil_tmp4_8_post ≤ 0___cil_tmp4_8_0 + ___cil_tmp4_8_0 ≤ 0___cil_tmp4_8_0___cil_tmp4_8_0 ≤ 0Result_4_post + Result_4_post ≤ 0Result_4_postResult_4_post ≤ 0Result_4_0 + Result_4_0 ≤ 0Result_4_0Result_4_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 { 2, 4, 2_var_snapshot, 2* }.

### 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 8.

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

 9: __snapshot_2____retres1_9_post ≤ ___retres1_9_post ∧ ___retres1_9_post ≤ __snapshot_2____retres1_9_post 11: __snapshot_2____retres1_9_post ≤ __snapshot_2____retres1_9_post ∧ __snapshot_2____retres1_9_post ≤ __snapshot_2____retres1_9_post 2: __snapshot_2____retres1_9_post ≤ __snapshot_2____retres1_9_post ∧ __snapshot_2____retres1_9_post ≤ __snapshot_2____retres1_9_post 3: __snapshot_2____retres1_9_post ≤ __snapshot_2____retres1_9_post ∧ __snapshot_2____retres1_9_post ≤ __snapshot_2____retres1_9_post

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

 9: __snapshot_2____retres1_9_0 ≤ ___retres1_9_0 ∧ ___retres1_9_0 ≤ __snapshot_2____retres1_9_0 11: __snapshot_2____retres1_9_0 ≤ __snapshot_2____retres1_9_0 ∧ __snapshot_2____retres1_9_0 ≤ __snapshot_2____retres1_9_0 2: __snapshot_2____retres1_9_0 ≤ __snapshot_2____retres1_9_0 ∧ __snapshot_2____retres1_9_0 ≤ __snapshot_2____retres1_9_0 3: __snapshot_2____retres1_9_0 ≤ __snapshot_2____retres1_9_0 ∧ __snapshot_2____retres1_9_0 ≤ __snapshot_2____retres1_9_0

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

 9: __snapshot_2____cil_tmp2_10_post ≤ ___cil_tmp2_10_post ∧ ___cil_tmp2_10_post ≤ __snapshot_2____cil_tmp2_10_post 11: __snapshot_2____cil_tmp2_10_post ≤ __snapshot_2____cil_tmp2_10_post ∧ __snapshot_2____cil_tmp2_10_post ≤ __snapshot_2____cil_tmp2_10_post 2: __snapshot_2____cil_tmp2_10_post ≤ __snapshot_2____cil_tmp2_10_post ∧ __snapshot_2____cil_tmp2_10_post ≤ __snapshot_2____cil_tmp2_10_post 3: __snapshot_2____cil_tmp2_10_post ≤ __snapshot_2____cil_tmp2_10_post ∧ __snapshot_2____cil_tmp2_10_post ≤ __snapshot_2____cil_tmp2_10_post

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

 9: __snapshot_2____cil_tmp2_10_0 ≤ ___cil_tmp2_10_0 ∧ ___cil_tmp2_10_0 ≤ __snapshot_2____cil_tmp2_10_0 11: __snapshot_2____cil_tmp2_10_0 ≤ __snapshot_2____cil_tmp2_10_0 ∧ __snapshot_2____cil_tmp2_10_0 ≤ __snapshot_2____cil_tmp2_10_0 2: __snapshot_2____cil_tmp2_10_0 ≤ __snapshot_2____cil_tmp2_10_0 ∧ __snapshot_2____cil_tmp2_10_0 ≤ __snapshot_2____cil_tmp2_10_0 3: __snapshot_2____cil_tmp2_10_0 ≤ __snapshot_2____cil_tmp2_10_0 ∧ __snapshot_2____cil_tmp2_10_0 ≤ __snapshot_2____cil_tmp2_10_0

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

 9: __snapshot_2_i_5_post ≤ i_5_post ∧ i_5_post ≤ __snapshot_2_i_5_post 11: __snapshot_2_i_5_post ≤ __snapshot_2_i_5_post ∧ __snapshot_2_i_5_post ≤ __snapshot_2_i_5_post 2: __snapshot_2_i_5_post ≤ __snapshot_2_i_5_post ∧ __snapshot_2_i_5_post ≤ __snapshot_2_i_5_post 3: __snapshot_2_i_5_post ≤ __snapshot_2_i_5_post ∧ __snapshot_2_i_5_post ≤ __snapshot_2_i_5_post

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

 9: __snapshot_2_d_6_0 ≤ d_6_0 ∧ d_6_0 ≤ __snapshot_2_d_6_0 11: __snapshot_2_d_6_0 ≤ __snapshot_2_d_6_0 ∧ __snapshot_2_d_6_0 ≤ __snapshot_2_d_6_0 2: __snapshot_2_d_6_0 ≤ __snapshot_2_d_6_0 ∧ __snapshot_2_d_6_0 ≤ __snapshot_2_d_6_0 3: __snapshot_2_d_6_0 ≤ __snapshot_2_d_6_0 ∧ __snapshot_2_d_6_0 ≤ __snapshot_2_d_6_0

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

 9: __snapshot_2_i_5_0 ≤ i_5_0 ∧ i_5_0 ≤ __snapshot_2_i_5_0 11: __snapshot_2_i_5_0 ≤ __snapshot_2_i_5_0 ∧ __snapshot_2_i_5_0 ≤ __snapshot_2_i_5_0 2: __snapshot_2_i_5_0 ≤ __snapshot_2_i_5_0 ∧ __snapshot_2_i_5_0 ≤ __snapshot_2_i_5_0 3: __snapshot_2_i_5_0 ≤ __snapshot_2_i_5_0 ∧ __snapshot_2_i_5_0 ≤ __snapshot_2_i_5_0

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

 9: __snapshot_2____retres3_7_post ≤ ___retres3_7_post ∧ ___retres3_7_post ≤ __snapshot_2____retres3_7_post 11: __snapshot_2____retres3_7_post ≤ __snapshot_2____retres3_7_post ∧ __snapshot_2____retres3_7_post ≤ __snapshot_2____retres3_7_post 2: __snapshot_2____retres3_7_post ≤ __snapshot_2____retres3_7_post ∧ __snapshot_2____retres3_7_post ≤ __snapshot_2____retres3_7_post 3: __snapshot_2____retres3_7_post ≤ __snapshot_2____retres3_7_post ∧ __snapshot_2____retres3_7_post ≤ __snapshot_2____retres3_7_post

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

 9: __snapshot_2____retres3_7_0 ≤ ___retres3_7_0 ∧ ___retres3_7_0 ≤ __snapshot_2____retres3_7_0 11: __snapshot_2____retres3_7_0 ≤ __snapshot_2____retres3_7_0 ∧ __snapshot_2____retres3_7_0 ≤ __snapshot_2____retres3_7_0 2: __snapshot_2____retres3_7_0 ≤ __snapshot_2____retres3_7_0 ∧ __snapshot_2____retres3_7_0 ≤ __snapshot_2____retres3_7_0 3: __snapshot_2____retres3_7_0 ≤ __snapshot_2____retres3_7_0 ∧ __snapshot_2____retres3_7_0 ≤ __snapshot_2____retres3_7_0

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

 9: __snapshot_2____cil_tmp4_8_post ≤ ___cil_tmp4_8_post ∧ ___cil_tmp4_8_post ≤ __snapshot_2____cil_tmp4_8_post 11: __snapshot_2____cil_tmp4_8_post ≤ __snapshot_2____cil_tmp4_8_post ∧ __snapshot_2____cil_tmp4_8_post ≤ __snapshot_2____cil_tmp4_8_post 2: __snapshot_2____cil_tmp4_8_post ≤ __snapshot_2____cil_tmp4_8_post ∧ __snapshot_2____cil_tmp4_8_post ≤ __snapshot_2____cil_tmp4_8_post 3: __snapshot_2____cil_tmp4_8_post ≤ __snapshot_2____cil_tmp4_8_post ∧ __snapshot_2____cil_tmp4_8_post ≤ __snapshot_2____cil_tmp4_8_post

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

 9: __snapshot_2____cil_tmp4_8_0 ≤ ___cil_tmp4_8_0 ∧ ___cil_tmp4_8_0 ≤ __snapshot_2____cil_tmp4_8_0 11: __snapshot_2____cil_tmp4_8_0 ≤ __snapshot_2____cil_tmp4_8_0 ∧ __snapshot_2____cil_tmp4_8_0 ≤ __snapshot_2____cil_tmp4_8_0 2: __snapshot_2____cil_tmp4_8_0 ≤ __snapshot_2____cil_tmp4_8_0 ∧ __snapshot_2____cil_tmp4_8_0 ≤ __snapshot_2____cil_tmp4_8_0 3: __snapshot_2____cil_tmp4_8_0 ≤ __snapshot_2____cil_tmp4_8_0 ∧ __snapshot_2____cil_tmp4_8_0 ≤ __snapshot_2____cil_tmp4_8_0

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

 9: __snapshot_2_Result_4_post ≤ Result_4_post ∧ Result_4_post ≤ __snapshot_2_Result_4_post 11: __snapshot_2_Result_4_post ≤ __snapshot_2_Result_4_post ∧ __snapshot_2_Result_4_post ≤ __snapshot_2_Result_4_post 2: __snapshot_2_Result_4_post ≤ __snapshot_2_Result_4_post ∧ __snapshot_2_Result_4_post ≤ __snapshot_2_Result_4_post 3: __snapshot_2_Result_4_post ≤ __snapshot_2_Result_4_post ∧ __snapshot_2_Result_4_post ≤ __snapshot_2_Result_4_post

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

 9: __snapshot_2_Result_4_0 ≤ Result_4_0 ∧ Result_4_0 ≤ __snapshot_2_Result_4_0 11: __snapshot_2_Result_4_0 ≤ __snapshot_2_Result_4_0 ∧ __snapshot_2_Result_4_0 ≤ __snapshot_2_Result_4_0 2: __snapshot_2_Result_4_0 ≤ __snapshot_2_Result_4_0 ∧ __snapshot_2_Result_4_0 ≤ __snapshot_2_Result_4_0 3: __snapshot_2_Result_4_0 ≤ __snapshot_2_Result_4_0 ∧ __snapshot_2_Result_4_0 ≤ __snapshot_2_Result_4_0

The following invariants are asserted.

 0: TRUE 1: TRUE 2: 1 + d_6_0 ≤ 0 3: Result_4_post ≤ 0 ∧ ___cil_tmp4_8_post ≤ 0 ∧ ___retres3_7_post ≤ 0 ∧ − ___retres3_7_post ≤ 0 ∧ Result_4_0 ≤ 0 ∧ ___cil_tmp4_8_0 ≤ 0 ∧ ___retres3_7_0 ≤ 0 ∧ − ___retres3_7_0 ≤ 0 4: 1 + d_6_0 ≤ 0 5: Result_4_post ≤ 0 ∧ ___cil_tmp4_8_post ≤ 0 ∧ ___retres3_7_post ≤ 0 ∧ − ___retres3_7_post ≤ 0 ∧ Result_4_0 ≤ 0 ∧ ___cil_tmp4_8_0 ≤ 0 ∧ ___retres3_7_0 ≤ 0 ∧ − ___retres3_7_0 ≤ 0 ∧ ___cil_tmp2_10_post ≤ 0 ∧ ___retres1_9_post ≤ 0 ∧ − ___retres1_9_post ≤ 0 ∧ ___cil_tmp2_10_0 ≤ 0 ∧ ___retres1_9_0 ≤ 0 ∧ − ___retres1_9_0 ≤ 0 6: TRUE 2: 1 + d_6_0 ≤ 0 ∨ 1 + d_6_0 ≤ 0 ∧ 1 − __snapshot_2_i_5_0 + i_5_0 ≤ 0 ∧ − __snapshot_2_i_5_0 ≤ 0 4: 1 + d_6_0 ≤ 0 ∧ 1 − __snapshot_2_i_5_0 + i_5_0 ≤ 0 ∧ − __snapshot_2_i_5_0 ≤ 0 2_var_snapshot: 1 + d_6_0 ≤ 0 ∧ − __snapshot_2_i_5_0 + i_5_0 ≤ 0 ∧ 1 − __snapshot_2_i_5_0 + d_6_0 + i_5_0 ≤ 0 2*: 1 + d_6_0 ≤ 0 ∧ 1 − __snapshot_2_i_5_0 + i_5_0 ≤ 0 ∧ − __snapshot_2_i_5_0 ≤ 0

The invariants are proved as follows.

### IMPACT Invariant Proof

• nodes (location) invariant:  0 (6) TRUE 1 (0) TRUE 2 (1) TRUE 3 (3) Result_4_post ≤ 0 ∧ ___cil_tmp4_8_post ≤ 0 ∧ ___retres3_7_post ≤ 0 ∧ − ___retres3_7_post ≤ 0 ∧ Result_4_0 ≤ 0 ∧ ___cil_tmp4_8_0 ≤ 0 ∧ ___retres3_7_0 ≤ 0 ∧ − ___retres3_7_0 ≤ 0 4 (2) 1 + d_6_0 ≤ 0 5 (3) Result_4_post ≤ 0 ∧ ___cil_tmp4_8_post ≤ 0 ∧ ___retres3_7_post ≤ 0 ∧ − ___retres3_7_post ≤ 0 ∧ Result_4_0 ≤ 0 ∧ ___cil_tmp4_8_0 ≤ 0 ∧ ___retres3_7_0 ≤ 0 ∧ − ___retres3_7_0 ≤ 0 6 (4) 1 + d_6_0 ≤ 0 7 (2) 1 + d_6_0 ≤ 0 8 (2_var_snapshot) 1 + d_6_0 ≤ 0 ∧ − __snapshot_2_i_5_0 + i_5_0 ≤ 0 ∧ 1 − __snapshot_2_i_5_0 + d_6_0 + i_5_0 ≤ 0 13 (2) 1 + d_6_0 ≤ 0 17 (4) 1 + d_6_0 ≤ 0 ∧ 1 − __snapshot_2_i_5_0 + i_5_0 ≤ 0 ∧ − __snapshot_2_i_5_0 ≤ 0 18 (2*) 1 + d_6_0 ≤ 0 ∧ 1 − __snapshot_2_i_5_0 + i_5_0 ≤ 0 ∧ − __snapshot_2_i_5_0 ≤ 0 19 (2) 1 + d_6_0 ≤ 0 ∧ 1 − __snapshot_2_i_5_0 + i_5_0 ≤ 0 ∧ − __snapshot_2_i_5_0 ≤ 0 20 (2_var_snapshot) 1 + d_6_0 ≤ 0 ∧ − __snapshot_2_i_5_0 + i_5_0 ≤ 0 ∧ 1 − __snapshot_2_i_5_0 + d_6_0 + i_5_0 ≤ 0 25 (5) Result_4_post ≤ 0 ∧ ___cil_tmp4_8_post ≤ 0 ∧ ___retres3_7_post ≤ 0 ∧ − ___retres3_7_post ≤ 0 ∧ Result_4_0 ≤ 0 ∧ ___cil_tmp4_8_0 ≤ 0 ∧ ___retres3_7_0 ≤ 0 ∧ − ___retres3_7_0 ≤ 0 ∧ ___cil_tmp2_10_post ≤ 0 ∧ ___retres1_9_post ≤ 0 ∧ − ___retres1_9_post ≤ 0 ∧ ___cil_tmp2_10_0 ≤ 0 ∧ ___retres1_9_0 ≤ 0 ∧ − ___retres1_9_0 ≤ 0
• initial node: 0
• cover edges:
3 → 5 Hint: distribute conclusion [1, 0, 0, 0, 0, 0, 0, 0] [0, 1, 0, 0, 0, 0, 0, 0] [0, 0, 1, 0, 0, 0, 0, 0] [0, 0, 0, 1, 0, 0, 0, 0] [0, 0, 0, 0, 1, 0, 0, 0] [0, 0, 0, 0, 0, 1, 0, 0] [0, 0, 0, 0, 0, 0, 1, 0] [0, 0, 0, 0, 0, 0, 0, 1]
13 → 4 Hint: [1]
20 → 8 Hint: distribute conclusion [1, 0, 0] [0, 1, 0] [1, 1, 0]
• transition edges:
0 7 1 Hint: auto
1 0 2 Hint: auto
2 4 3 Hint: distribute conclusion [0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 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, 1, 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, 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, 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, 1, 0, 1, 0, 1, 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, 1, 0, 1, 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, 1, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
2 5 4 Hint: [1, 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]
4 1 5 Hint: distribute conclusion [0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 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, 1, 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, 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, 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, 1, 0, 1, 0, 1, 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, 1, 0, 1, 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, 1, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
4 2 6 Hint: [1, 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]
4 8 7 Hint: [1, 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]
5 6 25 Hint: distribute conclusion [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 1, 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, 1, 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, 1, 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, 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, 1, 0, 1, 0, 1, 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, 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, 1, 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, 1, 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, 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, 1, 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, 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, 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, 1, 0, 1, 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, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
6 3 13 Hint: [1, 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]
7 9 8 Hint: distribute conclusion [1, 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] [1, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
8 2 17 Hint: distribute conclusion [1, 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, 0, 0, 0, 0, 1, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] [0, 1, 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]
17 3 18 Hint: distribute conclusion [1, 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, 1, 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, 1, 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]
18 11 19 Hint: distribute conclusion [1, 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, 1, 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, 1, 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]
19 9 20 Hint: distribute conclusion [1, 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, 1, 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, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

### 6.1.1.1.15 Transition Removal

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

 2: i_5_0 4: __snapshot_2_i_5_0 2_var_snapshot: __snapshot_2_i_5_0 2*: __snapshot_2_i_5_0
Hints:
9 distribute assertion
 lexWeak[ [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, 1, 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, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
11 lexStrict[ [0, 1, 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, 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] ]
2 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
3 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 6.1.1.1.16 Transition Removal

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

 2: −1 2_var_snapshot: −2 4: −3 2*: −4
Hints:
9 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] ] 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] ]
2 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] ]
3 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] ]

### 6.1.1.1.17 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0