# LTS Termination Proof

by T2Cert

## Input

Integer Transition System
• Initial Location: 12

## Proof

The following invariants are asserted.

 0: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 1: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 2: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ − l_287_0 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 ∧ − l_1519_0 ≤ 0 3: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 4: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 ∧ j_36_post ≤ 0 ∧ − j_36_post ≤ 0 ∧ j_39_post ≤ 0 ∧ j_36_0 ≤ 0 ∧ − j_36_0 ≤ 0 ∧ j_39_0 ≤ 0 5: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ − l_287_0 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 ∧ j_36_post ≤ 0 ∧ − j_36_post ≤ 0 ∧ j_39_post ≤ 0 ∧ j_36_0 ≤ 0 ∧ − j_36_0 ≤ 0 ∧ j_39_0 ≤ 0 ∧ − j_39_0 ≤ 0 ∧ − l_1429_0 ≤ 0 6: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 ∧ j_36_post ≤ 0 ∧ − j_36_post ≤ 0 ∧ j_39_post ≤ 0 ∧ j_36_0 ≤ 0 ∧ − j_36_0 ≤ 0 ∧ j_39_0 ≤ 0 ∧ − j_39_0 ≤ 0 7: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ − l_287_0 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 ∧ j_36_post ≤ 0 ∧ − j_36_post ≤ 0 ∧ j_39_post ≤ 0 ∧ j_36_0 ≤ 0 ∧ − j_36_0 ≤ 0 ∧ j_39_0 ≤ 0 ∧ − j_39_0 ≤ 0 ∧ − l_855_0 ≤ 0 8: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 ∧ j_36_post ≤ 0 ∧ − j_36_post ≤ 0 ∧ j_39_post ≤ 0 ∧ j_36_0 ≤ 0 ∧ − j_36_0 ≤ 0 ∧ j_39_0 ≤ 0 ∧ − j_39_0 ≤ 0 9: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 10: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 11: TRUE 12: TRUE

The invariants are proved as follows.

### IMPACT Invariant Proof

• nodes (location) invariant:  0 (0) h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 1 (1) h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 2 (2) h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ − l_287_0 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 ∧ − l_1519_0 ≤ 0 3 (3) h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 4 (4) h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 ∧ j_36_post ≤ 0 ∧ − j_36_post ≤ 0 ∧ j_39_post ≤ 0 ∧ j_36_0 ≤ 0 ∧ − j_36_0 ≤ 0 ∧ j_39_0 ≤ 0 5 (5) h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ − l_287_0 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 ∧ j_36_post ≤ 0 ∧ − j_36_post ≤ 0 ∧ j_39_post ≤ 0 ∧ j_36_0 ≤ 0 ∧ − j_36_0 ≤ 0 ∧ j_39_0 ≤ 0 ∧ − j_39_0 ≤ 0 ∧ − l_1429_0 ≤ 0 6 (6) h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 ∧ j_36_post ≤ 0 ∧ − j_36_post ≤ 0 ∧ j_39_post ≤ 0 ∧ j_36_0 ≤ 0 ∧ − j_36_0 ≤ 0 ∧ j_39_0 ≤ 0 ∧ − j_39_0 ≤ 0 7 (7) h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ − l_287_0 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 ∧ j_36_post ≤ 0 ∧ − j_36_post ≤ 0 ∧ j_39_post ≤ 0 ∧ j_36_0 ≤ 0 ∧ − j_36_0 ≤ 0 ∧ j_39_0 ≤ 0 ∧ − j_39_0 ≤ 0 ∧ − l_855_0 ≤ 0 8 (8) h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 ∧ j_36_post ≤ 0 ∧ − j_36_post ≤ 0 ∧ j_39_post ≤ 0 ∧ j_36_0 ≤ 0 ∧ − j_36_0 ≤ 0 ∧ j_39_0 ≤ 0 ∧ − j_39_0 ≤ 0 9 (9) h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 10 (10) h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 11 (11) TRUE 12 (12) TRUE
• initial node: 12
• cover edges:
• transition edges:  0 0 1 1 1 2 1 2 2 2 3 3 3 4 4 3 11 9 4 5 5 4 6 5 5 7 6 6 8 7 6 9 7 7 10 8 9 12 10 9 13 10 10 14 0 11 15 0 12 16 11

