# LTS Termination Proof

by T2Cert

## Input

Integer Transition System
• Initial Location: 15
• Transitions: (pre-variables and post-variables)  0 0 1: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ Sorted5_post ≤ 0 ∧ − Sorted5_post ≤ 0 ∧ −1 + i8_post ≤ 0 ∧ 1 − i8_post ≤ 0 ∧ Sorted5_0 − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_post ≤ 0 ∧ i8_0 − i8_post ≤ 0 ∧ − i8_0 + i8_post ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0 0 1 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ −100 + Index2_0 ≤ 0 ∧ −1 − Index2_0 + Index2_post ≤ 0 ∧ 1 + Index2_0 − Index2_post ≤ 0 ∧ Index2_0 − Index2_post ≤ 0 ∧ − Index2_0 + Index2_post ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 2 2 0: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0 3 3 4: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0 5 4 3: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0 6 5 7: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0 7 6 1: 0 ≤ 0 ∧ 0 ≤ 0 ∧ Sorted5_0 ≤ 0 ∧ − Sorted5_0 ≤ 0 ∧ −1 − i8_0 + i8_post ≤ 0 ∧ 1 + i8_0 − i8_post ≤ 0 ∧ i8_0 − i8_post ≤ 0 ∧ − i8_0 + i8_post ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0 7 7 5: 1 − Sorted5_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0 7 8 5: 1 + Sorted5_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0 8 9 9: 0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − Index7_0 + Index7_post ≤ 0 ∧ 1 + Index7_0 − Index7_post ≤ 0 ∧ Index7_0 − Index7_post ≤ 0 ∧ − Index7_0 + Index7_post ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0 1 10 10: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0 11 11 8: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ Sorted5_post ≤ 0 ∧ − Sorted5_post ≤ 0 ∧ Sorted5_0 − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_post ≤ 0 ∧ Temp6_0 − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_post ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0 11 12 8: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0 12 13 11: −100 + Index7_0 + i8_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0 12 14 6: 101 − Index7_0 − i8_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0 13 15 6: 100 − Index7_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0 13 16 12: −99 + Index7_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0 9 17 13: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0 10 18 3: 100 − i8_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0 10 19 9: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −99 + i8_0 ≤ 0 ∧ −1 + Sorted5_post ≤ 0 ∧ 1 − Sorted5_post ≤ 0 ∧ −1 + Index7_post ≤ 0 ∧ 1 − Index7_post ≤ 0 ∧ Index7_0 − Index7_post ≤ 0 ∧ − Index7_0 + Index7_post ≤ 0 ∧ Sorted5_0 − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_post ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0 14 20 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ fact3_post − factor_post ≤ 0 ∧ − fact3_post + factor_post ≤ 0 ∧ −1 + Index2_post ≤ 0 ∧ 1 − Index2_post ≤ 0 ∧ Index2_0 − Index2_post ≤ 0 ∧ − Index2_0 + Index2_post ≤ 0 ∧ fact3_0 − fact3_post ≤ 0 ∧ − fact3_0 + fact3_post ≤ 0 ∧ factor_0 − factor_post ≤ 0 ∧ − factor_0 + factor_post ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 15 21 14: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0

## Proof

The following invariants are asserted.

 0: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 1: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 ∧ Sorted5_0 ≤ 0 ∧ − Sorted5_0 ≤ 0 2: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 3: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 4: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 5: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 6: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 7: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 8: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 9: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 10: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 ∧ Sorted5_0 ≤ 0 ∧ − Sorted5_0 ≤ 0 11: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 12: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 13: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 14: TRUE 15: TRUE

The invariants are proved as follows.

### IMPACT Invariant Proof

