# 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 ∧ 1 − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg1P + arg2 ≤ 0 ∧ arg1P − arg2 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 1 1 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arg1 − arg2P ≤ 0 ∧ − arg1 + arg2P ≤ 0 ∧ arg1 − arg3P ≤ 0 ∧ − arg1 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 2 2 1: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 100 − arg2 ≤ 0 ∧ arg2 − arg3 ≤ 0 ∧ − arg2 + arg3 ≤ 0 ∧ −1 − arg1P + arg1 ≤ 0 ∧ 1 + arg1P − arg1 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 2 3 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ −99 + arg2 ≤ 0 ∧ arg2 − arg3 ≤ 0 ∧ − arg2 + arg3 ≤ 0 ∧ 1 − arg2P + arg2 ≤ 0 ∧ −1 + arg2P − arg2 ≤ 0 ∧ 1 + arg2 − arg3P ≤ 0 ∧ −1 − arg2 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 2 4 3: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ −99 + arg2 ≤ 0 ∧ arg2 − arg3 ≤ 0 ∧ − arg2 + arg3 ≤ 0 ∧ − arg1P + arg2 ≤ 0 ∧ arg1P − arg2 ≤ 0 ∧ arg2 − arg3P ≤ 0 ∧ − arg2 + arg3P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 3 5 3: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ arg2 − arg3 ≤ 0 ∧ − arg2 + arg3 ≤ 0 ∧ −1 − arg2P + arg2 ≤ 0 ∧ 1 + arg2P − arg2 ≤ 0 ∧ −1 + arg2 − arg3P ≤ 0 ∧ 1 − arg2 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 3 6 4: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg2 ≤ 0 ∧ arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ arg3 ≤ 0 ∧ arg1 − arg2P ≤ 0 ∧ − arg1 + arg2P ≤ 0 ∧ arg1 − arg3P ≤ 0 ∧ − arg1 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 4 7 4: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ arg2 − arg3 ≤ 0 ∧ − arg2 + arg3 ≤ 0 ∧ −1 − arg2P + arg2 ≤ 0 ∧ 1 + arg2P − arg2 ≤ 0 ∧ −1 + arg2 − arg3P ≤ 0 ∧ 1 − arg2 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 4 8 5: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg2 ≤ 0 ∧ arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ arg3 ≤ 0 ∧ arg1 − arg2P ≤ 0 ∧ − arg1 + arg2P ≤ 0 ∧ arg1 − arg3P ≤ 0 ∧ − arg1 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 5 9 5: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ arg2 − arg3 ≤ 0 ∧ − arg2 + arg3 ≤ 0 ∧ −1 − arg2P + arg2 ≤ 0 ∧ 1 + arg2P − arg2 ≤ 0 ∧ −1 + arg2 − arg3P ≤ 0 ∧ 1 − arg2 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 5 10 6: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg2 ≤ 0 ∧ arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ arg3 ≤ 0 ∧ arg1 − arg2P ≤ 0 ∧ − arg1 + arg2P ≤ 0 ∧ arg1 − arg3P ≤ 0 ∧ − arg1 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 6 11 6: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ arg2 − arg3 ≤ 0 ∧ − arg2 + arg3 ≤ 0 ∧ −1 − arg2P + arg2 ≤ 0 ∧ 1 + arg2P − arg2 ≤ 0 ∧ −1 + arg2 − arg3P ≤ 0 ∧ 1 − arg2 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 6 12 7: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg2 ≤ 0 ∧ arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ arg3 ≤ 0 ∧ arg1 − arg2P ≤ 0 ∧ − arg1 + arg2P ≤ 0 ∧ arg1 − arg3P ≤ 0 ∧ − arg1 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 7 13 7: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ arg2 − arg3 ≤ 0 ∧ − arg2 + arg3 ≤ 0 ∧ −1 − arg2P + arg2 ≤ 0 ∧ 1 + arg2P − arg2 ≤ 0 ∧ −1 + arg2 − arg3P ≤ 0 ∧ 1 − arg2 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 7 14 8: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg2 ≤ 0 ∧ arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ arg3 ≤ 0 ∧ arg1 − arg2P ≤ 0 ∧ − arg1 + arg2P ≤ 0 ∧ arg1 − arg3P ≤ 0 ∧ − arg1 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 8 15 8: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ arg2 − arg3 ≤ 0 ∧ − arg2 + arg3 ≤ 0 ∧ −1 − arg2P + arg2 ≤ 0 ∧ 1 + arg2P − arg2 ≤ 0 ∧ −1 + arg2 − arg3P ≤ 0 ∧ 1 − arg2 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 8 16 9: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg2 ≤ 0 ∧ arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ arg3 ≤ 0 ∧ arg1 − arg2P ≤ 0 ∧ − arg1 + arg2P ≤ 0 ∧ arg1 − arg3P ≤ 0 ∧ − arg1 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 9 17 9: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ arg2 − arg3 ≤ 0 ∧ − arg2 + arg3 ≤ 0 ∧ −1 − arg2P + arg2 ≤ 0 ∧ 1 + arg2P − arg2 ≤ 0 ∧ −1 + arg2 − arg3P ≤ 0 ∧ 1 − arg2 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 9 18 10: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg2 ≤ 0 ∧ arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ arg3 ≤ 0 ∧ arg1 − arg2P ≤ 0 ∧ − arg1 + arg2P ≤ 0 ∧ arg1 − arg3P ≤ 0 ∧ − arg1 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 10 19 10: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ arg2 − arg3 ≤ 0 ∧ − arg2 + arg3 ≤ 0 ∧ −1 − arg2P + arg2 ≤ 0 ∧ 1 + arg2P − arg2 ≤ 0 ∧ −1 + arg2 − arg3P ≤ 0 ∧ 1 − arg2 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 10 20 11: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg2 ≤ 0 ∧ arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ arg3 ≤ 0 ∧ arg1 − arg2P ≤ 0 ∧ − arg1 + arg2P ≤ 0 ∧ arg1 − arg3P ≤ 0 ∧ − arg1 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 11 21 11: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ arg2 − arg3 ≤ 0 ∧ − arg2 + arg3 ≤ 0 ∧ −1 − arg2P + arg2 ≤ 0 ∧ 1 + arg2P − arg2 ≤ 0 ∧ −1 + arg2 − arg3P ≤ 0 ∧ 1 − arg2 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 11 22 12: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg2 ≤ 0 ∧ arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ arg3 ≤ 0 ∧ arg1 − arg2P ≤ 0 ∧ − arg1 + arg2P ≤ 0 ∧ arg1 − arg3P ≤ 0 ∧ − arg1 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 12 23 12: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ arg2 − arg3 ≤ 0 ∧ − arg2 + arg3 ≤ 0 ∧ −1 − arg2P + arg2 ≤ 0 ∧ 1 + arg2P − arg2 ≤ 0 ∧ −1 + arg2 − arg3P ≤ 0 ∧ 1 − arg2 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 12 24 13: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg2 ≤ 0 ∧ arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ arg3 ≤ 0 ∧ arg1 − arg2P ≤ 0 ∧ − arg1 + arg2P ≤ 0 ∧ arg1 − arg3P ≤ 0 ∧ − arg1 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 13 25 13: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ arg2 − arg3 ≤ 0 ∧ − arg2 + arg3 ≤ 0 ∧ −1 − arg2P + arg2 ≤ 0 ∧ 1 + arg2P − arg2 ≤ 0 ∧ −1 + arg2 − arg3P ≤ 0 ∧ 1 − arg2 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 13 26 14: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg2 ≤ 0 ∧ arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ arg3 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 14 27 14: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ −1 − arg1P + arg1 ≤ 0 ∧ 1 + arg1P − arg1 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 15 28 0: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0