### 2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 0 17 0: − tp_44_post + tp_44_post ≤ 0 ∧ tp_44_post − tp_44_post ≤ 0 ∧ − tp_44_3 + tp_44_3 ≤ 0 ∧ tp_44_3 − tp_44_3 ≤ 0 ∧ − tp_44_2 + tp_44_2 ≤ 0 ∧ tp_44_2 − tp_44_2 ≤ 0 ∧ − tp_44_1 + tp_44_1 ≤ 0 ∧ tp_44_1 − tp_44_1 ≤ 0 ∧ − tp_44_0 + tp_44_0 ≤ 0 ∧ tp_44_0 − tp_44_0 ≤ 0 ∧ − tp_32_post + tp_32_post ≤ 0 ∧ tp_32_post − tp_32_post ≤ 0 ∧ − tp_32_2 + tp_32_2 ≤ 0 ∧ tp_32_2 − tp_32_2 ≤ 0 ∧ − tp_32_1 + tp_32_1 ≤ 0 ∧ tp_32_1 − tp_32_1 ≤ 0 ∧ − tp_32_0 + tp_32_0 ≤ 0 ∧ tp_32_0 − tp_32_0 ≤ 0 ∧ − tp_30_post + tp_30_post ≤ 0 ∧ tp_30_post − tp_30_post ≤ 0 ∧ − tp_30_1 + tp_30_1 ≤ 0 ∧ tp_30_1 − tp_30_1 ≤ 0 ∧ − tp_30_0 + tp_30_0 ≤ 0 ∧ tp_30_0 − tp_30_0 ≤ 0 ∧ − tp_19_0 + tp_19_0 ≤ 0 ∧ tp_19_0 − tp_19_0 ≤ 0 ∧ − t_45_post + t_45_post ≤ 0 ∧ t_45_post − t_45_post ≤ 0 ∧ − t_45_1 + t_45_1 ≤ 0 ∧ t_45_1 − t_45_1 ≤ 0 ∧ − t_45_0 + t_45_0 ≤ 0 ∧ t_45_0 − t_45_0 ≤ 0 ∧ − t_40_post + t_40_post ≤ 0 ∧ t_40_post − t_40_post ≤ 0 ∧ − t_40_0 + t_40_0 ≤ 0 ∧ t_40_0 − t_40_0 ≤ 0 ∧ − t_38_post + t_38_post ≤ 0 ∧ t_38_post − t_38_post ≤ 0 ∧ − t_38_0 + t_38_0 ≤ 0 ∧ t_38_0 − t_38_0 ≤ 0 ∧ − t_35_post + t_35_post ≤ 0 ∧ t_35_post − t_35_post ≤ 0 ∧ − t_35_2 + t_35_2 ≤ 0 ∧ t_35_2 − t_35_2 ≤ 0 ∧ − t_35_1 + t_35_1 ≤ 0 ∧ t_35_1 − t_35_1 ≤ 0 ∧ − t_35_0 + t_35_0 ≤ 0 ∧ t_35_0 − t_35_0 ≤ 0 ∧ − t_14_0 + t_14_0 ≤ 0 ∧ t_14_0 − t_14_0 ≤ 0 ∧ − t_1303_post + t_1303_post ≤ 0 ∧ t_1303_post − t_1303_post ≤ 0 ∧ − t_1303_0 + t_1303_0 ≤ 0 ∧ t_1303_0 − t_1303_0 ≤ 0 ∧ − t_1057_post + t_1057_post ≤ 0 ∧ t_1057_post − t_1057_post ≤ 0 ∧ − t_1057_0 + t_1057_0 ≤ 0 ∧ t_1057_0 − t_1057_0 ≤ 0 ∧ − sCALLSITERETURN_43_post + sCALLSITERETURN_43_post ≤ 0 ∧ sCALLSITERETURN_43_post − sCALLSITERETURN_43_post ≤ 0 ∧ − sCALLSITERETURN_43_1 + sCALLSITERETURN_43_1 ≤ 0 ∧ sCALLSITERETURN_43_1 − sCALLSITERETURN_43_1 ≤ 0 ∧ − sCALLSITERETURN_43_0 + sCALLSITERETURN_43_0 ≤ 0 ∧ sCALLSITERETURN_43_0 − sCALLSITERETURN_43_0 ≤ 0 ∧ − sCALLSITERETURN_33_post + sCALLSITERETURN_33_post ≤ 0 ∧ sCALLSITERETURN_33_post − sCALLSITERETURN_33_post ≤ 0 ∧ − sCALLSITERETURN_33_2 + sCALLSITERETURN_33_2 ≤ 0 ∧ sCALLSITERETURN_33_2 − sCALLSITERETURN_33_2 ≤ 0 ∧ − sCALLSITERETURN_33_1 + sCALLSITERETURN_33_1 ≤ 0 ∧ sCALLSITERETURN_33_1 − sCALLSITERETURN_33_1 ≤ 0 ∧ − sCALLSITERETURN_33_0 + sCALLSITERETURN_33_0 ≤ 0 ∧ sCALLSITERETURN_33_0 − sCALLSITERETURN_33_0 ≤ 0 ∧ − sCALLSITERETURN_29_post + sCALLSITERETURN_29_post ≤ 0 ∧ sCALLSITERETURN_29_post − sCALLSITERETURN_29_post ≤ 0 ∧ − sCALLSITERETURN_29_0 + sCALLSITERETURN_29_0 ≤ 0 ∧ sCALLSITERETURN_29_0 − sCALLSITERETURN_29_0 ≤ 0 ∧ − sCALLSITERETURN_16_0 + sCALLSITERETURN_16_0 ≤ 0 ∧ sCALLSITERETURN_16_0 − sCALLSITERETURN_16_0 ≤ 0 ∧ − nd_7_post + nd_7_post ≤ 0 ∧ nd_7_post − nd_7_post ≤ 0 ∧ − nd_7_1 + nd_7_1 ≤ 0 ∧ nd_7_1 − nd_7_1 ≤ 0 ∧ − nd_7_0 + nd_7_0 ≤ 0 ∧ nd_7_0 − nd_7_0 ≤ 0 ∧ − mt_20_post + mt_20_post ≤ 0 ∧ mt_20_post − mt_20_post ≤ 0 ∧ − mt_20_0 + mt_20_0 ≤ 0 ∧ mt_20_0 − mt_20_0 ≤ 0 ∧ − mt_18_post + mt_18_post ≤ 0 ∧ mt_18_post − mt_18_post ≤ 0 ∧ − mt_18_1 + mt_18_1 ≤ 0 ∧ mt_18_1 − mt_18_1 ≤ 0 ∧ − mt_18_0 + mt_18_0 ≤ 0 ∧ mt_18_0 − mt_18_0 ≤ 0 ∧ − lt_17_post + lt_17_post ≤ 0 ∧ lt_17_post − lt_17_post ≤ 0 ∧ − lt_17_1 + lt_17_1 ≤ 0 ∧ lt_17_1 − lt_17_1 ≤ 0 ∧ − lt_17_0 + lt_17_0 ≤ 0 ∧ lt_17_0 − lt_17_0 ≤ 0 ∧ − lt_1256_post + lt_1256_post ≤ 0 ∧ lt_1256_post − lt_1256_post ≤ 0 ∧ − lt_1256_0 + lt_1256_0 ≤ 0 ∧ lt_1256_0 − lt_1256_0 ≤ 0 ∧ − lt_10_post + lt_10_post ≤ 0 ∧ lt_10_post − lt_10_post ≤ 0 ∧ − lt_10_1 + lt_10_1 ≤ 0 ∧ lt_10_1 − lt_10_1 ≤ 0 ∧ − lt_10_0 + lt_10_0 ≤ 0 ∧ lt_10_0 − lt_10_0 ≤ 0 ∧ − l_855_post + l_855_post ≤ 0 ∧ l_855_post − l_855_post ≤ 0 ∧ − l_855_0 + l_855_0 ≤ 0 ∧ l_855_0 − l_855_0 ≤ 0 ∧ − l_287_post + l_287_post ≤ 0 ∧ l_287_post − l_287_post ≤ 0 ∧ − l_287_0 + l_287_0 ≤ 0 ∧ l_287_0 − l_287_0 ≤ 0 ∧ − l_27_post + l_27_post ≤ 0 ∧ l_27_post − l_27_post ≤ 0 ∧ − l_27_0 + l_27_0 ≤ 0 ∧ l_27_0 − l_27_0 ≤ 0 ∧ − l_1519_post + l_1519_post ≤ 0 ∧ l_1519_post − l_1519_post ≤ 0 ∧ − l_1519_0 + l_1519_0 ≤ 0 ∧ l_1519_0 − l_1519_0 ≤ 0 ∧ − l_1429_post + l_1429_post ≤ 0 ∧ l_1429_post − l_1429_post ≤ 0 ∧ − l_1429_0 + l_1429_0 ≤ 0 ∧ l_1429_0 − l_1429_0 ≤ 0 ∧ − l_1304_post + l_1304_post ≤ 0 ∧ l_1304_post − l_1304_post ≤ 0 ∧ − l_1304_0 + l_1304_0 ≤ 0 ∧ l_1304_0 − l_1304_0 ≤ 0 ∧ − l_1119_post + l_1119_post ≤ 0 ∧ l_1119_post − l_1119_post ≤ 0 ∧ − l_1119_1 + l_1119_1 ≤ 0 ∧ l_1119_1 − l_1119_1 ≤ 0 ∧ − l_1119_0 + l_1119_0 ≤ 0 ∧ l_1119_0 − l_1119_0 ≤ 0 ∧ − j_39_post + j_39_post ≤ 0 ∧ j_39_post − j_39_post ≤ 0 ∧ − j_39_0 + j_39_0 ≤ 0 ∧ j_39_0 − j_39_0 ≤ 0 ∧ − j_36_post + j_36_post ≤ 0 ∧ j_36_post − j_36_post ≤ 0 ∧ − j_36_0 + j_36_0 ≤ 0 ∧ j_36_0 − j_36_0 ≤ 0 ∧ − i_31_post + i_31_post ≤ 0 ∧ i_31_post − i_31_post ≤ 0 ∧ − i_31_0 + i_31_0 ≤ 0 ∧ i_31_0 − i_31_0 ≤ 0 ∧ − h_46_post + h_46_post ≤ 0 ∧ h_46_post − h_46_post ≤ 0 ∧ − h_46_1 + h_46_1 ≤ 0 ∧ h_46_1 − h_46_1 ≤ 0 ∧ − h_46_0 + h_46_0 ≤ 0 ∧ h_46_0 − h_46_0 ≤ 0 ∧ − h_37_post + h_37_post ≤ 0 ∧ h_37_post − h_37_post ≤ 0 ∧ − h_37_0 + h_37_0 ≤ 0 ∧ h_37_0 − h_37_0 ≤ 0 ∧ − h_34_post + h_34_post ≤ 0 ∧ h_34_post − h_34_post ≤ 0 ∧ − h_34_2 + h_34_2 ≤ 0 ∧ h_34_2 − h_34_2 ≤ 0 ∧ − h_34_1 + h_34_1 ≤ 0 ∧ h_34_1 − h_34_1 ≤ 0 ∧ − h_34_0 + h_34_0 ≤ 0 ∧ h_34_0 − h_34_0 ≤ 0 ∧ − h_28_post + h_28_post ≤ 0 ∧ h_28_post − h_28_post ≤ 0 ∧ − h_28_0 + h_28_0 ≤ 0 ∧ h_28_0 − h_28_0 ≤ 0 ∧ − f_1323_post + f_1323_post ≤ 0 ∧ f_1323_post − f_1323_post ≤ 0 ∧ − f_1323_0 + f_1323_0 ≤ 0 ∧ f_1323_0 − f_1323_0 ≤ 0 ∧ − fF_1324_post + fF_1324_post ≤ 0 ∧ fF_1324_post − fF_1324_post ≤ 0 ∧ − fF_1324_0 + fF_1324_0 ≤ 0 ∧ fF_1324_0 − fF_1324_0 ≤ 0 ∧ − c_990_post + c_990_post ≤ 0 ∧ c_990_post − c_990_post ≤ 0 ∧ − c_990_0 + c_990_0 ≤ 0 ∧ c_990_0 − c_990_0 ≤ 0 ∧ − c_98_post + c_98_post ≤ 0 ∧ c_98_post − c_98_post ≤ 0 ∧ − c_98_1 + c_98_1 ≤ 0 ∧ c_98_1 − c_98_1 ≤ 0 ∧ − c_98_0 + c_98_0 ≤ 0 ∧ c_98_0 − c_98_0 ≤ 0 ∧ − c_958_post + c_958_post ≤ 0 ∧ c_958_post − c_958_post ≤ 0 ∧ − c_958_1 + c_958_1 ≤ 0 ∧ c_958_1 − c_958_1 ≤ 0 ∧ − c_958_0 + c_958_0 ≤ 0 ∧ c_958_0 − c_958_0 ≤ 0 ∧ − c_901_post + c_901_post ≤ 0 ∧ c_901_post − c_901_post ≤ 0 ∧ − c_901_0 + c_901_0 ≤ 0 ∧ c_901_0 − c_901_0 ≤ 0 ∧ − c_1481_post + c_1481_post ≤ 0 ∧ c_1481_post − c_1481_post ≤ 0 ∧ − c_1481_1 + c_1481_1 ≤ 0 ∧ c_1481_1 − c_1481_1 ≤ 0 ∧ − c_1481_0 + c_1481_0 ≤ 0 ∧ c_1481_0 − c_1481_0 ≤ 0 ∧ − c_1186_post + c_1186_post ≤ 0 ∧ c_1186_post − c_1186_post ≤ 0 ∧ − c_1186_0 + c_1186_0 ≤ 0 ∧ c_1186_0 − c_1186_0 ≤ 0 ∧ − Flink_0 + Flink_0 ≤ 0 ∧ Flink_0 − Flink_0 ≤ 0
and for every transition t, a duplicate t is considered.

