# LTS Termination Proof

by T2Cert

## Input

Integer Transition System
• Initial Location: 12
• Transitions: (pre-variables and post-variables)  0 0 1: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 2 1 3: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 4 2 5: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 6 3 7: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 8 4 6: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + ___const_5_0 − k6_0 ≤ 0 ∧ −1 − j5_0 + j5_post ≤ 0 ∧ 1 + j5_0 − j5_post ≤ 0 ∧ j5_0 − j5_post ≤ 0 ∧ − j5_0 + j5_post ≤ 0 ∧ − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 8 5 9: 0 ≤ 0 ∧ 0 ≤ 0 ∧ − ___const_5_0 + k6_0 ≤ 0 ∧ −1 − k6_0 + k6_post ≤ 0 ∧ 1 + k6_0 − k6_post ≤ 0 ∧ k6_0 − k6_post ≤ 0 ∧ − k6_0 + k6_post ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 7 6 4: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + ___const_5_0 − j5_0 ≤ 0 ∧ −1 − i4_0 + i4_post ≤ 0 ∧ 1 + i4_0 − i4_post ≤ 0 ∧ i4_0 − i4_post ≤ 0 ∧ − i4_0 + i4_post ≤ 0 ∧ − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 7 7 9: 0 ≤ 0 ∧ 0 ≤ 0 ∧ − ___const_5_0 + j5_0 ≤ 0 ∧ −1 + k6_post ≤ 0 ∧ 1 − k6_post ≤ 0 ∧ k6_0 − k6_post ≤ 0 ∧ − k6_0 + k6_post ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 5 8 10: 1 + ___const_5_0 − i4_0 ≤ 0 ∧ − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 5 9 6: 0 ≤ 0 ∧ 0 ≤ 0 ∧ − ___const_5_0 + i4_0 ≤ 0 ∧ −1 + j5_post ≤ 0 ∧ 1 − j5_post ≤ 0 ∧ j5_0 − j5_post ≤ 0 ∧ − j5_0 + j5_post ≤ 0 ∧ − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 9 10 8: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 3 11 0: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + ___const_5_0 − j5_0 ≤ 0 ∧ −1 − i4_0 + i4_post ≤ 0 ∧ 1 + i4_0 − i4_post ≤ 0 ∧ i4_0 − i4_post ≤ 0 ∧ − i4_0 + i4_post ≤ 0 ∧ − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 3 12 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ − ___const_5_0 + j5_0 ≤ 0 ∧ −1 − j5_0 + j5_post ≤ 0 ∧ 1 + j5_0 − j5_post ≤ 0 ∧ j5_0 − j5_post ≤ 0 ∧ − j5_0 + j5_post ≤ 0 ∧ − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 1 13 4: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + ___const_5_0 − i4_0 ≤ 0 ∧ −1 + i4_post ≤ 0 ∧ 1 − i4_post ≤ 0 ∧ i4_0 − i4_post ≤ 0 ∧ − i4_0 + i4_post ≤ 0 ∧ − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 1 14 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ − ___const_5_0 + i4_0 ≤ 0 ∧ −1 + j5_post ≤ 0 ∧ 1 − j5_post ≤ 0 ∧ j5_0 − j5_post ≤ 0 ∧ − j5_0 + j5_post ≤ 0 ∧ − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 11 15 0: 0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 + i4_post ≤ 0 ∧ 1 − i4_post ≤ 0 ∧ i4_0 − i4_post ≤ 0 ∧ − i4_0 + i4_post ≤ 0 ∧ − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 12 16 11: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0

## Proof

### 1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 0 17 0: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 2 24 2: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 4 31 4: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 6 38 6: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 9 45 9: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0
and for every transition t, a duplicate t is considered.

### 2 Transition Removal

We remove transitions 8, 13, 15, 16 using the following ranking functions, which are bounded by −23.

 12: 0 11: 0 0: 0 1: 0 2: 0 3: 0 4: 0 5: 0 6: 0 7: 0 8: 0 9: 0 10: 0 12: −6 11: −7 0: −8 1: −8 2: −8 3: −8 0_var_snapshot: −8 0*: −8 2_var_snapshot: −8 2*: −8 4: −11 5: −11 6: −11 7: −11 8: −11 9: −11 4_var_snapshot: −11 4*: −11 6_var_snapshot: −11 6*: −11 9_var_snapshot: −11 9*: −11 10: −16
Hints:
 18 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 25 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 32 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 39 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 46 lexWeak[ [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] ] 1 lexWeak[ [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] ] 3 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 4 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 5 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 6 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 7 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 9 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 10 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 11 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 12 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 14 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 8 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] ] 13 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] ] 15 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] ] 16 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] ]

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