• nodes (location) invariant:  0 (0) 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 1 (1) 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 ∧ Sorted5_0 ≤ 0 ∧ − Sorted5_0 ≤ 0 2 (2) 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 3 (3) 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 4 (4) 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 5 (5) 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 6 (6) 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 7 (7) 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 8 (8) 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 9 (9) 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 10 (10) 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 ∧ Sorted5_0 ≤ 0 ∧ − Sorted5_0 ≤ 0 11 (11) 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 12 (12) 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 13 (13) 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 14 (14) TRUE 15 (15) TRUE
• initial node: 15
• cover edges:
• transition edges:  0 0 1 0 1 2 1 10 10 2 2 0 3 3 4 5 4 3 6 5 7 7 6 1 7 7 5 7 8 5 8 9 9 9 17 13 10 18 3 10 19 9 11 11 8 11 12 8 12 13 11 12 14 6 13 15 6 13 16 12 14 20 2 15 21 14

### 2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 1 22 1: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0 2 29 2: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0 9 36 9: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
and for every transition t, a duplicate t is considered.

### 3 Transition Removal

We remove transitions 0, 3, 4, 7, 8, 18, 20, 21 using the following ranking functions, which are bounded by −23.

 15: 0 14: 0 0: 0 2: 0 1: 0 6: 0 7: 0 8: 0 9: 0 10: 0 11: 0 12: 0 13: 0 5: 0 3: 0 4: 0 15: −8 14: −9 0: −10 2: −10 2_var_snapshot: −10 2*: −10 1: −11 6: −11 7: −11 8: −11 9: −11 10: −11 11: −11 12: −11 13: −11 1_var_snapshot: −11 1*: −11 9_var_snapshot: −11 9*: −11 5: −12 3: −15 4: −16
Hints:
 23 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] ] 30 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] ] 37 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] ] 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] ] 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] ] 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] ] 6 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] ] 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, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 13 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] ] 14 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] ] 15 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] ] 16 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] ] 17 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] ] 19 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 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] ] 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] ] 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, 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, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 21 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] ]

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

1* 25 1: i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0factor_post + factor_post ≤ 0factor_postfactor_post ≤ 0factor_0 + factor_0 ≤ 0factor_0factor_0 ≤ 0fact3_post + fact3_post ≤ 0fact3_postfact3_post ≤ 0fact3_0 + fact3_0 ≤ 0fact3_0fact3_0 ≤ 0Temp6_post + Temp6_post ≤ 0Temp6_postTemp6_post ≤ 0Temp6_0 + Temp6_0 ≤ 0Temp6_0Temp6_0 ≤ 0Sorted5_post + Sorted5_post ≤ 0Sorted5_postSorted5_post ≤ 0Sorted5_0 + Sorted5_0 ≤ 0Sorted5_0Sorted5_0 ≤ 0Index7_post + Index7_post ≤ 0Index7_postIndex7_post ≤ 0Index7_0 + Index7_0 ≤ 0Index7_0Index7_0 ≤ 0Index2_post + Index2_post ≤ 0Index2_postIndex2_post ≤ 0Index2_0 + Index2_0 ≤ 0Index2_0Index2_0 ≤ 0

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

1 23 1_var_snapshot: i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0factor_post + factor_post ≤ 0factor_postfactor_post ≤ 0factor_0 + factor_0 ≤ 0factor_0factor_0 ≤ 0fact3_post + fact3_post ≤ 0fact3_postfact3_post ≤ 0fact3_0 + fact3_0 ≤ 0fact3_0fact3_0 ≤ 0Temp6_post + Temp6_post ≤ 0Temp6_postTemp6_post ≤ 0Temp6_0 + Temp6_0 ≤ 0Temp6_0Temp6_0 ≤ 0Sorted5_post + Sorted5_post ≤ 0Sorted5_postSorted5_post ≤ 0Sorted5_0 + Sorted5_0 ≤ 0Sorted5_0Sorted5_0 ≤ 0Index7_post + Index7_post ≤ 0Index7_postIndex7_post ≤ 0Index7_0 + Index7_0 ≤ 0Index7_0Index7_0 ≤ 0Index2_post + Index2_post ≤ 0Index2_postIndex2_post ≤ 0Index2_0 + Index2_0 ≤ 0Index2_0Index2_0 ≤ 0

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