### 3 Transition Removal

We remove transitions 4, 5, 6, 7, 8, 9, 10, 15, 16 using the following ranking functions, which are bounded by −21.

 12: 0 11: 0 0: 0 1: 0 2: 0 3: 0 9: 0 10: 0 4: 0 5: 0 6: 0 7: 0 8: 0 12: −9 11: −10 0: −11 1: −11 2: −11 3: −11 9: −11 10: −11 0_var_snapshot: −11 0*: −11 4: −12 5: −13 6: −14 7: −15 8: −16

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

0* 20 0: tp_44_post + tp_44_post ≤ 0tp_44_posttp_44_post ≤ 0tp_44_3 + tp_44_3 ≤ 0tp_44_3tp_44_3 ≤ 0tp_44_2 + tp_44_2 ≤ 0tp_44_2tp_44_2 ≤ 0tp_44_1 + tp_44_1 ≤ 0tp_44_1tp_44_1 ≤ 0tp_44_0 + tp_44_0 ≤ 0tp_44_0tp_44_0 ≤ 0tp_32_post + tp_32_post ≤ 0tp_32_posttp_32_post ≤ 0tp_32_2 + tp_32_2 ≤ 0tp_32_2tp_32_2 ≤ 0tp_32_1 + tp_32_1 ≤ 0tp_32_1tp_32_1 ≤ 0tp_32_0 + tp_32_0 ≤ 0tp_32_0tp_32_0 ≤ 0tp_30_post + tp_30_post ≤ 0tp_30_posttp_30_post ≤ 0tp_30_1 + tp_30_1 ≤ 0tp_30_1tp_30_1 ≤ 0tp_30_0 + tp_30_0 ≤ 0tp_30_0tp_30_0 ≤ 0tp_19_0 + tp_19_0 ≤ 0tp_19_0tp_19_0 ≤ 0t_45_post + t_45_post ≤ 0t_45_postt_45_post ≤ 0t_45_1 + t_45_1 ≤ 0t_45_1t_45_1 ≤ 0t_45_0 + t_45_0 ≤ 0t_45_0t_45_0 ≤ 0t_40_post + t_40_post ≤ 0t_40_postt_40_post ≤ 0t_40_0 + t_40_0 ≤ 0t_40_0t_40_0 ≤ 0t_38_post + t_38_post ≤ 0t_38_postt_38_post ≤ 0t_38_0 + t_38_0 ≤ 0t_38_0t_38_0 ≤ 0t_35_post + t_35_post ≤ 0t_35_postt_35_post ≤ 0t_35_2 + t_35_2 ≤ 0t_35_2t_35_2 ≤ 0t_35_1 + t_35_1 ≤ 0t_35_1t_35_1 ≤ 0t_35_0 + t_35_0 ≤ 0t_35_0t_35_0 ≤ 0t_14_0 + t_14_0 ≤ 0t_14_0t_14_0 ≤ 0t_1303_post + t_1303_post ≤ 0t_1303_postt_1303_post ≤ 0t_1303_0 + t_1303_0 ≤ 0t_1303_0t_1303_0 ≤ 0t_1057_post + t_1057_post ≤ 0t_1057_postt_1057_post ≤ 0t_1057_0 + t_1057_0 ≤ 0t_1057_0t_1057_0 ≤ 0sCALLSITERETURN_43_post + sCALLSITERETURN_43_post ≤ 0sCALLSITERETURN_43_postsCALLSITERETURN_43_post ≤ 0sCALLSITERETURN_43_1 + sCALLSITERETURN_43_1 ≤ 0sCALLSITERETURN_43_1sCALLSITERETURN_43_1 ≤ 0sCALLSITERETURN_43_0 + sCALLSITERETURN_43_0 ≤ 0sCALLSITERETURN_43_0sCALLSITERETURN_43_0 ≤ 0sCALLSITERETURN_33_post + sCALLSITERETURN_33_post ≤ 0sCALLSITERETURN_33_postsCALLSITERETURN_33_post ≤ 0sCALLSITERETURN_33_2 + sCALLSITERETURN_33_2 ≤ 0sCALLSITERETURN_33_2sCALLSITERETURN_33_2 ≤ 0sCALLSITERETURN_33_1 + sCALLSITERETURN_33_1 ≤ 0sCALLSITERETURN_33_1sCALLSITERETURN_33_1 ≤ 0sCALLSITERETURN_33_0 + sCALLSITERETURN_33_0 ≤ 0sCALLSITERETURN_33_0sCALLSITERETURN_33_0 ≤ 0sCALLSITERETURN_29_post + sCALLSITERETURN_29_post ≤ 0sCALLSITERETURN_29_postsCALLSITERETURN_29_post ≤ 0sCALLSITERETURN_29_0 + sCALLSITERETURN_29_0 ≤ 0sCALLSITERETURN_29_0sCALLSITERETURN_29_0 ≤ 0sCALLSITERETURN_16_0 + sCALLSITERETURN_16_0 ≤ 0sCALLSITERETURN_16_0sCALLSITERETURN_16_0 ≤ 0nd_7_post + nd_7_post ≤ 0nd_7_postnd_7_post ≤ 0nd_7_1 + nd_7_1 ≤ 0nd_7_1nd_7_1 ≤ 0nd_7_0 + nd_7_0 ≤ 0nd_7_0nd_7_0 ≤ 0mt_20_post + mt_20_post ≤ 0mt_20_postmt_20_post ≤ 0mt_20_0 + mt_20_0 ≤ 0mt_20_0mt_20_0 ≤ 0mt_18_post + mt_18_post ≤ 0mt_18_postmt_18_post ≤ 0mt_18_1 + mt_18_1 ≤ 0mt_18_1mt_18_1 ≤ 0mt_18_0 + mt_18_0 ≤ 0mt_18_0mt_18_0 ≤ 0lt_17_post + lt_17_post ≤ 0lt_17_postlt_17_post ≤ 0lt_17_1 + lt_17_1 ≤ 0lt_17_1lt_17_1 ≤ 0lt_17_0 + lt_17_0 ≤ 0lt_17_0lt_17_0 ≤ 0lt_1256_post + lt_1256_post ≤ 0lt_1256_postlt_1256_post ≤ 0lt_1256_0 + lt_1256_0 ≤ 0lt_1256_0lt_1256_0 ≤ 0lt_10_post + lt_10_post ≤ 0lt_10_postlt_10_post ≤ 0lt_10_1 + lt_10_1 ≤ 0lt_10_1lt_10_1 ≤ 0lt_10_0 + lt_10_0 ≤ 0lt_10_0lt_10_0 ≤ 0l_855_post + l_855_post ≤ 0l_855_postl_855_post ≤ 0l_855_0 + l_855_0 ≤ 0l_855_0l_855_0 ≤ 0l_287_post + l_287_post ≤ 0l_287_postl_287_post ≤ 0l_287_0 + l_287_0 ≤ 0l_287_0l_287_0 ≤ 0l_27_post + l_27_post ≤ 0l_27_postl_27_post ≤ 0l_27_0 + l_27_0 ≤ 0l_27_0l_27_0 ≤ 0l_1519_post + l_1519_post ≤ 0l_1519_postl_1519_post ≤ 0l_1519_0 + l_1519_0 ≤ 0l_1519_0l_1519_0 ≤ 0l_1429_post + l_1429_post ≤ 0l_1429_postl_1429_post ≤ 0l_1429_0 + l_1429_0 ≤ 0l_1429_0l_1429_0 ≤ 0l_1304_post + l_1304_post ≤ 0l_1304_postl_1304_post ≤ 0l_1304_0 + l_1304_0 ≤ 0l_1304_0l_1304_0 ≤ 0l_1119_post + l_1119_post ≤ 0l_1119_postl_1119_post ≤ 0l_1119_1 + l_1119_1 ≤ 0l_1119_1l_1119_1 ≤ 0l_1119_0 + l_1119_0 ≤ 0l_1119_0l_1119_0 ≤ 0j_39_post + j_39_post ≤ 0j_39_postj_39_post ≤ 0j_39_0 + j_39_0 ≤ 0j_39_0j_39_0 ≤ 0j_36_post + j_36_post ≤ 0j_36_postj_36_post ≤ 0j_36_0 + j_36_0 ≤ 0j_36_0j_36_0 ≤ 0i_31_post + i_31_post ≤ 0i_31_posti_31_post ≤ 0i_31_0 + i_31_0 ≤ 0i_31_0i_31_0 ≤ 0h_46_post + h_46_post ≤ 0h_46_posth_46_post ≤ 0h_46_1 + h_46_1 ≤ 0h_46_1h_46_1 ≤ 0h_46_0 + h_46_0 ≤ 0h_46_0h_46_0 ≤ 0h_37_post + h_37_post ≤ 0h_37_posth_37_post ≤ 0h_37_0 + h_37_0 ≤ 0h_37_0h_37_0 ≤ 0h_34_post + h_34_post ≤ 0h_34_posth_34_post ≤ 0h_34_2 + h_34_2 ≤ 0h_34_2h_34_2 ≤ 0h_34_1 + h_34_1 ≤ 0h_34_1h_34_1 ≤ 0h_34_0 + h_34_0 ≤ 0h_34_0h_34_0 ≤ 0h_28_post + h_28_post ≤ 0h_28_posth_28_post ≤ 0h_28_0 + h_28_0 ≤ 0h_28_0h_28_0 ≤ 0f_1323_post + f_1323_post ≤ 0f_1323_postf_1323_post ≤ 0f_1323_0 + f_1323_0 ≤ 0f_1323_0f_1323_0 ≤ 0fF_1324_post + fF_1324_post ≤ 0fF_1324_postfF_1324_post ≤ 0fF_1324_0 + fF_1324_0 ≤ 0fF_1324_0fF_1324_0 ≤ 0c_990_post + c_990_post ≤ 0c_990_postc_990_post ≤ 0c_990_0 + c_990_0 ≤ 0c_990_0c_990_0 ≤ 0c_98_post + c_98_post ≤ 0c_98_postc_98_post ≤ 0c_98_1 + c_98_1 ≤ 0c_98_1c_98_1 ≤ 0c_98_0 + c_98_0 ≤ 0c_98_0c_98_0 ≤ 0c_958_post + c_958_post ≤ 0c_958_postc_958_post ≤ 0c_958_1 + c_958_1 ≤ 0c_958_1c_958_1 ≤ 0c_958_0 + c_958_0 ≤ 0c_958_0c_958_0 ≤ 0c_901_post + c_901_post ≤ 0c_901_postc_901_post ≤ 0c_901_0 + c_901_0 ≤ 0c_901_0c_901_0 ≤ 0c_1481_post + c_1481_post ≤ 0c_1481_postc_1481_post ≤ 0c_1481_1 + c_1481_1 ≤ 0c_1481_1c_1481_1 ≤ 0c_1481_0 + c_1481_0 ≤ 0c_1481_0c_1481_0 ≤ 0c_1186_post + c_1186_post ≤ 0c_1186_postc_1186_post ≤ 0c_1186_0 + c_1186_0 ≤ 0c_1186_0c_1186_0 ≤ 0Flink_0 + Flink_0 ≤ 0Flink_0Flink_0 ≤ 0

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

