# LTS Termination Proof

by T2Cert

## Input

Integer Transition System
• Initial Location: 8
• Transitions: (pre-variables and post-variables)  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 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ − oldX2_post + x0_post ≤ 0 ∧ oldX2_post − x0_post ≤ 0 ∧ − oldX3_post + x1_post ≤ 0 ∧ oldX3_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ oldX2_0 − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_post ≤ 0 ∧ oldX3_0 − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 0 1 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ 1 − oldX0_post + x0_post ≤ 0 ∧ −1 + oldX0_post − x0_post ≤ 0 ∧ − oldX2_post + x1_post ≤ 0 ∧ oldX2_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ oldX2_0 − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 0 2 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ 1 − oldX1_post + x1_post ≤ 0 ∧ −1 + oldX1_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 3 3 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 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ − oldX2_post + x0_post ≤ 0 ∧ oldX2_post − x0_post ≤ 0 ∧ − oldX3_post + x1_post ≤ 0 ∧ oldX3_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ oldX2_0 − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_post ≤ 0 ∧ oldX3_0 − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 3 4 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ 1 − oldX0_post + x0_post ≤ 0 ∧ −1 + oldX0_post − x0_post ≤ 0 ∧ −1 + x1_post ≤ 0 ∧ 1 − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 4 5 0: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ 1 − oldX1_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 4 6 3: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ oldX1_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 5 7 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 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ − oldX2_post + x0_post ≤ 0 ∧ oldX2_post − x0_post ≤ 0 ∧ − oldX3_post + x1_post ≤ 0 ∧ oldX3_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ oldX2_0 − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_post ≤ 0 ∧ oldX3_0 − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 6 8 4: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ 1 − oldX0_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 6 9 5: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ oldX0_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 2 10 6: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 7 11 0: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0 7 12 3: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0 7 13 1: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0 7 14 4: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0 7 15 5: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0 7 16 6: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0 7 17 2: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0 8 18 7: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_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 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0
and for every transition t, a duplicate t is considered.

### 2 Transition Removal

We remove transitions 0, 3, 7, 9, 11, 12, 13, 14, 15, 16, 17, 18 using the following ranking functions, which are bounded by −15.

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

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 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_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 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0

### 5 SCC Decomposition

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

### 5.1 SCC Subproblem 1/1

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

### 5.1.1 Splitting Cut-Point Transitions

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

### 5.1.1.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 19.

The new variable __snapshot_2_x1_post is introduced. The transition formulas are extended as follows:

 20: __snapshot_2_x1_post ≤ x1_post ∧ x1_post ≤ __snapshot_2_x1_post 22: __snapshot_2_x1_post ≤ __snapshot_2_x1_post ∧ __snapshot_2_x1_post ≤ __snapshot_2_x1_post 1: __snapshot_2_x1_post ≤ __snapshot_2_x1_post ∧ __snapshot_2_x1_post ≤ __snapshot_2_x1_post 2: __snapshot_2_x1_post ≤ __snapshot_2_x1_post ∧ __snapshot_2_x1_post ≤ __snapshot_2_x1_post 4: __snapshot_2_x1_post ≤ __snapshot_2_x1_post ∧ __snapshot_2_x1_post ≤ __snapshot_2_x1_post 5: __snapshot_2_x1_post ≤ __snapshot_2_x1_post ∧ __snapshot_2_x1_post ≤ __snapshot_2_x1_post 6: __snapshot_2_x1_post ≤ __snapshot_2_x1_post ∧ __snapshot_2_x1_post ≤ __snapshot_2_x1_post 8: __snapshot_2_x1_post ≤ __snapshot_2_x1_post ∧ __snapshot_2_x1_post ≤ __snapshot_2_x1_post 10: __snapshot_2_x1_post ≤ __snapshot_2_x1_post ∧ __snapshot_2_x1_post ≤ __snapshot_2_x1_post

The new variable __snapshot_2_x1_0 is introduced. The transition formulas are extended as follows:

 20: __snapshot_2_x1_0 ≤ x1_0 ∧ x1_0 ≤ __snapshot_2_x1_0 22: __snapshot_2_x1_0 ≤ __snapshot_2_x1_0 ∧ __snapshot_2_x1_0 ≤ __snapshot_2_x1_0 1: __snapshot_2_x1_0 ≤ __snapshot_2_x1_0 ∧ __snapshot_2_x1_0 ≤ __snapshot_2_x1_0 2: __snapshot_2_x1_0 ≤ __snapshot_2_x1_0 ∧ __snapshot_2_x1_0 ≤ __snapshot_2_x1_0 4: __snapshot_2_x1_0 ≤ __snapshot_2_x1_0 ∧ __snapshot_2_x1_0 ≤ __snapshot_2_x1_0 5: __snapshot_2_x1_0 ≤ __snapshot_2_x1_0 ∧ __snapshot_2_x1_0 ≤ __snapshot_2_x1_0 6: __snapshot_2_x1_0 ≤ __snapshot_2_x1_0 ∧ __snapshot_2_x1_0 ≤ __snapshot_2_x1_0 8: __snapshot_2_x1_0 ≤ __snapshot_2_x1_0 ∧ __snapshot_2_x1_0 ≤ __snapshot_2_x1_0 10: __snapshot_2_x1_0 ≤ __snapshot_2_x1_0 ∧ __snapshot_2_x1_0 ≤ __snapshot_2_x1_0