## Proof

The following invariants are asserted.

 0: TRUE 1: TRUE 2: TRUE 3: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0 4: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0 5: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0 6: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0 7: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0 8: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0 9: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0 10: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0 11: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0 12: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0 13: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0 14: TRUE 15: TRUE

The invariants are proved as follows.

### IMPACT Invariant Proof

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

### 2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 1 29 1: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 2 36 2: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 3 43 3: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 4 50 4: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 5 57 5: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 6 64 6: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 7 71 7: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 8 78 8: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 9 85 9: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 10 92 10: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 11 99 11: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 12 106 12: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 13 113 13: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 14 120 14: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
and for every transition t, a duplicate t is considered.

### 3 Transition Removal

We remove transitions 0, 4, 6, 8, 10, 12, 14, 16, 18, 20, 22, 24, 26, 28 using the following ranking functions, which are bounded by −61.

 15: 0 0: 0 1: 0 2: 0 3: 0 4: 0 5: 0 6: 0 7: 0 8: 0 9: 0 10: 0 11: 0 12: 0 13: 0 14: 0 15: −16 0: −17 1: −18 2: −18 1_var_snapshot: −18 1*: −18 2_var_snapshot: −18 2*: −18 3: −21 3_var_snapshot: −21 3*: −21 4: −24 4_var_snapshot: −24 4*: −24 5: −27 5_var_snapshot: −27 5*: −27 6: −30 6_var_snapshot: −30 6*: −30 7: −33 7_var_snapshot: −33 7*: −33 8: −36 8_var_snapshot: −36 8*: −36 9: −39 9_var_snapshot: −39 9*: −39 10: −42 10_var_snapshot: −42 10*: −42 11: −45 11_var_snapshot: −45 11*: −45 12: −48 12_var_snapshot: −48 12*: −48 13: −51 13_var_snapshot: −51 13*: −51 14: −54 14_var_snapshot: −54 14*: −54
