# LTS Termination Proof

by T2Cert

## Input

Integer Transition System
• Initial Location: 17
• Transitions: (pre-variables and post-variables)  0 0 1: 0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − i_0 + i_post ≤ 0 ∧ 1 + i_0 − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 0 1 2: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 3 2 4: 0 ≤ 0 ∧ 0 ≤ 0 ∧ edgecount_0 − i_0 ≤ 0 ∧ i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 3 3 0: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − edgecount_0 + i_0 ≤ 0 ∧ x_0 − x_post ≤ 0 ∧ − x_0 + x_post ≤ 0 ∧ y_0 − y_post ≤ 0 ∧ − y_0 + y_post ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 5 4 6: 0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − j_0 + j_post ≤ 0 ∧ 1 + j_0 − j_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 7 5 8: 0 ≤ 0 ∧ 0 ≤ 0 ∧ edgecount_0 − j_0 ≤ 0 ∧ −1 − i_0 + i_post ≤ 0 ∧ 1 + i_0 − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 7 6 5: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − edgecount_0 + j_0 ≤ 0 ∧ x_0 − x_post ≤ 0 ∧ − x_0 + x_post ≤ 0 ∧ y_0 − y_post ≤ 0 ∧ − y_0 + y_post ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 9 7 1: 0 ≤ 0 ∧ 0 ≤ 0 ∧ − i_0 + nodecount_0 ≤ 0 ∧ i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 9 8 6: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + i_0 − nodecount_0 ≤ 0 ∧ j_post ≤ 0 ∧ − j_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 10 9 11: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 11 10 12: 0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − i_0 + i_post ≤ 0 ∧ 1 + i_0 − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 13 11 10: 1 − i_0 + source_0 ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 13 12 10: 1 + i_0 − source_0 ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 13 13 11: i_0 − source_0 ≤ 0 ∧ − i_0 + source_0 ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 14 14 8: 0 ≤ 0 ∧ 0 ≤ 0 ∧ − i_0 + nodecount_0 ≤ 0 ∧ i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 14 15 13: 1 + i_0 − nodecount_0 ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 12 16 14: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 8 17 9: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 6 18 7: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 1 19 3: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 4 20 15: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 15 21 2: − i_0 + nodecount_0 ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 15 22 4: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + i_0 − nodecount_0 ≤ 0 ∧ −1 − i_0 + i_post ≤ 0 ∧ 1 + i_0 − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 16 23 12: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − ___const_5_0 + nodecount_post ≤ 0 ∧ ___const_5_0 − nodecount_post ≤ 0 ∧ − ___const_20_0 + edgecount_post ≤ 0 ∧ ___const_20_0 − edgecount_post ≤ 0 ∧ source_post ≤ 0 ∧ − source_post ≤ 0 ∧ i_post ≤ 0 ∧ − i_post ≤ 0 ∧ edgecount_0 − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ nodecount_0 − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_post ≤ 0 ∧ source_0 − source_post ≤ 0 ∧ − source_0 + source_post ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 17 24 16: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0

## Proof

The following invariants are asserted.

 0: source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 1: source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 2: source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 3: source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 4: source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 5: source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 6: source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 7: source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 8: source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 9: source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 10: source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 11: source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 12: source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 13: source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 14: source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 15: source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 16: TRUE 17: TRUE

The invariants are proved as follows.

### IMPACT Invariant Proof

• nodes (location) invariant:  0 (0) source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 1 (1) source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 2 (2) source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 3 (3) source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 4 (4) source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 5 (5) source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 6 (6) source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 7 (7) source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 8 (8) source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 9 (9) source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 10 (10) source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 11 (11) source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 12 (12) source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 13 (13) source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 14 (14) source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 15 (15) source_post ≤ 0 ∧ − source_post ≤ 0 ∧ − source_0 ≤ 0 16 (16) TRUE 17 (17) TRUE
• initial node: 17
• cover edges:
• transition edges:  0 0 1 0 1 2 1 19 3 3 2 4 3 3 0 4 20 15 5 4 6 6 18 7 7 5 8 7 6 5 8 17 9 9 7 1 9 8 6 10 9 11 11 10 12 12 16 14 13 11 10 13 12 10 13 13 11 14 14 8 14 15 13 15 21 2 15 22 4 16 23 12 17 24 16

### 2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 1 25 1: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 4 32 4: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 6 39 6: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 8 46 8: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 12 53 12: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0
and for every transition t, a duplicate t is considered.

### 3 Transition Removal

