# LTS Termination Proof

by T2Cert

## Input

Integer Transition System
• Initial Location: 13
• Transitions: (pre-variables and post-variables)  0 0 1: ___const_5_0 − i2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0 0 1 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − ___const_5_0 + i2_0 ≤ 0 ∧ j3_post ≤ 0 ∧ − j3_post ≤ 0 ∧ j3_0 − j3_post ≤ 0 ∧ − j3_0 + j3_post ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0 3 2 0: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0 2 3 4: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0 1 4 5: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0 6 5 7: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0 8 6 9: 0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − l5_0 + l5_post ≤ 0 ∧ 1 + l5_0 − l5_post ≤ 0 ∧ l5_0 − l5_post ≤ 0 ∧ − l5_0 + l5_post ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0 9 7 10: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0 11 8 8: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0 11 9 1: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0 11 10 8: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0 10 11 6: 0 ≤ 0 ∧ 0 ≤ 0 ∧ ___const_5_0 − l5_0 ≤ 0 ∧ −1 − k4_0 + k4_post ≤ 0 ∧ 1 + k4_0 − k4_post ≤ 0 ∧ k4_0 − k4_post ≤ 0 ∧ − k4_0 + k4_post ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0 10 12 11: 1 − ___const_5_0 + l5_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0 7 13 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ ___const_5_0 − k4_0 ≤ 0 ∧ −1 − j3_0 + j3_post ≤ 0 ∧ 1 + j3_0 − j3_post ≤ 0 ∧ j3_0 − j3_post ≤ 0 ∧ − j3_0 + j3_post ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0 7 14 9: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − ___const_5_0 + k4_0 ≤ 0 ∧ l5_post ≤ 0 ∧ − l5_post ≤ 0 ∧ l5_0 − l5_post ≤ 0 ∧ − l5_0 + l5_post ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0 4 15 3: 0 ≤ 0 ∧ 0 ≤ 0 ∧ ___const_5_0 − j3_0 ≤ 0 ∧ −1 − i2_0 + i2_post ≤ 0 ∧ 1 + i2_0 − i2_post ≤ 0 ∧ i2_0 − i2_post ≤ 0 ∧ − i2_0 + i2_post ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0 4 16 6: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − ___const_5_0 + j3_0 ≤ 0 ∧ k4_post ≤ 0 ∧ − k4_post ≤ 0 ∧ k4_0 − k4_post ≤ 0 ∧ − k4_0 + k4_post ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0 12 17 3: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − ___const_400_0 + x1_post ≤ 0 ∧ ___const_400_0 − x1_post ≤ 0 ∧ i2_post ≤ 0 ∧ − i2_post ≤ 0 ∧ i2_0 − i2_post ≤ 0 ∧ − i2_0 + i2_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0 13 18 12: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0

## Proof

### 1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 2 19 2: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0 3 26 3: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0 6 33 6: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0 9 40 9: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0
and for every transition t, a duplicate t is considered.

### 2 Transition Removal

We remove transitions 0, 4, 9, 17, 18 using the following ranking functions, which are bounded by −21.

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

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

2* 22 2: x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0l5_post + l5_post ≤ 0l5_postl5_post ≤ 0l5_0 + l5_0 ≤ 0l5_0l5_0 ≤ 0k4_post + k4_post ≤ 0k4_postk4_post ≤ 0k4_0 + k4_0 ≤ 0k4_0k4_0 ≤ 0j3_post + j3_post ≤ 0j3_postj3_post ≤ 0j3_0 + j3_0 ≤ 0j3_0j3_0 ≤ 0i2_post + i2_post ≤ 0i2_posti2_post ≤ 0i2_0 + i2_0 ≤ 0i2_0i2_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0___const_400_0 + ___const_400_0 ≤ 0___const_400_0___const_400_0 ≤ 0

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

