# 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 − x2_0 ≤ 0 ∧ − oldX2_post + x2_0 ≤ 0 ∧ oldX3_post − x3_0 ≤ 0 ∧ − oldX3_post + x3_0 ≤ 0 ∧ − oldX4_post + oldX5_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ − oldX2_post + x2_post ≤ 0 ∧ oldX2_post − x2_post ≤ 0 ∧ − oldX3_post + x3_post ≤ 0 ∧ oldX3_post − x3_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 ∧ oldX4_0 − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_post ≤ 0 ∧ oldX5_0 − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ x2_0 − x2_post ≤ 0 ∧ − x2_0 + x2_post ≤ 0 ∧ x3_0 − x3_post ≤ 0 ∧ − x3_0 + x3_post ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 0 1 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 ∧ 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 − x2_0 ≤ 0 ∧ − oldX2_post + x2_0 ≤ 0 ∧ oldX3_post − x3_0 ≤ 0 ∧ − oldX3_post + x3_0 ≤ 0 ∧ 1 + oldX4_post − oldX5_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ − oldX2_post + x2_post ≤ 0 ∧ oldX2_post − x2_post ≤ 0 ∧ − oldX3_post + x3_post ≤ 0 ∧ oldX3_post − x3_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 ∧ oldX4_0 − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_post ≤ 0 ∧ oldX5_0 − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ x2_0 − x2_post ≤ 0 ∧ − x2_0 + x2_post ≤ 0 ∧ x3_0 − x3_post ≤ 0 ∧ − x3_0 + x3_post ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 3 2 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 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ oldX2_post − x2_0 ≤ 0 ∧ − oldX2_post + x2_0 ≤ 0 ∧ oldX3_post − x3_0 ≤ 0 ∧ − oldX3_post + x3_0 ≤ 0 ∧ oldX0_post − oldX3_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ − oldX2_post + x2_post ≤ 0 ∧ oldX2_post − x2_post ≤ 0 ∧ − oldX3_post + x3_post ≤ 0 ∧ oldX3_post − x3_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 ∧ x2_0 − x2_post ≤ 0 ∧ − x2_0 + x2_post ≤ 0 ∧ x3_0 − x3_post ≤ 0 ∧ − x3_0 + x3_post ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 3 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 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ oldX2_post − x2_0 ≤ 0 ∧ − oldX2_post + x2_0 ≤ 0 ∧ oldX3_post − x3_0 ≤ 0 ∧ − oldX3_post + x3_0 ≤ 0 ∧ 1 − oldX0_post + oldX3_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ − oldX2_post + x2_post ≤ 0 ∧ oldX2_post − x2_post ≤ 0 ∧ − oldX3_post + x3_post ≤ 0 ∧ oldX3_post − x3_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 ∧ x2_0 − x2_post ≤ 0 ∧ − x2_0 + x2_post ≤ 0 ∧ x3_0 − x3_post ≤ 0 ∧ − x3_0 + x3_post ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 5 4 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 ∧ 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 − x2_0 ≤ 0 ∧ − oldX2_post + x2_0 ≤ 0 ∧ oldX3_post − x3_0 ≤ 0 ∧ − oldX3_post + x3_0 ≤ 0 ∧ −1 + oldX0_post − oldX3_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ − oldX2_post + x2_post ≤ 0 ∧ oldX2_post − x2_post ≤ 0 ∧ − oldX3_post + x3_post ≤ 0 ∧ oldX3_post − x3_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 ∧ x2_0 − x2_post ≤ 0 ∧ − x2_0 + x2_post ≤ 0 ∧ x3_0 − x3_post ≤ 0 ∧ − x3_0 + x3_post ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 5 5 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 ∧ 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 − x2_0 ≤ 0 ∧ − oldX2_post + x2_0 ≤ 0 ∧ oldX3_post − x3_0 ≤ 0 ∧ − oldX3_post + x3_0 ≤ 0 ∧ 2 − oldX0_post + oldX3_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ − oldX2_post + x2_post ≤ 0 ∧ oldX2_post − x2_post ≤ 0 ∧ − oldX3_post + x3_post ≤ 0 ∧ oldX3_post − x3_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 ∧ x2_0 − x2_post ≤ 0 ∧ − x2_0 + x2_post ≤ 0 ∧ x3_0 − x3_post ≤ 0 ∧ − x3_0 + x3_post ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 8 6 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 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ oldX2_post − x2_0 ≤ 0 ∧ − oldX2_post + x2_0 ≤ 0 ∧ oldX3_post − x3_0 ≤ 0 ∧ − oldX3_post + x3_0 ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ − oldX2_post + x2_post ≤ 0 ∧ oldX2_post − x2_post ≤ 0 ∧ −1 − oldX2_post + x3_post ≤ 0 ∧ 1 + oldX2_post − x3_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 ∧ x2_0 − x2_post ≤ 0 ∧ − x2_0 + x2_post ≤ 0 ∧ x3_0 − x3_post ≤ 0 ∧ − x3_0 + x3_post ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 9 7 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 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ oldX2_post − x2_0 ≤ 0 ∧ − oldX2_post + x2_0 ≤ 0 ∧ oldX3_post − x3_0 ≤ 0 ∧ − oldX3_post + x3_0 ≤ 0 ∧ −1 + oldX0_post − oldX2_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ − oldX2_post + x2_post ≤ 0 ∧ oldX2_post − x2_post ≤ 0 ∧ x3_post ≤ 0 ∧ − x3_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 ∧ x2_0 − x2_post ≤ 0 ∧ − x2_0 + x2_post ≤ 0 ∧ x3_0 − x3_post ≤ 0 ∧ − x3_0 + x3_post ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 9 8 8: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 − x2_0 ≤ 0 ∧ − oldX2_post + x2_0 ≤ 0 ∧ oldX3_post − x3_0 ≤ 0 ∧ − oldX3_post + x3_0 ≤ 0 ∧ 2 − oldX0_post + oldX2_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ − oldX2_post + x2_post ≤ 0 ∧ oldX2_post − x2_post ≤ 0 ∧ − oldX4_post + x3_post ≤ 0 ∧ oldX4_post − x3_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 ∧ oldX4_0 − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ x2_0 − x2_post ≤ 0 ∧ − x2_0 + x2_post ≤ 0 ∧ x3_0 − x3_post ≤ 0 ∧ − x3_0 + x3_post ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 10 9 11: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 − x2_0 ≤ 0 ∧ − oldX2_post + x2_0 ≤ 0 ∧ oldX3_post − x3_0 ≤ 0 ∧ − oldX3_post + x3_0 ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ −1 − oldX1_post + x1_post ≤ 0 ∧ 1 + oldX1_post − x1_post ≤ 0 ∧ − oldX4_post + x2_post ≤ 0 ∧ oldX4_post − x2_post ≤ 0 ∧ − oldX5_post + x3_post ≤ 0 ∧ oldX5_post − x3_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 ∧ oldX4_0 − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_post ≤ 0 ∧ oldX5_0 − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ x2_0 − x2_post ≤ 0 ∧ − x2_0 + x2_post ≤ 0 ∧ x3_0 − x3_post ≤ 0 ∧ − x3_0 + x3_post ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 11 10 9: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 − x2_0 ≤ 0 ∧ − oldX2_post + x2_0 ≤ 0 ∧ oldX3_post − x3_0 ≤ 0 ∧ − oldX3_post + x3_0 ≤ 0 ∧ −1 + oldX0_post − oldX1_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ x2_post ≤ 0 ∧ − x2_post ≤ 0 ∧ − oldX4_post + x3_post ≤ 0 ∧ oldX4_post − x3_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 ∧ oldX4_0 − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ x2_0 − x2_post ≤ 0 ∧ − x2_0 + x2_post ≤ 0 ∧ x3_0 − x3_post ≤ 0 ∧ − x3_0 + x3_post ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 11 11 10: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 − x2_0 ≤ 0 ∧ − oldX2_post + x2_0 ≤ 0 ∧ oldX3_post − x3_0 ≤ 0 ∧ − oldX3_post + x3_0 ≤ 0 ∧ 2 − oldX0_post + oldX1_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ − oldX4_post + x2_post ≤ 0 ∧ oldX4_post − x2_post ≤ 0 ∧ − oldX5_post + x3_post ≤ 0 ∧ oldX5_post − x3_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 ∧ oldX4_0 − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_post ≤ 0 ∧ oldX5_0 − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ x2_0 − x2_post ≤ 0 ∧ − x2_0 + x2_post ≤ 0 ∧ x3_0 − x3_post ≤ 0 ∧ − x3_0 + x3_post ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 12 12 11: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 − x2_0 ≤ 0 ∧ − oldX2_post + x2_0 ≤ 0 ∧ oldX3_post − x3_0 ≤ 0 ∧ − oldX3_post + x3_0 ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ x1_post ≤ 0 ∧ − x1_post ≤ 0 ∧ − oldX4_post + x2_post ≤ 0 ∧ oldX4_post − x2_post ≤ 0 ∧ − oldX5_post + x3_post ≤ 0 ∧ oldX5_post − x3_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 ∧ oldX4_0 − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_post ≤ 0 ∧ oldX5_0 − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ x2_0 − x2_post ≤ 0 ∧ − x2_0 + x2_post ≤ 0 ∧ x3_0 − x3_post ≤ 0 ∧ − x3_0 + x3_post ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 6 13 13: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 − x2_0 ≤ 0 ∧ − oldX2_post + x2_0 ≤ 0 ∧ oldX3_post − x3_0 ≤ 0 ∧ − oldX3_post + x3_0 ≤ 0 ∧ − oldX4_post + x0_post ≤ 0 ∧ oldX4_post − x0_post ≤ 0 ∧ − oldX5_post + x1_post ≤ 0 ∧ oldX5_post − x1_post ≤ 0 ∧ − oldX6_post + x2_post ≤ 0 ∧ oldX6_post − x2_post ≤ 0 ∧ − oldX7_post + x3_post ≤ 0 ∧ oldX7_post − x3_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 ∧ oldX4_0 − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_post ≤ 0 ∧ oldX5_0 − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_post ≤ 0 ∧ oldX6_0 − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_post ≤ 0 ∧ oldX7_0 − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ x2_0 − x2_post ≤ 0 ∧ − x2_0 + x2_post ≤ 0 ∧ x3_0 − x3_post ≤ 0 ∧ − x3_0 + x3_post ≤ 0 7 14 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 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ oldX2_post − x2_0 ≤ 0 ∧ − oldX2_post + x2_0 ≤ 0 ∧ oldX3_post − x3_0 ≤ 0 ∧ − oldX3_post + x3_0 ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ − oldX2_post + x2_post ≤ 0 ∧ oldX2_post − x2_post ≤ 0 ∧ −1 − oldX3_post + x3_post ≤ 0 ∧ 1 + oldX3_post − x3_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 ∧ x2_0 − x2_post ≤ 0 ∧ − x2_0 + x2_post ≤ 0 ∧ x3_0 − x3_post ≤ 0 ∧ − x3_0 + x3_post ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 1 15 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 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ oldX2_post − x2_0 ≤ 0 ∧ − oldX2_post + x2_0 ≤ 0 ∧ oldX3_post − x3_0 ≤ 0 ∧ − oldX3_post + x3_0 ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ − oldX2_post + x2_post ≤ 0 ∧ oldX2_post − x2_post ≤ 0 ∧ −1 − oldX3_post + x3_post ≤ 0 ∧ 1 + oldX3_post − x3_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 ∧ x2_0 − x2_post ≤ 0 ∧ − x2_0 + x2_post ≤ 0 ∧ x3_0 − x3_post ≤ 0 ∧ − x3_0 + x3_post ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 2 16 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 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ oldX1_post − x1_0 ≤ 0 ∧ − oldX1_post + x1_0 ≤ 0 ∧ oldX2_post − x2_0 ≤ 0 ∧ − oldX2_post + x2_0 ≤ 0 ∧ oldX3_post − x3_0 ≤ 0 ∧ − oldX3_post + x3_0 ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ − oldX2_post + x2_post ≤ 0 ∧ oldX2_post − x2_post ≤ 0 ∧ − oldX3_post + x3_post ≤ 0 ∧ oldX3_post − x3_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 ∧ x2_0 − x2_post ≤ 0 ∧ − x2_0 + x2_post ≤ 0 ∧ x3_0 − x3_post ≤ 0 ∧ − x3_0 + x3_post ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 4 17 9: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 − x2_0 ≤ 0 ∧ − oldX2_post + x2_0 ≤ 0 ∧ oldX3_post − x3_0 ≤ 0 ∧ − oldX3_post + x3_0 ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX1_post + x1_post ≤ 0 ∧ oldX1_post − x1_post ≤ 0 ∧ −1 − oldX2_post + x2_post ≤ 0 ∧ 1 + oldX2_post − x2_post ≤ 0 ∧ − oldX4_post + x3_post ≤ 0 ∧ oldX4_post − x3_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 ∧ oldX4_0 − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ x2_0 − x2_post ≤ 0 ∧ − x2_0 + x2_post ≤ 0 ∧ x3_0 − x3_post ≤ 0 ∧ − x3_0 + x3_post ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 14 18 12: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 − x2_0 ≤ 0 ∧ − oldX2_post + x2_0 ≤ 0 ∧ oldX3_post − x3_0 ≤ 0 ∧ − oldX3_post + x3_0 ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ − oldX4_post + x1_post ≤ 0 ∧ oldX4_post − x1_post ≤ 0 ∧ − oldX5_post + x2_post ≤ 0 ∧ oldX5_post − x2_post ≤ 0 ∧ − oldX6_post + x3_post ≤ 0 ∧ oldX6_post − x3_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 ∧ oldX4_0 − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_post ≤ 0 ∧ oldX5_0 − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_post ≤ 0 ∧ oldX6_0 − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ x2_0 − x2_post ≤ 0 ∧ − x2_0 + x2_post ≤ 0 ∧ x3_0 − x3_post ≤ 0 ∧ − x3_0 + x3_post ≤ 0 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 14 19 0: − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 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 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_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 14 20 3: − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 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 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_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 14 21 5: − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 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 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_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 14 22 8: − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 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 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_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 14 23 9: − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 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 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_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 14 24 10: − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 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 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_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 14 25 11: − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 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 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_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 14 26 12: − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 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 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_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 14 27 13: − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 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 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_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 14 28 6: − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 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 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_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 14 29 7: − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 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 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_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 14 30 1: − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 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 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_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 14 31 2: − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 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 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_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 14 32 4: − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 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 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_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 15 33 14: − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 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 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_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:
 3 34 3: − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 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 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_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 4 41 4: − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 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 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_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 5 48 5: − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 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 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_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 11 55 11: − x3_post + x3_post ≤ 0 ∧ x3_post − x3_post ≤ 0 ∧ − x3_0 + x3_0 ≤ 0 ∧ x3_0 − x3_0 ≤ 0 ∧ − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 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 ∧ − oldX7_post + oldX7_post ≤ 0 ∧ oldX7_post − oldX7_post ≤ 0 ∧ − oldX7_0 + oldX7_0 ≤ 0 ∧ oldX7_0 − oldX7_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_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 4, 7, 10, 12, 13, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33 using the following ranking functions, which are bounded by −27.

 15: 0 14: 0 12: 0 10: 0 11: 0 0: 0 1: 0 2: 0 3: 0 4: 0 8: 0 9: 0 5: 0 7: 0 6: 0 13: 0 15: −9 14: −10 12: −11 10: −12 11: −12 11_var_snapshot: −12 11*: −12 0: −15 1: −15 2: −15 3: −15 4: −15 8: −15 9: −15 3_var_snapshot: −15 3*: −15 4_var_snapshot: −15 4*: −15 5: −18 7: −18 5_var_snapshot: −18 5*: −18 6: −21 13: −22