We remove transitions 1, 2, 7, 14, 21, 23, 24 using the following ranking functions, which are bounded by −27.

 17: 0 16: 0 10: 0 11: 0 12: 0 13: 0 14: 0 5: 0 6: 0 7: 0 8: 0 9: 0 0: 0 1: 0 3: 0 4: 0 15: 0 2: 0 17: −8 16: −9 10: −10 11: −10 12: −10 13: −10 14: −10 12_var_snapshot: −10 12*: −10 5: −11 6: −11 7: −11 8: −11 9: −11 6_var_snapshot: −11 6*: −11 8_var_snapshot: −11 8*: −11 0: −14 1: −14 3: −14 1_var_snapshot: −14 1*: −14 4: −15 15: −15 4_var_snapshot: −15 4*: −15 2: −16
Hints:
 26 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] ] 33 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] ] 40 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] ] 47 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] ] 54 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 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] ] 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] ] 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] ] 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] ] 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] ] 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] ] 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] ] 10 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 11 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 12 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 13 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 15 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 16 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 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] ] 18 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 19 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 22 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] ] 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] ] 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] ] 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] ] 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] ] 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] ] 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] ] 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] ]

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

1* 28 1: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_0 ≤ 0

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

1 26 1_var_snapshot: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_0 ≤ 0

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

4* 35 4: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_0 ≤ 0

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

4 33 4_var_snapshot: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_0 ≤ 0

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

6* 42 6: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_0 ≤ 0

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

6 40 6_var_snapshot: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_0 ≤ 0

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

8* 49 8: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_0 ≤ 0

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

8 47 8_var_snapshot: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_0 ≤ 0

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

12* 56 12: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_0 ≤ 0

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

12 54 12_var_snapshot: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0___const_5_0 + ___const_5_0 ≤ 0___const_5_0___const_5_0 ≤ 0___const_20_0 + ___const_20_0 ≤ 0___const_20_0___const_20_0 ≤ 0

### 14 SCC Decomposition

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

### 14.1 SCC Subproblem 1/4

Here we consider the SCC { 4, 15, 4_var_snapshot, 4* }.

### 14.1.1 Transition Removal

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

 4: 2 − 4⋅i_0 + 4⋅nodecount_0 15: −4⋅i_0 + 4⋅nodecount_0 4_var_snapshot: 1 − 4⋅i_0 + 4⋅nodecount_0 4*: 3 − 4⋅i_0 + 4⋅nodecount_0
Hints:
 33 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0] ] 35 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0] ] 20 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0] ] 22 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 4, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 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] ]

### 14.1.2 Transition Removal

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

 4: −1 15: −3 4_var_snapshot: −2 4*: 0
Hints:
 33 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] ] 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] ] 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] ]

### 14.1.3 Transition Removal

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

 4: 1 15: 0 4_var_snapshot: 0 4*: 0
Hints:
 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] ]

### 14.1.4 Splitting Cut-Point Transitions

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

### 14.1.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 32.

### 14.1.4.1.1 Splitting Cut-Point Transitions

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

### 14.2 SCC Subproblem 2/4

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

### 14.2.1 Transition Removal

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

 0: −2 + 4⋅edgecount_0 − 4⋅i_0 1: 1 + 4⋅edgecount_0 − 4⋅i_0 3: −1 + 4⋅edgecount_0 − 4⋅i_0 1_var_snapshot: 4⋅edgecount_0 − 4⋅i_0 1*: 2 + 4⋅edgecount_0 − 4⋅i_0
Hints:
 26 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, 4, 0, 0, 4, 0, 0, 0, 0, 0] ] 28 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, 4, 0, 0, 4, 0, 0, 0, 0, 0] ] 0 lexWeak[ [0, 0, 0, 0, 0, 0, 4, 0, 4, 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] ] 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, 4, 0, 0, 4, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 19 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 4, 0, 0, 0, 0, 0] ]

### 14.2.2 Transition Removal

We remove transitions 26, 28, 0, 19 using the following ranking functions, which are bounded by −4.

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

### 14.2.3 Splitting Cut-Point Transitions

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

### 14.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 25.

### 14.2.3.1.1 Splitting Cut-Point Transitions

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

### 14.3 SCC Subproblem 3/4

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

### 14.3.1 Transition Removal

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

 5: −5⋅i_0 + 5⋅nodecount_0 6: −5⋅i_0 + 5⋅nodecount_0 7: −5⋅i_0 + 5⋅nodecount_0 8: 3 − 5⋅i_0 + 5⋅nodecount_0 9: 1 − 5⋅i_0 + 5⋅nodecount_0 6_var_snapshot: −5⋅i_0 + 5⋅nodecount_0 6*: −5⋅i_0 + 5⋅nodecount_0 8_var_snapshot: 2 − 5⋅i_0 + 5⋅nodecount_0 8*: 4 − 5⋅i_0 + 5⋅nodecount_0