2* 32 2: i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0factor_post + factor_post ≤ 0factor_postfactor_post ≤ 0factor_0 + factor_0 ≤ 0factor_0factor_0 ≤ 0fact3_post + fact3_post ≤ 0fact3_postfact3_post ≤ 0fact3_0 + fact3_0 ≤ 0fact3_0fact3_0 ≤ 0Temp6_post + Temp6_post ≤ 0Temp6_postTemp6_post ≤ 0Temp6_0 + Temp6_0 ≤ 0Temp6_0Temp6_0 ≤ 0Sorted5_post + Sorted5_post ≤ 0Sorted5_postSorted5_post ≤ 0Sorted5_0 + Sorted5_0 ≤ 0Sorted5_0Sorted5_0 ≤ 0Index7_post + Index7_post ≤ 0Index7_postIndex7_post ≤ 0Index7_0 + Index7_0 ≤ 0Index7_0Index7_0 ≤ 0Index2_post + Index2_post ≤ 0Index2_postIndex2_post ≤ 0Index2_0 + Index2_0 ≤ 0Index2_0Index2_0 ≤ 0

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

2 30 2_var_snapshot: i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0factor_post + factor_post ≤ 0factor_postfactor_post ≤ 0factor_0 + factor_0 ≤ 0factor_0factor_0 ≤ 0fact3_post + fact3_post ≤ 0fact3_postfact3_post ≤ 0fact3_0 + fact3_0 ≤ 0fact3_0fact3_0 ≤ 0Temp6_post + Temp6_post ≤ 0Temp6_postTemp6_post ≤ 0Temp6_0 + Temp6_0 ≤ 0Temp6_0Temp6_0 ≤ 0Sorted5_post + Sorted5_post ≤ 0Sorted5_postSorted5_post ≤ 0Sorted5_0 + Sorted5_0 ≤ 0Sorted5_0Sorted5_0 ≤ 0Index7_post + Index7_post ≤ 0Index7_postIndex7_post ≤ 0Index7_0 + Index7_0 ≤ 0Index7_0Index7_0 ≤ 0Index2_post + Index2_post ≤ 0Index2_postIndex2_post ≤ 0Index2_0 + Index2_0 ≤ 0Index2_0Index2_0 ≤ 0

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

9* 39 9: i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0factor_post + factor_post ≤ 0factor_postfactor_post ≤ 0factor_0 + factor_0 ≤ 0factor_0factor_0 ≤ 0fact3_post + fact3_post ≤ 0fact3_postfact3_post ≤ 0fact3_0 + fact3_0 ≤ 0fact3_0fact3_0 ≤ 0Temp6_post + Temp6_post ≤ 0Temp6_postTemp6_post ≤ 0Temp6_0 + Temp6_0 ≤ 0Temp6_0Temp6_0 ≤ 0Sorted5_post + Sorted5_post ≤ 0Sorted5_postSorted5_post ≤ 0Sorted5_0 + Sorted5_0 ≤ 0Sorted5_0Sorted5_0 ≤ 0Index7_post + Index7_post ≤ 0Index7_postIndex7_post ≤ 0Index7_0 + Index7_0 ≤ 0Index7_0Index7_0 ≤ 0Index2_post + Index2_post ≤ 0Index2_postIndex2_post ≤ 0Index2_0 + Index2_0 ≤ 0Index2_0Index2_0 ≤ 0

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

9 37 9_var_snapshot: i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0factor_post + factor_post ≤ 0factor_postfactor_post ≤ 0factor_0 + factor_0 ≤ 0factor_0factor_0 ≤ 0fact3_post + fact3_post ≤ 0fact3_postfact3_post ≤ 0fact3_0 + fact3_0 ≤ 0fact3_0fact3_0 ≤ 0Temp6_post + Temp6_post ≤ 0Temp6_postTemp6_post ≤ 0Temp6_0 + Temp6_0 ≤ 0Temp6_0Temp6_0 ≤ 0Sorted5_post + Sorted5_post ≤ 0Sorted5_postSorted5_post ≤ 0Sorted5_0 + Sorted5_0 ≤ 0Sorted5_0Sorted5_0 ≤ 0Index7_post + Index7_post ≤ 0Index7_postIndex7_post ≤ 0Index7_0 + Index7_0 ≤ 0Index7_0Index7_0 ≤ 0Index2_post + Index2_post ≤ 0Index2_postIndex2_post ≤ 0Index2_0 + Index2_0 ≤ 0Index2_0Index2_0 ≤ 0