The new variable __snapshot_2_x0_post is introduced. The transition formulas are extended as follows:

 20: __snapshot_2_x0_post ≤ x0_post ∧ x0_post ≤ __snapshot_2_x0_post 22: __snapshot_2_x0_post ≤ __snapshot_2_x0_post ∧ __snapshot_2_x0_post ≤ __snapshot_2_x0_post 1: __snapshot_2_x0_post ≤ __snapshot_2_x0_post ∧ __snapshot_2_x0_post ≤ __snapshot_2_x0_post 2: __snapshot_2_x0_post ≤ __snapshot_2_x0_post ∧ __snapshot_2_x0_post ≤ __snapshot_2_x0_post 4: __snapshot_2_x0_post ≤ __snapshot_2_x0_post ∧ __snapshot_2_x0_post ≤ __snapshot_2_x0_post 5: __snapshot_2_x0_post ≤ __snapshot_2_x0_post ∧ __snapshot_2_x0_post ≤ __snapshot_2_x0_post 6: __snapshot_2_x0_post ≤ __snapshot_2_x0_post ∧ __snapshot_2_x0_post ≤ __snapshot_2_x0_post 8: __snapshot_2_x0_post ≤ __snapshot_2_x0_post ∧ __snapshot_2_x0_post ≤ __snapshot_2_x0_post 10: __snapshot_2_x0_post ≤ __snapshot_2_x0_post ∧ __snapshot_2_x0_post ≤ __snapshot_2_x0_post

The new variable __snapshot_2_x0_0 is introduced. The transition formulas are extended as follows:

 20: __snapshot_2_x0_0 ≤ x0_0 ∧ x0_0 ≤ __snapshot_2_x0_0 22: __snapshot_2_x0_0 ≤ __snapshot_2_x0_0 ∧ __snapshot_2_x0_0 ≤ __snapshot_2_x0_0 1: __snapshot_2_x0_0 ≤ __snapshot_2_x0_0 ∧ __snapshot_2_x0_0 ≤ __snapshot_2_x0_0 2: __snapshot_2_x0_0 ≤ __snapshot_2_x0_0 ∧ __snapshot_2_x0_0 ≤ __snapshot_2_x0_0 4: __snapshot_2_x0_0 ≤ __snapshot_2_x0_0 ∧ __snapshot_2_x0_0 ≤ __snapshot_2_x0_0 5: __snapshot_2_x0_0 ≤ __snapshot_2_x0_0 ∧ __snapshot_2_x0_0 ≤ __snapshot_2_x0_0 6: __snapshot_2_x0_0 ≤ __snapshot_2_x0_0 ∧ __snapshot_2_x0_0 ≤ __snapshot_2_x0_0 8: __snapshot_2_x0_0 ≤ __snapshot_2_x0_0 ∧ __snapshot_2_x0_0 ≤ __snapshot_2_x0_0 10: __snapshot_2_x0_0 ≤ __snapshot_2_x0_0 ∧ __snapshot_2_x0_0 ≤ __snapshot_2_x0_0

The new variable __snapshot_2_oldX3_post is introduced. The transition formulas are extended as follows:

 20: __snapshot_2_oldX3_post ≤ oldX3_post ∧ oldX3_post ≤ __snapshot_2_oldX3_post 22: __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post ∧ __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post 1: __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post ∧ __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post 2: __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post ∧ __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post 4: __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post ∧ __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post 5: __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post ∧ __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post 6: __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post ∧ __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post 8: __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post ∧ __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post 10: __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post ∧ __snapshot_2_oldX3_post ≤ __snapshot_2_oldX3_post

The new variable __snapshot_2_oldX3_0 is introduced. The transition formulas are extended as follows:

 20: __snapshot_2_oldX3_0 ≤ oldX3_0 ∧ oldX3_0 ≤ __snapshot_2_oldX3_0 22: __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 ∧ __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 1: __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 ∧ __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 2: __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 ∧ __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 4: __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 ∧ __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 5: __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 ∧ __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 6: __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 ∧ __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 8: __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 ∧ __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 10: __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0 ∧ __snapshot_2_oldX3_0 ≤ __snapshot_2_oldX3_0