Hints:
 35 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] ] 42 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] ] 49 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] ] 56 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 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, 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, 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, 0, 0, 0, 0, 0] ] 3 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, 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, 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, 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, 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, 0, 0, 0, 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, 0, 0, 0, 0, 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, 0, 0, 0, 0, 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, 0, 0, 0, 0, 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, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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] ] 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, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 22 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] ] 23 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] ] 24 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] ] 25 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] ] 26 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] ] 27 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] ] 28 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] ] 29 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] ] 30 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] ] 31 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] ] 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 33 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] ]

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

3* 37 3: x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_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 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_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.

3 35 3_var_snapshot: x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_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 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_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.

4* 44 4: x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_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 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_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.

4 42 4_var_snapshot: x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_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 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_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.

5* 51 5: x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_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 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_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.

5 49 5_var_snapshot: x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_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 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_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.

11* 58 11: x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_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 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_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.

11 56 11_var_snapshot: x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_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 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_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

### 11 SCC Decomposition

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

### 11.1 SCC Subproblem 1/3

Here we consider the SCC { 10, 11, 11_var_snapshot, 11* }.

### 11.1.1 Transition Removal

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

 10: −2 + 5⋅x0_0 − 5⋅x1_0 11: 1 + 5⋅x0_0 − 5⋅x1_0 11_var_snapshot: 5⋅x0_0 − 5⋅x1_0 11*: 2 + 5⋅x0_0 − 5⋅x1_0