0* 20 0: k6_post + k6_post ≤ 0k6_postk6_post ≤ 0k6_0 + k6_0 ≤ 0k6_0k6_0 ≤ 0j5_post + j5_post ≤ 0j5_postj5_post ≤ 0j5_0 + j5_0 ≤ 0j5_0j5_0 ≤ 0i4_post + i4_post ≤ 0i4_posti4_post ≤ 0i4_0 + i4_0 ≤ 0i4_0i4_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0

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

0 18 0_var_snapshot: k6_post + k6_post ≤ 0k6_postk6_post ≤ 0k6_0 + k6_0 ≤ 0k6_0k6_0 ≤ 0j5_post + j5_post ≤ 0j5_postj5_post ≤ 0j5_0 + j5_0 ≤ 0j5_0j5_0 ≤ 0i4_post + i4_post ≤ 0i4_posti4_post ≤ 0i4_0 + i4_0 ≤ 0i4_0i4_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0

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

2* 27 2: k6_post + k6_post ≤ 0k6_postk6_post ≤ 0k6_0 + k6_0 ≤ 0k6_0k6_0 ≤ 0j5_post + j5_post ≤ 0j5_postj5_post ≤ 0j5_0 + j5_0 ≤ 0j5_0j5_0 ≤ 0i4_post + i4_post ≤ 0i4_posti4_post ≤ 0i4_0 + i4_0 ≤ 0i4_0i4_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0

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

2 25 2_var_snapshot: k6_post + k6_post ≤ 0k6_postk6_post ≤ 0k6_0 + k6_0 ≤ 0k6_0k6_0 ≤ 0j5_post + j5_post ≤ 0j5_postj5_post ≤ 0j5_0 + j5_0 ≤ 0j5_0j5_0 ≤ 0i4_post + i4_post ≤ 0i4_posti4_post ≤ 0i4_0 + i4_0 ≤ 0i4_0i4_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0

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

4* 34 4: k6_post + k6_post ≤ 0k6_postk6_post ≤ 0k6_0 + k6_0 ≤ 0k6_0k6_0 ≤ 0j5_post + j5_post ≤ 0j5_postj5_post ≤ 0j5_0 + j5_0 ≤ 0j5_0j5_0 ≤ 0i4_post + i4_post ≤ 0i4_posti4_post ≤ 0i4_0 + i4_0 ≤ 0i4_0i4_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0

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

4 32 4_var_snapshot: k6_post + k6_post ≤ 0k6_postk6_post ≤ 0k6_0 + k6_0 ≤ 0k6_0k6_0 ≤ 0j5_post + j5_post ≤ 0j5_postj5_post ≤ 0j5_0 + j5_0 ≤ 0j5_0j5_0 ≤ 0i4_post + i4_post ≤ 0i4_posti4_post ≤ 0i4_0 + i4_0 ≤ 0i4_0i4_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0

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

6* 41 6: k6_post + k6_post ≤ 0k6_postk6_post ≤ 0k6_0 + k6_0 ≤ 0k6_0k6_0 ≤ 0j5_post + j5_post ≤ 0j5_postj5_post ≤ 0j5_0 + j5_0 ≤ 0j5_0j5_0 ≤ 0i4_post + i4_post ≤ 0i4_posti4_post ≤ 0i4_0 + i4_0 ≤ 0i4_0i4_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0

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

6 39 6_var_snapshot: k6_post + k6_post ≤ 0k6_postk6_post ≤ 0k6_0 + k6_0 ≤ 0k6_0k6_0 ≤ 0j5_post + j5_post ≤ 0j5_postj5_post ≤ 0j5_0 + j5_0 ≤ 0j5_0j5_0 ≤ 0i4_post + i4_post ≤ 0i4_posti4_post ≤ 0i4_0 + i4_0 ≤ 0i4_0i4_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0

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

9* 48 9: k6_post + k6_post ≤ 0k6_postk6_post ≤ 0k6_0 + k6_0 ≤ 0k6_0k6_0 ≤ 0j5_post + j5_post ≤ 0j5_postj5_post ≤ 0j5_0 + j5_0 ≤ 0j5_0j5_0 ≤ 0i4_post + i4_post ≤ 0i4_posti4_post ≤ 0i4_0 + i4_0 ≤ 0i4_0i4_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0

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

9 46 9_var_snapshot: k6_post + k6_post ≤ 0k6_postk6_post ≤ 0k6_0 + k6_0 ≤ 0k6_0k6_0 ≤ 0j5_post + j5_post ≤ 0j5_postj5_post ≤ 0j5_0 + j5_0 ≤ 0j5_0j5_0 ≤ 0i4_post + i4_post ≤ 0i4_posti4_post ≤ 0i4_0 + i4_0 ≤ 0i4_0i4_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0