Hints:
 40 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 5, 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, 5, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0] ] 47 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 5, 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, 5, 0, 0, 0, 0, 0, 0, 0, 0, 5, 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, 5, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0] ] 5 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 5, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 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, 5, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0] ] 8 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 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] ] 17 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0] ] 18 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 14.3.2 Transition Removal

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

 5: −2 + 5⋅edgecount_0 − 5⋅j_0 6: 1 + 5⋅edgecount_0 − 5⋅j_0 7: −1 + 5⋅edgecount_0 − 5⋅j_0 8: −3 + 5⋅edgecount_0 − 5⋅j_0 9: −5 + 5⋅edgecount_0 − 5⋅j_0 6_var_snapshot: 5⋅edgecount_0 − 5⋅j_0 6*: 2 + 5⋅edgecount_0 − 5⋅j_0 8_var_snapshot: −4 + 5⋅edgecount_0 − 5⋅j_0 8*: −2 + 5⋅edgecount_0 − 5⋅j_0
Hints:
 40 lexWeak[ [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, 0, 0, 0, 0, 5, 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, 5, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0] ] 47 lexWeak[ [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, 0, 0, 0, 0, 5, 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, 5, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0] ] 4 lexWeak[ [0, 0, 0, 0, 0, 0, 5, 0, 5, 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, 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, 5, 0, 0, 5, 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, 5, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0] , [0, 0, 0, 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] ] 17 lexWeak[ [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, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0] ] 18 lexWeak[ [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, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0] ]

### 14.3.3 Transition Removal

We remove transitions 40, 42, 47, 49, 4, 5, 17, 18 using the following ranking functions, which are bounded by −5.

 5: 3 6: 1 7: −1 8: −3 9: −5 6_var_snapshot: 0 6*: 2 8_var_snapshot: −4 8*: −2
Hints:
 40 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] ] 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] ] 47 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] ] 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] ] 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] ] 5 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] ] 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] ] 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] ]

### 14.3.4 Splitting Cut-Point Transitions

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

### 14.3.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 39.

### 14.3.4.1.1 Splitting Cut-Point Transitions

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

### 14.3.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 46.

### 14.3.4.2.1 Splitting Cut-Point Transitions

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

### 14.4 SCC Subproblem 4/4

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

### 14.4.1 Transition Removal

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

 10: −3 − 7⋅i_0 + 7⋅source_0 11: −4 − 7⋅i_0 + 7⋅source_0 12: 1 − 7⋅i_0 + 7⋅source_0 13: −2 − 7⋅i_0 + 7⋅source_0 14: −1 − 7⋅i_0 + 7⋅source_0 12_var_snapshot: −7⋅i_0 + 7⋅source_0 12*: 2 − 7⋅i_0 + 7⋅source_0
Hints:
 54 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0] ] 56 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0] ] 9 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0] ] 10 lexWeak[ [0, 0, 0, 0, 0, 0, 7, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 11 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0] ] 12 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0] ] 16 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 14.4.2 Transition Removal

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

 10: −3 − 6⋅i_0 + 6⋅nodecount_0 11: −3 − 6⋅i_0 + 6⋅nodecount_0 12: 1 − 6⋅i_0 + 6⋅nodecount_0 13: −2 − 6⋅i_0 + 6⋅nodecount_0 14: −1 − 6⋅i_0 + 6⋅nodecount_0 12_var_snapshot: −6⋅i_0 + 6⋅nodecount_0 12*: 2 − 6⋅i_0 + 6⋅nodecount_0
Hints:
 54 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 6, 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, 6, 0, 0, 0, 0, 0, 0, 0, 0, 6, 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, 6, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0] ] 10 lexWeak[ [0, 0, 0, 0, 0, 0, 6, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 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, 6, 0, 0, 0, 0, 0, 0, 0, 0, 6, 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, 6, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 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] ] 16 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 14.4.3 Transition Removal

We remove transitions 54, 56, 10, 11, 16 using the following ranking functions, which are bounded by −6.

 10: −1 11: −2 12: −4 13: 0 14: −6 12_var_snapshot: −5 12*: −3
Hints:
 54 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] ] 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] ] 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] ] 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] ] 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, 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] ]

### 14.4.4 Transition Removal

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

 10: 1 11: 0 12: 0 13: 0 14: 0 12_var_snapshot: 0 12*: 0
Hints:
 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] ]

### 14.4.5 Splitting Cut-Point Transitions

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

### 14.4.5.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 53.

### 14.4.5.1.1 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0