Hints:
 56 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 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, 0, 0, 0] ] 58 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 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, 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, 5, 0, 0, 5, 0, 0, 0, 0, 5, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 5, 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, 5, 0, 0, 5, 0, 0, 0, 0, 0, 5, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 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, 0, 0, 5, 0, 0, 5, 0, 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, 0, 0, 0, 0, 0, 0] ]

### 11.1.2 Transition Removal

We remove transitions 56, 9 using the following ranking functions, which are bounded by −3.

 10: 0 11: −2 11_var_snapshot: −3 11*: −1
Hints:
 56 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] ] 58 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] ] 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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.1.3 Transition Removal

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

 10: 0 11: −1 11_var_snapshot: 0 11*: 0
Hints:
 58 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] ]

### 11.1.4 Splitting Cut-Point Transitions

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

### 11.1.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 55.

### 11.1.4.1.1 Splitting Cut-Point Transitions

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

### 11.2 SCC Subproblem 2/3

Here we consider the SCC { 5, 7, 5_var_snapshot, 5* }.

### 11.2.1 Transition Removal

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

 5: 2 + 4⋅x0_0 − 4⋅x3_0 7: 4⋅x0_0 − 4⋅x3_0 5_var_snapshot: 1 + 4⋅x0_0 − 4⋅x3_0 5*: 3 + 4⋅x0_0 − 4⋅x3_0