### 13 SCC Decomposition

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

### 13.1 SCC Subproblem 1/2

Here we consider the SCC { 4, 5, 6, 7, 8, 9, 4_var_snapshot, 4*, 6_var_snapshot, 6*, 9_var_snapshot, 9* }.

### 13.1.1 Transition Removal

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

 4: 10 + 12⋅___const_5_0 − 12⋅i4_0 5: 8 + 12⋅___const_5_0 − 12⋅i4_0 6: 12⋅___const_5_0 − 12⋅i4_0 7: 12⋅___const_5_0 − 12⋅i4_0 8: 12⋅___const_5_0 − 12⋅i4_0 9: 12⋅___const_5_0 − 12⋅i4_0 4_var_snapshot: 9 + 12⋅___const_5_0 − 12⋅i4_0 4*: 11 + 12⋅___const_5_0 − 12⋅i4_0 6_var_snapshot: 12⋅___const_5_0 − 12⋅i4_0 6*: 12⋅___const_5_0 − 12⋅i4_0 9_var_snapshot: 12⋅___const_5_0 − 12⋅i4_0 9*: 12⋅___const_5_0 − 12⋅i4_0
Hints:
 32 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 12, 12, 0] ] 34 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 12, 12, 0] ] 39 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 12, 12, 0] ] 41 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 12, 12, 0] ] 46 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 12, 12, 0] ] 48 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 12, 12, 0] ] 2 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 12, 12, 0] ] 3 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 12, 12, 0] ] 4 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 12, 12, 0] ] 5 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 12, 12, 0] ] 6 lexWeak[ [0, 0, 0, 0, 12, 0, 12, 0, 0, 0, 0, 0, 0, 0, 0, 12, 0] ] 7 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 12, 12, 0] ] 9 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 12, 12, 0] , [0, 0, 12, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 10 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 12, 12, 0] ]

### 13.1.2 Transition Removal

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

 4: −1 + 12⋅___const_5_0 − 12⋅j5_0 5: −3 + 12⋅___const_5_0 − 12⋅j5_0 6: 3 + 12⋅___const_5_0 − 12⋅j5_0 7: 1 + 12⋅___const_5_0 − 12⋅j5_0 8: 12⋅___const_5_0 − 12⋅j5_0 9: 12⋅___const_5_0 − 12⋅j5_0 4_var_snapshot: −2 + 12⋅___const_5_0 − 12⋅j5_0 4*: 12⋅___const_5_0 − 12⋅j5_0 6_var_snapshot: 2 + 12⋅___const_5_0 − 12⋅j5_0 6*: 4 + 12⋅___const_5_0 − 12⋅j5_0 9_var_snapshot: 12⋅___const_5_0 − 12⋅j5_0 9*: 12⋅___const_5_0 − 12⋅j5_0
Hints:
 32 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 12, 0, 0, 0, 0, 12, 0] ] 34 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 12, 0, 0, 0, 0, 12, 0] ] 39 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 12, 0, 0, 0, 0, 12, 0] ] 41 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 12, 0, 0, 0, 0, 12, 0] ] 46 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 12, 0, 0, 0, 0, 12, 0] ] 48 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 12, 0, 0, 0, 0, 12, 0] ] 2 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 12, 0, 0, 0, 0, 12, 0] ] 3 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 12, 0, 0, 0, 0, 12, 0] ] 4 lexWeak[ [0, 0, 0, 0, 12, 0, 12, 0, 0, 0, 0, 0, 0, 0, 0, 12, 0] ] 5 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 12, 0, 0, 0, 0, 12, 0] ] 6 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 12, 12, 0] ] 7 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 12, 0, 0, 0, 0, 12, 0] , [0, 0, 12, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 10 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 12, 0, 0, 0, 0, 12, 0] ]

### 13.1.3 Transition Removal

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

 4: −5 + 4⋅___const_5_0 − 4⋅k6_0 5: −7 + 4⋅___const_5_0 − 4⋅k6_0 6: −2 + 4⋅___const_5_0 − 4⋅k6_0 7: −4 + 4⋅___const_5_0 − 4⋅k6_0 8: −1 + 4⋅___const_5_0 − 4⋅k6_0 9: 1 + 4⋅___const_5_0 − 4⋅k6_0 4_var_snapshot: −6 + 4⋅___const_5_0 − 4⋅k6_0 4*: −4 + 4⋅___const_5_0 − 4⋅k6_0 6_var_snapshot: −3 + 4⋅___const_5_0 − 4⋅k6_0 6*: −1 + 4⋅___const_5_0 − 4⋅k6_0 9_var_snapshot: 4⋅___const_5_0 − 4⋅k6_0 9*: 2 + 4⋅___const_5_0 − 4⋅k6_0