2 20 2_var_snapshot: x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0l5_post + l5_post ≤ 0l5_postl5_post ≤ 0l5_0 + l5_0 ≤ 0l5_0l5_0 ≤ 0k4_post + k4_post ≤ 0k4_postk4_post ≤ 0k4_0 + k4_0 ≤ 0k4_0k4_0 ≤ 0j3_post + j3_post ≤ 0j3_postj3_post ≤ 0j3_0 + j3_0 ≤ 0j3_0j3_0 ≤ 0i2_post + i2_post ≤ 0i2_posti2_post ≤ 0i2_0 + i2_0 ≤ 0i2_0i2_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0___const_400_0 + ___const_400_0 ≤ 0___const_400_0___const_400_0 ≤ 0

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

3* 29 3: x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0l5_post + l5_post ≤ 0l5_postl5_post ≤ 0l5_0 + l5_0 ≤ 0l5_0l5_0 ≤ 0k4_post + k4_post ≤ 0k4_postk4_post ≤ 0k4_0 + k4_0 ≤ 0k4_0k4_0 ≤ 0j3_post + j3_post ≤ 0j3_postj3_post ≤ 0j3_0 + j3_0 ≤ 0j3_0j3_0 ≤ 0i2_post + i2_post ≤ 0i2_posti2_post ≤ 0i2_0 + i2_0 ≤ 0i2_0i2_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0___const_400_0 + ___const_400_0 ≤ 0___const_400_0___const_400_0 ≤ 0

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

3 27 3_var_snapshot: x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0l5_post + l5_post ≤ 0l5_postl5_post ≤ 0l5_0 + l5_0 ≤ 0l5_0l5_0 ≤ 0k4_post + k4_post ≤ 0k4_postk4_post ≤ 0k4_0 + k4_0 ≤ 0k4_0k4_0 ≤ 0j3_post + j3_post ≤ 0j3_postj3_post ≤ 0j3_0 + j3_0 ≤ 0j3_0j3_0 ≤ 0i2_post + i2_post ≤ 0i2_posti2_post ≤ 0i2_0 + i2_0 ≤ 0i2_0i2_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0___const_400_0 + ___const_400_0 ≤ 0___const_400_0___const_400_0 ≤ 0

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

6* 36 6: x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0l5_post + l5_post ≤ 0l5_postl5_post ≤ 0l5_0 + l5_0 ≤ 0l5_0l5_0 ≤ 0k4_post + k4_post ≤ 0k4_postk4_post ≤ 0k4_0 + k4_0 ≤ 0k4_0k4_0 ≤ 0j3_post + j3_post ≤ 0j3_postj3_post ≤ 0j3_0 + j3_0 ≤ 0j3_0j3_0 ≤ 0i2_post + i2_post ≤ 0i2_posti2_post ≤ 0i2_0 + i2_0 ≤ 0i2_0i2_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0___const_400_0 + ___const_400_0 ≤ 0___const_400_0___const_400_0 ≤ 0

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

6 34 6_var_snapshot: x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0l5_post + l5_post ≤ 0l5_postl5_post ≤ 0l5_0 + l5_0 ≤ 0l5_0l5_0 ≤ 0k4_post + k4_post ≤ 0k4_postk4_post ≤ 0k4_0 + k4_0 ≤ 0k4_0k4_0 ≤ 0j3_post + j3_post ≤ 0j3_postj3_post ≤ 0j3_0 + j3_0 ≤ 0j3_0j3_0 ≤ 0i2_post + i2_post ≤ 0i2_posti2_post ≤ 0i2_0 + i2_0 ≤ 0i2_0i2_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0___const_400_0 + ___const_400_0 ≤ 0___const_400_0___const_400_0 ≤ 0

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