Hints:
 49 lexWeak[ [0, 0, 0, 4, 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, 0, 0, 0] ] 51 lexWeak[ [0, 0, 0, 4, 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, 0, 0, 0] ] 5 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 4, 0, 4, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 4, 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, 0, 0, 4, 0, 0, 0, 0, 0, 0, 4, 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, 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, 4, 0, 0, 0, 0, 0, 0, 4, 4, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 11.2.2 Transition Removal

We remove transitions 49, 14 using the following ranking functions, which are bounded by −1.

 5: 0 7: 2 5_var_snapshot: −1 5*: 1
Hints:
 49 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] ] 51 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] ] 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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.2.3 Transition Removal

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

 5: −1 7: 0 5_var_snapshot: 0 5*: 0
Hints:
 51 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] ]

### 11.2.4 Splitting Cut-Point Transitions

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

### 11.2.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 48.

### 11.2.4.1.1 Splitting Cut-Point Transitions

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

### 11.3 SCC Subproblem 3/3

Here we consider the SCC { 0, 1, 2, 3, 4, 8, 9, 3_var_snapshot, 3*, 4_var_snapshot, 4* }.

### 11.3.1 Transition Removal

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

 0: 3 + 6⋅x0_0 − 6⋅x2_0 1: 3 + 6⋅x0_0 − 6⋅x2_0 2: 3 + 6⋅x0_0 − 6⋅x2_0 3: 3 + 6⋅x0_0 − 6⋅x2_0 4: 1 + 6⋅x0_0 − 6⋅x2_0 8: 4 + 6⋅x0_0 − 6⋅x2_0 9: 5 + 6⋅x0_0 − 6⋅x2_0 3_var_snapshot: 3 + 6⋅x0_0 − 6⋅x2_0 3*: 3 + 6⋅x0_0 − 6⋅x2_0 4_var_snapshot: 6⋅x0_0 − 6⋅x2_0 4*: 2 + 6⋅x0_0 − 6⋅x2_0