Hints:
 32 lexWeak[ [0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0] ] 34 lexWeak[ [0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0] ] 39 lexWeak[ [0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0] ] 41 lexWeak[ [0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0] ] 46 lexWeak[ [0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0] ] 48 lexWeak[ [0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0] ] 2 lexWeak[ [0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0] ] 3 lexWeak[ [0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0] ] 4 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 4, 0] ] 5 lexStrict[ [0, 0, 0, 0, 4, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0] , [0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 6 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 4, 0] ] 10 lexWeak[ [0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0] ]

### 13.1.4 Transition Removal

We remove transitions 32, 34, 39, 41, 46, 48, 2, 3, 4, 6, 10 using the following ranking functions, which are bounded by −9.

 4: −7 5: −9 6: −3 7: −5 8: −1 9: 1 4_var_snapshot: −8 4*: −6 6_var_snapshot: −4 6*: −2 9_var_snapshot: 0 9*: 2
Hints:
 32 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] ] 34 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] ] 39 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] ] 41 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] ] 46 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] ] 48 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] ] 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] ] 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] ] 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] ] 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] ] 10 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] ]

### 13.1.5 Splitting Cut-Point Transitions

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

### 13.1.5.1 Cut-Point Subproblem 1/3

Here we consider cut-point transition 31.

### 13.1.5.1.1 Splitting Cut-Point Transitions

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

### 13.1.5.2 Cut-Point Subproblem 2/3

Here we consider cut-point transition 38.

### 13.1.5.2.1 Splitting Cut-Point Transitions

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

### 13.1.5.3 Cut-Point Subproblem 3/3

Here we consider cut-point transition 45.

### 13.1.5.3.1 Splitting Cut-Point Transitions

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

### 13.2 SCC Subproblem 2/2

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

### 13.2.1 Transition Removal

We remove transition 14 using the following ranking functions, which are bounded by −1.

 0: 2 + 9⋅___const_5_0 − 9⋅i4_0 1: 9⋅___const_5_0 − 9⋅i4_0 2: −6 + 9⋅___const_5_0 − 9⋅i4_0 3: −6 + 9⋅___const_5_0 − 9⋅i4_0 0_var_snapshot: 1 + 9⋅___const_5_0 − 9⋅i4_0 0*: 3 + 9⋅___const_5_0 − 9⋅i4_0 2_var_snapshot: −6 + 9⋅___const_5_0 − 9⋅i4_0 2*: −6 + 9⋅___const_5_0 − 9⋅i4_0
Hints:
 18 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 9, 9, 0] ] 20 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 9, 9, 0] ] 25 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 9, 9, 0] ] 27 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 9, 9, 0] ] 0 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 9, 9, 0] ] 1 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 9, 9, 0] ] 11 lexWeak[ [0, 0, 0, 0, 9, 0, 9, 0, 0, 0, 0, 0, 0, 0, 0, 9, 0] ] 12 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 9, 9, 0] ] 14 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 9, 9, 0] , [0, 0, 9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 13.2.2 Transition Removal

We remove transition 12 using the following ranking functions, which are bounded by −1.

 0: −2 + 3⋅___const_5_0 − 3⋅j5_0 1: −4 + 3⋅___const_5_0 − 3⋅j5_0 2: 1 + 3⋅___const_5_0 − 3⋅j5_0 3: 3⋅___const_5_0 − 3⋅j5_0 0_var_snapshot: −3 + 3⋅___const_5_0 − 3⋅j5_0 0*: −1 + 3⋅___const_5_0 − 3⋅j5_0 2_var_snapshot: 3⋅___const_5_0 − 3⋅j5_0 2*: 2 + 3⋅___const_5_0 − 3⋅j5_0
Hints:
 18 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 3, 0] ] 20 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 3, 0] ] 25 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 3, 0] ] 27 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 3, 0] ] 0 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 3, 0] ] 1 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 3, 0] ] 11 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 3, 0] ] 12 lexStrict[ [0, 0, 0, 0, 3, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0] , [0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 13.2.3 Transition Removal

We remove transitions 18, 20, 25, 27, 0, 11 using the following ranking functions, which are bounded by −3.

 0: −1 1: −3 2: 3 3: 1 0_var_snapshot: −2 0*: 0 2_var_snapshot: 2 2*: 4
Hints:
 18 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] ] 20 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] ] 25 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] ] 27 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 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] ] 1 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 11 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] ]

### 13.2.4 Transition Removal

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

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

### 13.2.5 Splitting Cut-Point Transitions

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

### 13.2.5.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 17.

### 13.2.5.1.1 Splitting Cut-Point Transitions

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

### 13.2.5.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 24.

### 13.2.5.2.1 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0