### 10 SCC Decomposition

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

### 10.1 SCC Subproblem 1/2

Here we consider the SCC { 1, 6, 7, 8, 9, 10, 11, 12, 13, 1_var_snapshot, 1*, 9_var_snapshot, 9* }.

### 10.1.1 Transition Removal

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

 1: 1 − 7⋅i8_0 6: −3 − 7⋅i8_0 7: −4 − 7⋅i8_0 8: −2 − 7⋅i8_0 9: 2⋅factor_0 − 7⋅i8_0 10: 1 + 2⋅factor_post − 7⋅i8_0 11: 2⋅factor_post − 7⋅i8_0 12: 2⋅factor_0 − 7⋅i8_0 13: 2⋅factor_post − 7⋅i8_0 1_var_snapshot: −7⋅i8_0 1*: 2 − 7⋅i8_0 9_var_snapshot: 2 + 2⋅factor_0 + 2⋅factor_post − 7⋅i8_0 9*: 2⋅factor_post − 7⋅i8_0
Hints:
 23 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 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 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 37 lexWeak[ [0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 7, 2, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 39 lexWeak[ [0, 0, 2, 0, 0, 2, 0, 0, 0, 0, 7, 0, 0, 2, 0, 0, 0, 0, 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, 7, 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 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 9 lexWeak[ [0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 10 lexWeak[ [0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 11 lexWeak[ [0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 12 lexWeak[ [0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 7, 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 lexWeak[ [0, 2, 0, 0, 0, 0, 2, 0, 0, 0, 0, 7, 2, 0, 0, 0, 0, 0, 0, 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, 2, 0, 0, 0, 0, 7, 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 lexWeak[ [0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 7, 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 lexWeak[ [0, 0, 2, 0, 0, 2, 0, 0, 0, 0, 0, 7, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 17 lexWeak[ [0, 0, 0, 0, 0, 0, 2, 0, 0, 0, 7, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 19 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, 7, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 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.1.2 Transition Removal

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

 1: −7⋅Index7_0 + 4⋅fact3_post + 2⋅factor_0 6: −3 − 7⋅Index7_0 7: −7⋅Index7_0 + 4⋅fact3_post 8: −7⋅Index7_0 + 4⋅factor_0 9: −5 − 7⋅Index7_0 − 6⋅factor_post 10: −7⋅Index7_0 + 4⋅fact3_post + 4⋅factor_0 11: −7⋅Index7_0 + 3⋅factor_post 12: −2 − 7⋅Index7_0 13: −7⋅Index7_0 + factor_post 1_var_snapshot: −3 − 7⋅Index7_0 + 4⋅fact3_post 1*: −1 − 7⋅Index7_0 + 4⋅fact3_post 9_var_snapshot: −7⋅Index7_0 9*: −7⋅Index7_0 + 4⋅factor_0 − 6⋅factor_post
Hints:
 23 lexWeak[ [0, 0, 0, 0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0] ] 25 lexWeak[ [0, 0, 0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0] ] 37 lexWeak[ [0, 6, 0, 0, 0, 0, 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, 0, 0, 0, 0] ] 39 lexWeak[ [0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0] ] 5 lexWeak[ [4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0] ] 6 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0] ] 9 lexWeak[ [0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 7, 0, 7, 0, 0, 0, 0, 0, 6, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 10 lexWeak[ [0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0] ] 11 lexWeak[ [0, 0, 3, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0] ] 12 lexWeak[ [0, 0, 3, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0] ] 13 lexWeak[ [0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0] ] 14 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, 7, 0, 0, 0, 0] ] 15 lexWeak[ [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, 7, 0, 0, 0, 0] ] 16 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, 7, 0, 0, 0, 0] , [0, 0, 1, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 17 lexWeak[ [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, 7, 0, 0, 0, 0] ]

### 10.1.3 Transition Removal

We remove transitions 23, 25, 37, 39, 5, 9, 10, 11, 12, 13, 14, 15, 17 using the following ranking functions, which are bounded by −5.

 1: 3⋅factor_post 6: −2⋅fact3_post + factor_0 + factor_post 7: −2 − 2⋅fact3_post + factor_0 8: 2 − 5⋅fact3_0 − 2⋅fact3_post + factor_0 + 3⋅factor_post 9: −4 − 5⋅fact3_0 − 2⋅fact3_post 10: −1 + 4⋅factor_0 11: −5⋅fact3_0 − 2⋅fact3_post + factor_0 12: Index2_0 − 5⋅fact3_0 − 2⋅fact3_post + factor_0 13: −2⋅fact3_post + factor_0 1_var_snapshot: 4⋅factor_0 1*: −2⋅fact3_post + factor_0 + 3⋅factor_post 9_var_snapshot: −2⋅fact3_post 9*: −5⋅fact3_0 − 2⋅fact3_post + 3⋅factor_post
Hints:
 23 lexStrict[ [0, 0, 3, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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[ [2, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [2, 0, 3, 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] ] 37 lexStrict[ [0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [2, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 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, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [2, 0, 3, 0, 5, 0, 0, 0, 0, 0, 0, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [2, 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] ] 6 lexWeak[ [0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 1, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 9 lexStrict[ [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 2, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [2, 0, 3, 0, 5, 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] ] 10 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 11 lexStrict[ [0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 1, 0, 0, 2, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0] , [2, 0, 0, 0, 5, 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] ] 12 lexStrict[ [0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 1, 0, 0, 2, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [2, 0, 0, 0, 5, 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] ] 13 lexStrict[ [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 2, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [2, 0, 0, 1, 5, 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] ] 14 lexStrict[ [0, 1, 0, 1, 5, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [2, 0, 0, 1, 5, 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] ] 15 lexStrict[ [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [2, 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] ] 17 lexStrict[ [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 10.1.4 Transition Removal

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

 1: 0 6: 0 7: Index2_0 8: 0 9: 0 10: 0 11: 0 12: 0 13: 0 1_var_snapshot: 0 1*: 0 9_var_snapshot: 0 9*: 0
Hints:
 6 lexStrict[ [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, 0, 0, 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.1.5 Splitting Cut-Point Transitions

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

### 10.1.5.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 22.

### 10.1.5.1.1 Splitting Cut-Point Transitions

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

### 10.1.5.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 36.

### 10.1.5.2.1 Splitting Cut-Point Transitions

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

### 10.2 SCC Subproblem 2/2

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

### 10.2.1 Transition Removal

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

 0: −4⋅Index2_0 + 3⋅factor_0 + factor_post 2: −2 − 4⋅Index2_0 2_var_snapshot: −4⋅Index2_0 + 3⋅factor_0 2*: −4⋅Index2_0 + factor_post
Hints:
 30 lexWeak[ [0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4] ] 32 lexWeak[ [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, 4] ] 1 lexStrict[ [0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 4, 0, 4, 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, 1, 0, 0, 3, 0, 0, 4, 0, 0, 0, 0, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4] ]

### 10.2.2 Transition Removal

We remove transitions 30, 32, 2 using the following ranking functions, which are bounded by −2.

 0: fact3_0 + factor_0 2: 0 2_var_snapshot: factor_0 2*: 1
Hints:
 30 lexStrict[ [0, 0, 0, 0, 1, 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] ] 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, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 1, 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, 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] ]

### 10.2.3 Splitting Cut-Point Transitions

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

### 10.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 29.

### 10.2.3.1.1 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0