0 18 0_var_snapshot: tp_44_post + tp_44_post ≤ 0tp_44_posttp_44_post ≤ 0tp_44_3 + tp_44_3 ≤ 0tp_44_3tp_44_3 ≤ 0tp_44_2 + tp_44_2 ≤ 0tp_44_2tp_44_2 ≤ 0tp_44_1 + tp_44_1 ≤ 0tp_44_1tp_44_1 ≤ 0tp_44_0 + tp_44_0 ≤ 0tp_44_0tp_44_0 ≤ 0tp_32_post + tp_32_post ≤ 0tp_32_posttp_32_post ≤ 0tp_32_2 + tp_32_2 ≤ 0tp_32_2tp_32_2 ≤ 0tp_32_1 + tp_32_1 ≤ 0tp_32_1tp_32_1 ≤ 0tp_32_0 + tp_32_0 ≤ 0tp_32_0tp_32_0 ≤ 0tp_30_post + tp_30_post ≤ 0tp_30_posttp_30_post ≤ 0tp_30_1 + tp_30_1 ≤ 0tp_30_1tp_30_1 ≤ 0tp_30_0 + tp_30_0 ≤ 0tp_30_0tp_30_0 ≤ 0tp_19_0 + tp_19_0 ≤ 0tp_19_0tp_19_0 ≤ 0t_45_post + t_45_post ≤ 0t_45_postt_45_post ≤ 0t_45_1 + t_45_1 ≤ 0t_45_1t_45_1 ≤ 0t_45_0 + t_45_0 ≤ 0t_45_0t_45_0 ≤ 0t_40_post + t_40_post ≤ 0t_40_postt_40_post ≤ 0t_40_0 + t_40_0 ≤ 0t_40_0t_40_0 ≤ 0t_38_post + t_38_post ≤ 0t_38_postt_38_post ≤ 0t_38_0 + t_38_0 ≤ 0t_38_0t_38_0 ≤ 0t_35_post + t_35_post ≤ 0t_35_postt_35_post ≤ 0t_35_2 + t_35_2 ≤ 0t_35_2t_35_2 ≤ 0t_35_1 + t_35_1 ≤ 0t_35_1t_35_1 ≤ 0t_35_0 + t_35_0 ≤ 0t_35_0t_35_0 ≤ 0t_14_0 + t_14_0 ≤ 0t_14_0t_14_0 ≤ 0t_1303_post + t_1303_post ≤ 0t_1303_postt_1303_post ≤ 0t_1303_0 + t_1303_0 ≤ 0t_1303_0t_1303_0 ≤ 0t_1057_post + t_1057_post ≤ 0t_1057_postt_1057_post ≤ 0t_1057_0 + t_1057_0 ≤ 0t_1057_0t_1057_0 ≤ 0sCALLSITERETURN_43_post + sCALLSITERETURN_43_post ≤ 0sCALLSITERETURN_43_postsCALLSITERETURN_43_post ≤ 0sCALLSITERETURN_43_1 + sCALLSITERETURN_43_1 ≤ 0sCALLSITERETURN_43_1sCALLSITERETURN_43_1 ≤ 0sCALLSITERETURN_43_0 + sCALLSITERETURN_43_0 ≤ 0sCALLSITERETURN_43_0sCALLSITERETURN_43_0 ≤ 0sCALLSITERETURN_33_post + sCALLSITERETURN_33_post ≤ 0sCALLSITERETURN_33_postsCALLSITERETURN_33_post ≤ 0sCALLSITERETURN_33_2 + sCALLSITERETURN_33_2 ≤ 0sCALLSITERETURN_33_2sCALLSITERETURN_33_2 ≤ 0sCALLSITERETURN_33_1 + sCALLSITERETURN_33_1 ≤ 0sCALLSITERETURN_33_1sCALLSITERETURN_33_1 ≤ 0sCALLSITERETURN_33_0 + sCALLSITERETURN_33_0 ≤ 0sCALLSITERETURN_33_0sCALLSITERETURN_33_0 ≤ 0sCALLSITERETURN_29_post + sCALLSITERETURN_29_post ≤ 0sCALLSITERETURN_29_postsCALLSITERETURN_29_post ≤ 0sCALLSITERETURN_29_0 + sCALLSITERETURN_29_0 ≤ 0sCALLSITERETURN_29_0sCALLSITERETURN_29_0 ≤ 0sCALLSITERETURN_16_0 + sCALLSITERETURN_16_0 ≤ 0sCALLSITERETURN_16_0sCALLSITERETURN_16_0 ≤ 0nd_7_post + nd_7_post ≤ 0nd_7_postnd_7_post ≤ 0nd_7_1 + nd_7_1 ≤ 0nd_7_1nd_7_1 ≤ 0nd_7_0 + nd_7_0 ≤ 0nd_7_0nd_7_0 ≤ 0mt_20_post + mt_20_post ≤ 0mt_20_postmt_20_post ≤ 0mt_20_0 + mt_20_0 ≤ 0mt_20_0mt_20_0 ≤ 0mt_18_post + mt_18_post ≤ 0mt_18_postmt_18_post ≤ 0mt_18_1 + mt_18_1 ≤ 0mt_18_1mt_18_1 ≤ 0mt_18_0 + mt_18_0 ≤ 0mt_18_0mt_18_0 ≤ 0lt_17_post + lt_17_post ≤ 0lt_17_postlt_17_post ≤ 0lt_17_1 + lt_17_1 ≤ 0lt_17_1lt_17_1 ≤ 0lt_17_0 + lt_17_0 ≤ 0lt_17_0lt_17_0 ≤ 0lt_1256_post + lt_1256_post ≤ 0lt_1256_postlt_1256_post ≤ 0lt_1256_0 + lt_1256_0 ≤ 0lt_1256_0lt_1256_0 ≤ 0lt_10_post + lt_10_post ≤ 0lt_10_postlt_10_post ≤ 0lt_10_1 + lt_10_1 ≤ 0lt_10_1lt_10_1 ≤ 0lt_10_0 + lt_10_0 ≤ 0lt_10_0lt_10_0 ≤ 0l_855_post + l_855_post ≤ 0l_855_postl_855_post ≤ 0l_855_0 + l_855_0 ≤ 0l_855_0l_855_0 ≤ 0l_287_post + l_287_post ≤ 0l_287_postl_287_post ≤ 0l_287_0 + l_287_0 ≤ 0l_287_0l_287_0 ≤ 0l_27_post + l_27_post ≤ 0l_27_postl_27_post ≤ 0l_27_0 + l_27_0 ≤ 0l_27_0l_27_0 ≤ 0l_1519_post + l_1519_post ≤ 0l_1519_postl_1519_post ≤ 0l_1519_0 + l_1519_0 ≤ 0l_1519_0l_1519_0 ≤ 0l_1429_post + l_1429_post ≤ 0l_1429_postl_1429_post ≤ 0l_1429_0 + l_1429_0 ≤ 0l_1429_0l_1429_0 ≤ 0l_1304_post + l_1304_post ≤ 0l_1304_postl_1304_post ≤ 0l_1304_0 + l_1304_0 ≤ 0l_1304_0l_1304_0 ≤ 0l_1119_post + l_1119_post ≤ 0l_1119_postl_1119_post ≤ 0l_1119_1 + l_1119_1 ≤ 0l_1119_1l_1119_1 ≤ 0l_1119_0 + l_1119_0 ≤ 0l_1119_0l_1119_0 ≤ 0j_39_post + j_39_post ≤ 0j_39_postj_39_post ≤ 0j_39_0 + j_39_0 ≤ 0j_39_0j_39_0 ≤ 0j_36_post + j_36_post ≤ 0j_36_postj_36_post ≤ 0j_36_0 + j_36_0 ≤ 0j_36_0j_36_0 ≤ 0i_31_post + i_31_post ≤ 0i_31_posti_31_post ≤ 0i_31_0 + i_31_0 ≤ 0i_31_0i_31_0 ≤ 0h_46_post + h_46_post ≤ 0h_46_posth_46_post ≤ 0h_46_1 + h_46_1 ≤ 0h_46_1h_46_1 ≤ 0h_46_0 + h_46_0 ≤ 0h_46_0h_46_0 ≤ 0h_37_post + h_37_post ≤ 0h_37_posth_37_post ≤ 0h_37_0 + h_37_0 ≤ 0h_37_0h_37_0 ≤ 0h_34_post + h_34_post ≤ 0h_34_posth_34_post ≤ 0h_34_2 + h_34_2 ≤ 0h_34_2h_34_2 ≤ 0h_34_1 + h_34_1 ≤ 0h_34_1h_34_1 ≤ 0h_34_0 + h_34_0 ≤ 0h_34_0h_34_0 ≤ 0h_28_post + h_28_post ≤ 0h_28_posth_28_post ≤ 0h_28_0 + h_28_0 ≤ 0h_28_0h_28_0 ≤ 0f_1323_post + f_1323_post ≤ 0f_1323_postf_1323_post ≤ 0f_1323_0 + f_1323_0 ≤ 0f_1323_0f_1323_0 ≤ 0fF_1324_post + fF_1324_post ≤ 0fF_1324_postfF_1324_post ≤ 0fF_1324_0 + fF_1324_0 ≤ 0fF_1324_0fF_1324_0 ≤ 0c_990_post + c_990_post ≤ 0c_990_postc_990_post ≤ 0c_990_0 + c_990_0 ≤ 0c_990_0c_990_0 ≤ 0c_98_post + c_98_post ≤ 0c_98_postc_98_post ≤ 0c_98_1 + c_98_1 ≤ 0c_98_1c_98_1 ≤ 0c_98_0 + c_98_0 ≤ 0c_98_0c_98_0 ≤ 0c_958_post + c_958_post ≤ 0c_958_postc_958_post ≤ 0c_958_1 + c_958_1 ≤ 0c_958_1c_958_1 ≤ 0c_958_0 + c_958_0 ≤ 0c_958_0c_958_0 ≤ 0c_901_post + c_901_post ≤ 0c_901_postc_901_post ≤ 0c_901_0 + c_901_0 ≤ 0c_901_0c_901_0 ≤ 0c_1481_post + c_1481_post ≤ 0c_1481_postc_1481_post ≤ 0c_1481_1 + c_1481_1 ≤ 0c_1481_1c_1481_1 ≤ 0c_1481_0 + c_1481_0 ≤ 0c_1481_0c_1481_0 ≤ 0c_1186_post + c_1186_post ≤ 0c_1186_postc_1186_post ≤ 0c_1186_0 + c_1186_0 ≤ 0c_1186_0c_1186_0 ≤ 0Flink_0 + Flink_0 ≤ 0Flink_0Flink_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, 2, 3, 9, 10, 0_var_snapshot, 0* }.