Hints:
 30 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 37 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 44 lexWeak[ [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] ] 58 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 65 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 72 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 79 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 86 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 93 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 100 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 107 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 114 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 121 lexWeak[ [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] ] 2 lexWeak[ [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] ] 5 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 7 lexWeak[ [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] ] 11 lexWeak[ [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] ] 15 lexWeak[ [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] ] 19 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 21 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 23 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 25 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 27 lexWeak[ [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] ] 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] ] 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, 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, 0, 0, 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] ] 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] ] 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] ] 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] ] 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] ] 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] ] 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] ] 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] ] 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] ] 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] ]

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

1* 32 1: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

1 30 1_var_snapshot: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

2* 39 2: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

2 37 2_var_snapshot: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

3* 46 3: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

3 44 3_var_snapshot: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

4* 53 4: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

4 51 4_var_snapshot: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

5* 60 5: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

5 58 5_var_snapshot: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

6* 67 6: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

6 65 6_var_snapshot: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

7* 74 7: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

7 72 7_var_snapshot: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

8* 81 8: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

8 79 8_var_snapshot: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

9* 88 9: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

9 86 9_var_snapshot: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

10* 95 10: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

10 93 10_var_snapshot: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

11* 102 11: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

11 100 11_var_snapshot: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

12* 109 12: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

12 107 12_var_snapshot: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

13* 116 13: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

13 114 13_var_snapshot: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

14* 123 14: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

14 121 14_var_snapshot: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

### 32 SCC Decomposition

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

### 32.1 SCC Subproblem 1/13

Here we consider the SCC { 14, 14_var_snapshot, 14* }.

### 32.1.1 Transition Removal

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

 14: 1 + 3⋅arg1 14_var_snapshot: 3⋅arg1 14*: 2 + 3⋅arg1
Hints:
 121 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0] ] 123 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0] ] 27 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 3, 3, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 32.1.2 Transition Removal

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

 14: 0 14_var_snapshot: −1 14*: 1
Hints:
 121 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] ] 123 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 32.1.3 Transition Removal

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

 14: 0 14_var_snapshot: 0 14*: 1
Hints:
 123 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] ]

### 32.1.4 Splitting Cut-Point Transitions

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

### 32.1.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 120.

### 32.1.4.1.1 Splitting Cut-Point Transitions

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

### 32.2 SCC Subproblem 2/13

Here we consider the SCC { 13, 13_var_snapshot, 13* }.

### 32.2.1 Transition Removal

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

 13: −1 + 2⋅arg2 + arg3 13_var_snapshot: −2 + 2⋅arg2 + arg3 13*: 2⋅arg2 + arg3
Hints:
 114 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 116 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 25 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 2, 0, 1, 2, 0, 1, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 3, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 32.2.2 Transition Removal

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

 13: 0 13_var_snapshot: −1 13*: 1
Hints:
 114 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] ] 116 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] ]

### 32.2.3 Splitting Cut-Point Transitions

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

### 32.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 113.

### 32.2.3.1.1 Splitting Cut-Point Transitions

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

### 32.3 SCC Subproblem 3/13

Here we consider the SCC { 12, 12_var_snapshot, 12* }.

### 32.3.1 Transition Removal

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

 12: −1 + 2⋅arg2 + arg3 12_var_snapshot: −2 + 2⋅arg2 + arg3 12*: 2⋅arg2 + arg3
