# LTS Termination Proof

by T2Cert

## Input

Integer Transition System
• Initial Location: 13
• Transitions: (pre-variables and post-variables)  0 0 1: 5 − 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 0 1 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ −4 + 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 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 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 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 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 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 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 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 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 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 10 11 6: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 5 − 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 10 12 11: −4 + 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 7 13 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 5 − 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 7 14 9: 0 ≤ 0 ∧ 0 ≤ 0 ∧ −4 + 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 4 15 3: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 5 − 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 4 16 6: 0 ≤ 0 ∧ 0 ≤ 0 ∧ −4 + 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 12 17 3: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −400 + x1_post ≤ 0 ∧ 400 − 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 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

## Proof

### 1 Invariant Updates

The following invariants are asserted.

 0: −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 1: −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 2: −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 3: −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 4: −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 5: −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 6: −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 7: −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 8: −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 9: −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 10: −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 11: −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 12: TRUE 13: TRUE

The invariants are proved as follows.

### IMPACT Invariant Proof

• nodes (location) invariant:  0 (0) −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 1 (1) −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 2 (2) −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 3 (3) −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 4 (4) −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 5 (5) −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 6 (6) −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 7 (7) −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 8 (8) −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 9 (9) −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 10 (10) −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 11 (11) −400 + x1_post ≤ 0 ∧ 400 − x1_post ≤ 0 ∧ −400 + x1_0 ≤ 0 ∧ 400 − x1_0 ≤ 0 12 (12) TRUE 13 (13) TRUE
• initial node: 13
• cover edges:
• transition edges:  0 0 1 0 1 2 1 4 5 2 3 4 3 2 0 4 15 3 4 16 6 6 5 7 7 13 2 7 14 9 8 6 9 9 7 10 10 11 6 10 12 11 11 8 8 11 9 1 11 10 8 12 17 3 13 18 12

### 2 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 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 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 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
and for every transition t, a duplicate t is considered.

### 3 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

### 4 Location Addition

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

### 5 Location Addition

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

### 6 Location Addition

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

### 7 Location Addition

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

### 8 Location Addition

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

### 9 Location Addition

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

### 10 Location Addition

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

### 11 Location Addition

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

### 12 SCC Decomposition

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

### 12.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* }.

### 12.1.1 Transition Removal

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

 2: −1601⋅i2_0 4: −1601⋅i2_0 6: −1601⋅i2_0 7: −1601⋅i2_0 8: −1601⋅i2_0 9: −1601⋅i2_0 10: −1601⋅i2_0 11: −1601⋅i2_0 0: −1601⋅i2_0 + x1_0 3: 1200 − 1601⋅i2_0 2_var_snapshot: −1601⋅i2_0 2*: −1601⋅i2_0 3_var_snapshot: 800 − 1601⋅i2_0 3*: −1601⋅i2_0 + 4⋅x1_0 6_var_snapshot: −1601⋅i2_0 6*: −1601⋅i2_0 9_var_snapshot: −1601⋅i2_0 9*: −1601⋅i2_0

### 12.1.2 Transition Removal

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

 2: 800 − 1601⋅j3_0 + x1_0 + x1_post 4: −1601⋅j3_0 + x1_0 + x1_post 6: −1601⋅j3_0 + x1_0 7: −1601⋅j3_0 + x1_0 8: 400 − 1601⋅j3_0 9: −1601⋅j3_0 + x1_0 10: −1601⋅j3_0 + x1_post 11: −1601⋅j3_0 + x1_0 0: −1601⋅j3_0 + x1_post 3: 798 − 1601⋅j3_0 2_var_snapshot: 800 − 1601⋅j3_0 + x1_post 2*: −1601⋅j3_0 + x1_0 + 4⋅x1_post 3_var_snapshot: −3 − 1601⋅j3_0 + 2⋅x1_0 3*: 399 − 1601⋅j3_0 + x1_post 6_var_snapshot: −1601⋅j3_0 + x1_0 6*: −400 − 1601⋅j3_0 + x1_0 + x1_post 9_var_snapshot: 400 − 1601⋅j3_0 9*: −1601⋅j3_0 + x1_0

### 12.1.3 Transition Removal

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

 2: −401⋅k4_0 + x1_0 4: 399 − 401⋅k4_0 − x1_0 6: −396 − 6⋅k4_0 + x1_post 7: −398 − 6⋅k4_0 + x1_post 8: −6⋅k4_0 9: −6⋅k4_0 10: −6⋅k4_0 11: −6⋅k4_0 0: −401⋅k4_0 − 2⋅x1_post 3: 1 − 401⋅k4_0 − x1_0 2_var_snapshot: −401⋅k4_0 − x1_0 + x1_post 2*: 1977 − 401⋅k4_0 3_var_snapshot: −401⋅k4_0 − x1_0 3*: 398 − 401⋅k4_0 − 2⋅x1_0 + x1_post 6_var_snapshot: 3 − 6⋅k4_0 6*: 5 − 6⋅k4_0 9_var_snapshot: −6⋅k4_0 9*: −400 − 6⋅k4_0 + x1_post

### 12.1.4 Transition Removal

We remove transitions 20, 22, 27, 29, 34, 36, 2, 3, 5, 11, 13, 15 using the following ranking functions, which are bounded by −3601.

 2: 1200 − 7⋅x1_0 4: 400 − 7⋅x1_0 6: 0 7: −6⋅x1_0 + 4⋅x1_post 8: 800 9: 800 10: 2⋅x1_post 11: 800 0: −1 − x1_0 − 8⋅x1_post 3: −8⋅x1_post 2_var_snapshot: 800 − 7⋅x1_0 2*: −7⋅x1_0 + 4⋅x1_post 3_var_snapshot: − x1_0 − 8⋅x1_post 3*: −7⋅x1_0 6_var_snapshot: 2000 − 6⋅x1_0 6*: − x1_0 + 2⋅x1_post 9_var_snapshot: 800 9*: 2⋅x1_0

### 12.1.5 Transition Removal

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

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

### 12.1.6 Transition Removal

We remove transitions 41, 43, 6, 7, 8, 10 using the following ranking functions, which are bounded by −1201.

 2: 0 4: 0 6: 0 7: 0 8: 0 9: −2⋅x1_post 10: −4⋅x1_0 11: 1 0: 0 3: 0 2_var_snapshot: 0 2*: 0 3_var_snapshot: 0 3*: 0 6_var_snapshot: 0 6*: 0 9_var_snapshot: −3⋅x1_0 9*: −400

### 12.1.7 Splitting Cut-Point Transitions

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

### 12.1.7.1 Cut-Point Subproblem 1/4

Here we consider cut-point transition 19.

### 12.1.7.1.1 Splitting Cut-Point Transitions

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

### 12.1.7.2 Cut-Point Subproblem 2/4

Here we consider cut-point transition 26.

### 12.1.7.2.1 Splitting Cut-Point Transitions

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

### 12.1.7.3 Cut-Point Subproblem 3/4

Here we consider cut-point transition 33.

### 12.1.7.3.1 Splitting Cut-Point Transitions

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

### 12.1.7.4 Cut-Point Subproblem 4/4

Here we consider cut-point transition 40.

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