9* 43 9: x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0l5_post + l5_post ≤ 0l5_postl5_post ≤ 0l5_0 + l5_0 ≤ 0l5_0l5_0 ≤ 0k4_post + k4_post ≤ 0k4_postk4_post ≤ 0k4_0 + k4_0 ≤ 0k4_0k4_0 ≤ 0j3_post + j3_post ≤ 0j3_postj3_post ≤ 0j3_0 + j3_0 ≤ 0j3_0j3_0 ≤ 0i2_post + i2_post ≤ 0i2_posti2_post ≤ 0i2_0 + i2_0 ≤ 0i2_0i2_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0___const_400_0 + ___const_400_0 ≤ 0___const_400_0___const_400_0 ≤ 0

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

9 41 9_var_snapshot: x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0l5_post + l5_post ≤ 0l5_postl5_post ≤ 0l5_0 + l5_0 ≤ 0l5_0l5_0 ≤ 0k4_post + k4_post ≤ 0k4_postk4_post ≤ 0k4_0 + k4_0 ≤ 0k4_0k4_0 ≤ 0j3_post + j3_post ≤ 0j3_postj3_post ≤ 0j3_0 + j3_0 ≤ 0j3_0j3_0 ≤ 0i2_post + i2_post ≤ 0i2_posti2_post ≤ 0i2_0 + i2_0 ≤ 0i2_0i2_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0___const_400_0 + ___const_400_0 ≤ 0___const_400_0___const_400_0 ≤ 0

### 11 SCC Decomposition

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

### 11.1 SCC Subproblem 1/1

Here we consider the SCC { 2, 4, 6, 7, 8, 9, 10, 11, 0, 3, 2_var_snapshot, 2*, 3_var_snapshot, 3*, 6_var_snapshot, 6*, 9_var_snapshot, 9* }.

### 11.1.1 Transition Removal

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

 2: 5⋅___const_5_0 − 5⋅i2_0 4: 5⋅___const_5_0 − 5⋅i2_0 6: 5⋅___const_5_0 − 5⋅i2_0 7: 5⋅___const_5_0 − 5⋅i2_0 8: 5⋅___const_5_0 − 5⋅i2_0 9: 5⋅___const_5_0 − 5⋅i2_0 10: 5⋅___const_5_0 − 5⋅i2_0 11: 5⋅___const_5_0 − 5⋅i2_0 0: 1 + 5⋅___const_5_0 − 5⋅i2_0 3: 3 + 5⋅___const_5_0 − 5⋅i2_0 2_var_snapshot: 5⋅___const_5_0 − 5⋅i2_0 2*: 5⋅___const_5_0 − 5⋅i2_0 3_var_snapshot: 2 + 5⋅___const_5_0 − 5⋅i2_0 3*: 4 + 5⋅___const_5_0 − 5⋅i2_0 6_var_snapshot: 5⋅___const_5_0 − 5⋅i2_0 6*: 5⋅___const_5_0 − 5⋅i2_0 9_var_snapshot: 5⋅___const_5_0 − 5⋅i2_0 9*: 5⋅___const_5_0 − 5⋅i2_0

### 11.1.2 Transition Removal

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

 2: 1 + 13⋅___const_5_0 − 13⋅j3_0 4: 13⋅___const_5_0 − 13⋅j3_0 6: −11 + 13⋅___const_5_0 − 13⋅j3_0 7: −11 + 13⋅___const_5_0 − 13⋅j3_0 8: −11 + 13⋅___const_5_0 − 13⋅j3_0 9: −11 + 13⋅___const_5_0 − 13⋅j3_0 10: −11 + 13⋅___const_5_0 − 13⋅j3_0 11: −11 + 13⋅___const_5_0 − 13⋅j3_0 0: −4 + 13⋅___const_5_0 − 13⋅j3_0 3: −2 + 13⋅___const_5_0 − 13⋅j3_0 2_var_snapshot: 1 + 13⋅___const_5_0 − 13⋅j3_0 2*: 2 + 13⋅___const_5_0 − 13⋅j3_0 3_var_snapshot: −3 + 13⋅___const_5_0 − 13⋅j3_0 3*: −1 + 13⋅___const_5_0 − 13⋅j3_0 6_var_snapshot: −11 + 13⋅___const_5_0 − 13⋅j3_0 6*: −11 + 13⋅___const_5_0 − 13⋅j3_0 9_var_snapshot: −11 + 13⋅___const_5_0 − 13⋅j3_0 9*: −11 + 13⋅___const_5_0 − 13⋅j3_0