Hints:
 107 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 109 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 23 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 2, 0, 1, 2, 0, 1, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 3, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 32.3.2 Transition Removal

We remove transitions 107, 109 using the following ranking functions, which are bounded by −2.

 12: −1 12_var_snapshot: −2 12*: 0
Hints:
 107 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] ] 109 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] ]

### 32.3.3 Splitting Cut-Point Transitions

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

### 32.3.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 106.

### 32.3.3.1.1 Splitting Cut-Point Transitions

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

### 32.4 SCC Subproblem 4/13

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

### 32.4.1 Transition Removal

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

 11: 1 + 2⋅arg2 + arg3 11_var_snapshot: 2⋅arg2 + arg3 11*: 2 + 2⋅arg2 + arg3
Hints:
 100 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 102 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 21 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 2, 0, 1, 2, 0, 1, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 3, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 32.4.2 Transition Removal

We remove transitions 100, 102 using the following ranking functions, which are bounded by −2.

 11: −1 11_var_snapshot: −2 11*: 0
Hints:
 100 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] ] 102 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] ]

### 32.4.3 Splitting Cut-Point Transitions

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

### 32.4.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 99.

### 32.4.3.1.1 Splitting Cut-Point Transitions

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

### 32.5 SCC Subproblem 5/13

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

### 32.5.1 Transition Removal

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

 10: −1 + 2⋅arg2 + arg3 10_var_snapshot: −2 + 2⋅arg2 + arg3 10*: 2⋅arg2 + arg3
Hints:
 93 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 95 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 19 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 2, 0, 1, 2, 0, 1, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 3, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 32.5.2 Transition Removal

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

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

### 32.5.3 Splitting Cut-Point Transitions

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

### 32.5.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 92.

### 32.5.3.1.1 Splitting Cut-Point Transitions

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

### 32.6 SCC Subproblem 6/13

Here we consider the SCC { 9, 9_var_snapshot, 9* }.

### 32.6.1 Transition Removal

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

 9: 1 + 2⋅arg2 + arg3 9_var_snapshot: 2⋅arg2 + arg3 9*: 2 + 2⋅arg2 + arg3
Hints:
 86 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 88 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 17 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 2, 0, 1, 2, 0, 1, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 3, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 32.6.2 Transition Removal

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

 9: 0 9_var_snapshot: −1 9*: 1
Hints:
 86 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] ] 88 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] ]

### 32.6.3 Splitting Cut-Point Transitions

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

### 32.6.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 85.

### 32.6.3.1.1 Splitting Cut-Point Transitions

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

### 32.7 SCC Subproblem 7/13

Here we consider the SCC { 8, 8_var_snapshot, 8* }.

### 32.7.1 Transition Removal

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

 8: 1 + 2⋅arg2 + arg3 8_var_snapshot: 2⋅arg2 + arg3 8*: 2 + 2⋅arg2 + arg3
Hints:
 79 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 81 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 15 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 2, 0, 1, 2, 0, 1, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 3, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 32.7.2 Transition Removal

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

 8: 0 8_var_snapshot: −1 8*: 1
Hints:
 79 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] ] 81 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] ]

### 32.7.3 Splitting Cut-Point Transitions

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

### 32.7.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 78.

### 32.7.3.1.1 Splitting Cut-Point Transitions

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

### 32.8 SCC Subproblem 8/13

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

### 32.8.1 Transition Removal

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

 7: 1 + 2⋅arg2 + arg3 7_var_snapshot: 2⋅arg2 + arg3 7*: 2 + 2⋅arg2 + arg3
Hints:
 72 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 74 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 13 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 2, 0, 1, 2, 0, 1, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 3, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 32.8.2 Transition Removal

We remove transitions 72, 74 using the following ranking functions, which are bounded by −2.

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

### 32.8.3 Splitting Cut-Point Transitions

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

### 32.8.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 71.

### 32.8.3.1.1 Splitting Cut-Point Transitions

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

### 32.9 SCC Subproblem 9/13

Here we consider the SCC { 6, 6_var_snapshot, 6* }.

### 32.9.1 Transition Removal

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

 6: −1 + 2⋅arg2 + arg3 6_var_snapshot: −2 + 2⋅arg2 + arg3 6*: 2⋅arg2 + arg3