### 6.1.1 Transition Removal

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

 0: 8⋅l_27_0 − 8⋅mt_18_0 1: 8⋅l_27_0 − 8⋅mt_18_0 − 2⋅mt_18_1 2: −3 + 8⋅l_27_0 − 8⋅lt_10_0 3: −4 + 8⋅l_27_0 − 8⋅lt_10_0 9: 3 + 8⋅l_27_0 − 8⋅lt_10_0 + 8⋅lt_17_0 − 8⋅mt_18_0 10: 8⋅l_27_0 − 8⋅mt_18_0 + 2⋅mt_18_1 0_var_snapshot: −1 + 8⋅l_27_0 − 8⋅mt_18_0 0*: −1 + 8⋅l_27_0 − 8⋅mt_18_0 + 2⋅mt_18_1

### 6.1.2 Transition Removal

We remove transitions 20, 0, 1, 2, 3, 14 using the following ranking functions, which are bounded by −2.

 0: −2 + l_27_0 + 3⋅l_27_post 1: 0 2: − mt_18_1 3: −2⋅mt_18_1 9: 0 10: l_27_0 + 3⋅l_27_post 0_var_snapshot: l_27_0 0*: −1 + l_27_0 + 3⋅l_27_post

### 6.1.3 Transition Removal

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

 0: mt_18_1 1: 0 2: 0 3: 0 9: 0 10: 0 0_var_snapshot: 0 0*: 0

### 6.1.4 Splitting Cut-Point Transitions

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

### 6.1.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 17.

### 6.1.4.1.1 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0