Hints:
 35 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0] ] 37 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0] ] 42 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0] ] 44 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0] ] 0 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 6, 0, 0, 0, 6, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 6, 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, 6, 0, 0, 0, 0, 6, 0, 0, 0, 6, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 6, 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, 6, 0, 0, 0, 0, 6, 0, 0, 0, 6, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 3 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 6, 0, 0, 0, 6, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 6, 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, 6, 0, 0, 0, 0, 6, 0, 0, 6, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 6, 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, 6, 0, 0, 0, 0, 6, 0, 0, 0, 6, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 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, 0, 0, 0, 0, 6, 0, 0, 0, 0, 6, 0, 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, 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, 6, 0, 0, 0, 0, 6, 0, 0, 6, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 6, 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, 6, 0, 0, 0, 0, 6, 0, 0, 6, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 6, 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, 6, 0, 0, 0, 0, 6, 0, 0, 6, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 11.3.2 Transition Removal

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

 0: 2 + 10⋅x2_0 − 10⋅x3_0 1: 10⋅x2_0 − 10⋅x3_0 2: 1 + 10⋅x2_0 − 10⋅x3_0 3: 4 + 10⋅x2_0 − 10⋅x3_0 4: −1 + 10⋅x2_0 − 10⋅x3_0 8: −4 9: −3 + 10⋅oldX2_post − 10⋅oldX3_post 3_var_snapshot: 3 + 10⋅x2_0 − 10⋅x3_0 3*: 5 + 10⋅x2_0 − 10⋅x3_0 4_var_snapshot: −2 + 10⋅x2_0 − 10⋅x3_0 4*: 10⋅x2_0 − 10⋅x3_0