The new variable __snapshot_2_oldX2_post is introduced. The transition formulas are extended as follows:

 20: __snapshot_2_oldX2_post ≤ oldX2_post ∧ oldX2_post ≤ __snapshot_2_oldX2_post 22: __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post ∧ __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post 1: __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post ∧ __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post 2: __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post ∧ __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post 4: __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post ∧ __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post 5: __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post ∧ __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post 6: __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post ∧ __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post 8: __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post ∧ __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post 10: __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post ∧ __snapshot_2_oldX2_post ≤ __snapshot_2_oldX2_post

The new variable __snapshot_2_oldX2_0 is introduced. The transition formulas are extended as follows:

 20: __snapshot_2_oldX2_0 ≤ oldX2_0 ∧ oldX2_0 ≤ __snapshot_2_oldX2_0 22: __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 ∧ __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 1: __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 ∧ __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 2: __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 ∧ __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 4: __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 ∧ __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 5: __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 ∧ __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 6: __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 ∧ __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 8: __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 ∧ __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 10: __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0 ∧ __snapshot_2_oldX2_0 ≤ __snapshot_2_oldX2_0

The new variable __snapshot_2_oldX1_post is introduced. The transition formulas are extended as follows:

 20: __snapshot_2_oldX1_post ≤ oldX1_post ∧ oldX1_post ≤ __snapshot_2_oldX1_post 22: __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post ∧ __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post 1: __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post ∧ __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post 2: __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post ∧ __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post 4: __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post ∧ __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post 5: __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post ∧ __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post 6: __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post ∧ __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post 8: __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post ∧ __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post 10: __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post ∧ __snapshot_2_oldX1_post ≤ __snapshot_2_oldX1_post

The new variable __snapshot_2_oldX1_0 is introduced. The transition formulas are extended as follows:

 20: __snapshot_2_oldX1_0 ≤ oldX1_0 ∧ oldX1_0 ≤ __snapshot_2_oldX1_0 22: __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 ∧ __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 1: __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 ∧ __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 2: __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 ∧ __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 4: __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 ∧ __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 5: __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 ∧ __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 6: __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 ∧ __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 8: __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 ∧ __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 10: __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0 ∧ __snapshot_2_oldX1_0 ≤ __snapshot_2_oldX1_0

The new variable __snapshot_2_oldX0_post is introduced. The transition formulas are extended as follows:

 20: __snapshot_2_oldX0_post ≤ oldX0_post ∧ oldX0_post ≤ __snapshot_2_oldX0_post 22: __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post ∧ __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post 1: __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post ∧ __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post 2: __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post ∧ __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post 4: __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post ∧ __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post 5: __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post ∧ __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post 6: __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post ∧ __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post 8: __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post ∧ __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post 10: __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post ∧ __snapshot_2_oldX0_post ≤ __snapshot_2_oldX0_post

The new variable __snapshot_2_oldX0_0 is introduced. The transition formulas are extended as follows:

 20: __snapshot_2_oldX0_0 ≤ oldX0_0 ∧ oldX0_0 ≤ __snapshot_2_oldX0_0 22: __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 ∧ __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 1: __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 ∧ __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 2: __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 ∧ __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 4: __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 ∧ __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 5: __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 ∧ __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 6: __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 ∧ __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 8: __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 ∧ __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 10: __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0 ∧ __snapshot_2_oldX0_0 ≤ __snapshot_2_oldX0_0

The following invariants are asserted.

 0: TRUE 1: TRUE 2: TRUE 3: TRUE 4: TRUE 5: TRUE 6: TRUE 7: TRUE 8: TRUE 0: − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ − __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0 2: TRUE ∨ 1 − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0 ∨ − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0 3: − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0 4: − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ − __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0 6: − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ − __snapshot_2_x1_0 + x1_0 ≤ 0 2_var_snapshot: − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ − __snapshot_2_x1_0 + x1_0 ≤ 0 2*: 1 − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0 ∨ − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0

The invariants are proved as follows.

### IMPACT Invariant Proof