### 11.1.3 Transition Removal

We remove transitions 20, 22, 27, 29, 2, 3, 13, 15 using the following ranking functions, which are bounded by −8.

 2: −2 4: −4 6: 0 7: 0 8: 0 9: 0 10: 0 11: 0 0: −8 3: −6 2_var_snapshot: −3 2*: −1 3_var_snapshot: −7 3*: −5 6_var_snapshot: 0 6*: 0 9_var_snapshot: 0 9*: 0

### 11.1.4 Transition Removal

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

 2: 0 4: 0 6: 1 + 11⋅___const_5_0 − 11⋅k4_0 7: 11⋅___const_5_0 − 11⋅k4_0 8: −9 + 11⋅___const_5_0 − 11⋅k4_0 9: −9 + 11⋅___const_5_0 − 11⋅k4_0 10: −9 + 11⋅___const_5_0 − 11⋅k4_0 11: −9 + 11⋅___const_5_0 − 11⋅k4_0 0: 0 3: 0 2_var_snapshot: 0 2*: 0 3_var_snapshot: 0 3*: 0 6_var_snapshot: 1 + 11⋅___const_5_0 − 11⋅k4_0 6*: 2 + 11⋅___const_5_0 − 11⋅k4_0 9_var_snapshot: −9 + 11⋅___const_5_0 − 11⋅k4_0 9*: −9 + 11⋅___const_5_0 − 11⋅k4_0

### 11.1.5 Transition Removal

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

 2: 0 4: 0 6: −2 + 5⋅___const_5_0 − 5⋅l5_0 7: −4 + 5⋅___const_5_0 − 5⋅l5_0 8: −1 + 5⋅___const_5_0 − 5⋅l5_0 9: 2 + 5⋅___const_5_0 − 5⋅l5_0 10: 5⋅___const_5_0 − 5⋅l5_0 11: −1 + 5⋅___const_5_0 − 5⋅l5_0 0: 0 3: 0 2_var_snapshot: 0 2*: 0 3_var_snapshot: 0 3*: 0 6_var_snapshot: −3 + 5⋅___const_5_0 − 5⋅l5_0 6*: −1 + 5⋅___const_5_0 − 5⋅l5_0 9_var_snapshot: 1 + 5⋅___const_5_0 − 5⋅l5_0 9*: 3 + 5⋅___const_5_0 − 5⋅l5_0

### 11.1.6 Transition Removal

We remove transitions 34, 36, 41, 43, 5, 6, 7, 8, 10, 11 using the following ranking functions, which are bounded by −4.

 2: 0 4: 0 6: −2 7: −4 8: 4 9: 2 10: 0 11: 5 0: 0 3: 0 2_var_snapshot: 0 2*: 0 3_var_snapshot: 0 3*: 0 6_var_snapshot: −3 6*: −1 9_var_snapshot: 1 9*: 3

### 11.1.7 Splitting Cut-Point Transitions

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

### 11.1.7.1 Cut-Point Subproblem 1/4

Here we consider cut-point transition 19.

### 11.1.7.1.1 Splitting Cut-Point Transitions

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

### 11.1.7.2 Cut-Point Subproblem 2/4

Here we consider cut-point transition 26.

### 11.1.7.2.1 Splitting Cut-Point Transitions

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

### 11.1.7.3 Cut-Point Subproblem 3/4

Here we consider cut-point transition 33.

### 11.1.7.3.1 Splitting Cut-Point Transitions

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

### 11.1.7.4 Cut-Point Subproblem 4/4

Here we consider cut-point transition 40.

### 11.1.7.4.1 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0