Hints:
 35 lexWeak[ [0, 0, 0, 10, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 10, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 42 lexWeak[ [0, 0, 0, 10, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 44 lexWeak[ [0, 0, 0, 10, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10, 0, 0, 10, 0, 0, 0, 0, 0, 10, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10, 0, 0, 10, 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, 10, 0, 0, 10, 0, 0, 0, 0, 0, 10, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10, 0, 0, 10, 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, 10, 0, 0, 10, 0, 0, 0, 0, 0, 10, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 3 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10, 0, 0, 10, 0, 0, 0, 0, 0, 10, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 6 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, 10, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 10, 0, 0, 10, 0, 0, 0, 0, 10, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10, 0, 0, 10, 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, 10, 0, 0, 10, 0, 0, 0, 0, 10, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10, 0, 0, 10, 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, 10, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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.3.3 Transition Removal

We remove transition 3 using the following ranking functions, which are bounded by 7.

 0: 1 + 6⋅x0_0 − 6⋅x3_0 1: −1 + 6⋅x0_0 − 6⋅x3_0 2: 6⋅x0_0 − 6⋅x3_0 3: 3 + 6⋅x0_0 − 6⋅x3_0 4: 6⋅x0_0 − 6⋅x3_0 8: 0 9: −1 + 6⋅oldX0_post − 6⋅oldX3_post 3_var_snapshot: 2 + 6⋅x0_0 − 6⋅x3_0 3*: 4 + 6⋅x0_0 − 6⋅x3_0 4_var_snapshot: 6⋅x0_0 − 6⋅x3_0 4*: 1 + 6⋅x0_0 − 6⋅x3_0
Hints:
 35 lexWeak[ [0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0] ] 37 lexWeak[ [0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0] ] 42 lexWeak[ [0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0] ] 44 lexWeak[ [0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0] ] 0 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 6, 0, 6, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 6, 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, 6, 0, 0, 0, 0, 0, 0, 6, 0, 6, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 6, 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, 6, 0, 0, 0, 0, 0, 0, 6, 0, 6, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 6, 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, 6, 0, 0, 0, 0, 0, 0, 6, 0, 6, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 6, 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, 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, 6, 0, 0, 0, 0, 0, 0, 6, 6, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 6, 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, 6, 0, 0, 0, 0, 0, 0, 6, 6, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 6, 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, 6, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 11.3.4 Transition Removal

We remove transitions 35, 37, 44, 0, 1, 2, 15, 16, 17 using the following ranking functions, which are bounded by −7.

 0: 2 1: 0 2: 1 3: −2 4: −5 8: 0 9: −7 3_var_snapshot: −3 3*: −1 4_var_snapshot: −6 4*: −4
Hints:
 35 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] ] 37 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] ] 42 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] ] 44 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 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, 0, 0, 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 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, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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.3.5 Transition Removal

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

 0: 0 1: 0 2: 0 3: 0 4: 1 8: 0 9: 0 3_var_snapshot: 0 3*: 0 4_var_snapshot: 0 4*: 0
Hints:
 42 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] ]

### 11.3.6 Splitting Cut-Point Transitions

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

### 11.3.6.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 34.

### 11.3.6.1.1 Splitting Cut-Point Transitions

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

### 11.3.6.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 41.

### 11.3.6.2.1 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0