Hints:
 65 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 67 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 11 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 2, 0, 1, 2, 0, 1, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 3, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 32.9.2 Transition Removal

We remove transitions 65, 67 using the following ranking functions, which are bounded by −2.

 6: −1 6_var_snapshot: −2 6*: 0
Hints:
 65 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] ] 67 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] ]

### 32.9.3 Splitting Cut-Point Transitions

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

### 32.9.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 64.

### 32.9.3.1.1 Splitting Cut-Point Transitions

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

### 32.10 SCC Subproblem 10/13

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

### 32.10.1 Transition Removal

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

 5: −1 + 2⋅arg2 + arg3 5_var_snapshot: −2 + 2⋅arg2 + arg3 5*: 2⋅arg2 + arg3
Hints:
 58 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 60 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 9 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 2, 0, 1, 2, 0, 1, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 3, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 32.10.2 Transition Removal

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

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

### 32.10.3 Splitting Cut-Point Transitions

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

### 32.10.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 57.

### 32.10.3.1.1 Splitting Cut-Point Transitions

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

### 32.11 SCC Subproblem 11/13

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

### 32.11.1 Transition Removal

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

 4: 1 + 2⋅arg2 + arg3 4_var_snapshot: 2⋅arg2 + arg3 4*: 2 + 2⋅arg2 + arg3
Hints:
 51 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 53 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 7 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 2, 0, 1, 2, 0, 1, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 3, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 32.11.2 Transition Removal

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

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

### 32.11.3 Splitting Cut-Point Transitions

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

### 32.11.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 50.

### 32.11.3.1.1 Splitting Cut-Point Transitions

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

### 32.12 SCC Subproblem 12/13

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

### 32.12.1 Transition Removal

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

 3: 1 + 2⋅arg2 + arg3 3_var_snapshot: 2⋅arg2 + arg3 3*: 2 + 2⋅arg2 + arg3
Hints:
 44 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 46 lexWeak[ [0, 0, 0, 0, 1, 0, 0, 0, 2, 0, 0, 0, 0, 0] ] 5 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 2, 0, 1, 2, 0, 1, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 3, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 32.12.2 Transition Removal

We remove transitions 44, 46 using the following ranking functions, which are bounded by −2.

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

### 32.12.3 Splitting Cut-Point Transitions

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

### 32.12.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 43.

### 32.12.3.1.1 Splitting Cut-Point Transitions

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

### 32.13 SCC Subproblem 13/13

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

### 32.13.1 Transition Removal

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

 1: 2 + 4⋅arg1 2: 4⋅arg1 1_var_snapshot: 1 + 4⋅arg1 1*: 3 + 4⋅arg1 2_var_snapshot: 4⋅arg1 2*: 4⋅arg1
Hints:
 30 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0] ] 32 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0] ] 37 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0] ] 39 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0] ] 1 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0] ] 2 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 4, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 4, 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, 4, 0] ]

### 32.13.2 Transition Removal

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

 1: 3 − 3⋅arg1 2: 1 − arg2 − 2⋅arg3 1_var_snapshot: 3 − 3⋅arg1 1*: 4 − 3⋅arg1 2_var_snapshot: − arg2 − 2⋅arg3 2*: 2 − arg2 − 2⋅arg3
Hints:
 30 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3] ] 32 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3] ] 37 lexWeak[ [0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 0] ] 39 lexWeak[ [0, 0, 0, 2, 0, 0, 0, 1, 0, 0, 0, 0] ] 1 lexWeak[ [0, 0, 0, 0, 1, 0, 2, 0, 0, 1, 0, 2, 0, 0, 0, 0] ] 3 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 2, 1, 0, 2, 0, 0, 1, 0, 2, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 3, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 32.13.3 Transition Removal

We remove transitions 30, 37, 39, 1 using the following ranking functions, which are bounded by −3.

 1: 1 2: −2 1_var_snapshot: 0 1*: 2 2_var_snapshot: −3 2*: −1
Hints:
 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] ] 32 lexWeak[ [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] ] 39 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] ] 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] ]

### 32.13.4 Transition Removal

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

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

### 32.13.5 Splitting Cut-Point Transitions

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

### 32.13.5.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 29.

### 32.13.5.1.1 Splitting Cut-Point Transitions

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

### 32.13.5.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 36.

### 32.13.5.2.1 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0