• nodes (location) invariant:  0 (8) TRUE 1 (7) TRUE 2 (0) TRUE 3 (3) TRUE 4 (1) TRUE 5 (4) TRUE 6 (5) TRUE 7 (6) TRUE 8 (2) TRUE 9 (6) TRUE 10 (2) TRUE 11 (2_var_snapshot) − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ − __snapshot_2_x1_0 + x1_0 ≤ 0 16 (1) TRUE 17 (2) TRUE 18 (2) TRUE 19 (1) TRUE 20 (2) TRUE 21 (0) TRUE 22 (3) TRUE 23 (4) TRUE 24 (5) TRUE 25 (6) − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ − __snapshot_2_x1_0 + x1_0 ≤ 0 26 (4) − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ − __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0 27 (0) − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ − __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0 28 (3) − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0 29 (2*) 1 − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0 30 (2) 1 − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0 31 (2_var_snapshot) − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ − __snapshot_2_x1_0 + x1_0 ≤ 0 36 (1) TRUE 37 (2*) 1 − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0 38 (2*) − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0 43 (2) − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 + x1_0 ≤ 0 ∧ 1 − __snapshot_2_x0_0 ≤ 0 ∧ 1 − __snapshot_2_x1_0 ≤ 0 44 (2_var_snapshot) − __snapshot_2_x0_0 + x0_0 ≤ 0 ∧ − __snapshot_2_x1_0 + x1_0 ≤ 0
• initial node: 0
• cover edges:
4 → 36 Hint: auto
6 → 24 Hint: auto
9 → 7 Hint: auto
16 → 36 Hint: auto
17 → 8 Hint: auto
18 → 8 Hint: auto
19 → 36 Hint: auto
20 → 8 Hint: auto
21 → 2 Hint: auto
22 → 3 Hint: auto
23 → 5 Hint: auto
31 → 11 Hint: distribute conclusion [1, 0] [0, 1]
37 → 29 Hint: distribute conclusion [1, 0] [0, 1]
44 → 11 Hint: distribute conclusion [1, 0] [0, 1]
• transition edges:
0 18 1 Hint: auto
1 11 2 Hint: auto
1 12 3 Hint: auto
1 13 4 Hint: auto
1 14 5 Hint: auto
1 15 6 Hint: auto
1 16 7 Hint: auto
1 17 8 Hint: auto
2 0 16 Hint: auto
2 1 17 Hint: auto
2 2 18 Hint: auto
3 3 19 Hint: auto
3 4 20 Hint: auto
5 5 21 Hint: auto
5 6 22 Hint: auto
7 8 23 Hint: auto
7 9 24 Hint: auto
8 10 9 Hint: auto
8 19 10 Hint: auto
10 20 11 Hint: distribute conclusion [0, 0, 0, 0, 0, 0, 0, 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, 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]
11 10 25 Hint: distribute conclusion [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 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, 1, 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, 1, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 1, 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]
24 7 36 Hint: auto
25 8 26 Hint: distribute conclusion [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 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, 1, 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, 1, 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, 1, 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, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
26 5 27 Hint: distribute conclusion [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 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, 1, 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, 1, 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, 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, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
26 6 28 Hint: distribute conclusion [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 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, 1, 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, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
27 1 37 Hint: distribute conclusion [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 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, 1, 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, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
27 2 38 Hint: distribute conclusion [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 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, 1, 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, 1, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 1, 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, 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, 1, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
28 4 29 Hint: distribute conclusion [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 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, 1, 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, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
29 22 30 Hint: distribute conclusion [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, 1, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
30 20 31 Hint: distribute conclusion [0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 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]
38 22 43 Hint: distribute conclusion [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, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] [0, 1, 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, 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, 0, 0, 0, 0, 1, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
43 20 44 Hint: distribute conclusion [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 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]

### 5.1.1.1.14 Transition Removal

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

 0: [__snapshot_2_x0_0, __snapshot_2_x1_0] 2: [x0_0, x1_0] 3: [__snapshot_2_x0_0, __snapshot_2_x1_0] 4: [__snapshot_2_x0_0, __snapshot_2_x1_0] 6: [__snapshot_2_x0_0, __snapshot_2_x1_0] 2_var_snapshot: [__snapshot_2_x0_0, __snapshot_2_x1_0] 2*: [__snapshot_2_x0_0, __snapshot_2_x1_0]
Hints:
20 distribute assertion
 lexWeak[ [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, 1, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] lexWeak[ [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, 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, 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] ] lexWeak[ [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, 1, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
22 distribute assertion
 lexStrict[ [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, 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] ] lexStrict[ [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, 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, 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, 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] ]
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, 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, 1, 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, 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, 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] ]
4 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, 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, 1, 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, 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, 1, 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, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
8 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, 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, 1, 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, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 5.1.1.1.15 Transition Removal

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

 2: −1 2_var_snapshot: −2 6: −3 4: −4 0: −5 3: −6 2*: −7
Hints:
20 distribute assertion
 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, 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, 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, 0, 0, 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, 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, 0, 0, 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 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, 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, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
8 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, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 5.1.1.1.16 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0