# LTS Termination Proof

by T2Cert

## Input

Integer Transition System
• Initial Location: 11
• Transitions: (pre-variables and post-variables)  0 0 1: tmp_0 ≤ 0 ∧ − tmp_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_foo7_post + ret_foo7_post ≤ 0 ∧ ret_foo7_post − ret_foo7_post ≤ 0 ∧ − ret_foo7_0 + ret_foo7_0 ≤ 0 ∧ ret_foo7_0 − ret_foo7_0 ≤ 0 ∧ − ret_foo5_post + ret_foo5_post ≤ 0 ∧ ret_foo5_post − ret_foo5_post ≤ 0 ∧ − ret_foo5_0 + ret_foo5_0 ≤ 0 ∧ ret_foo5_0 − ret_foo5_0 ≤ 0 ∧ − il_post + il_post ≤ 0 ∧ il_post − il_post ≤ 0 ∧ − il_0 + il_0 ≤ 0 ∧ il_0 − il_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 0 1 2: 1 − tmp_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_foo7_post + ret_foo7_post ≤ 0 ∧ ret_foo7_post − ret_foo7_post ≤ 0 ∧ − ret_foo7_0 + ret_foo7_0 ≤ 0 ∧ ret_foo7_0 − ret_foo7_0 ≤ 0 ∧ − ret_foo5_post + ret_foo5_post ≤ 0 ∧ ret_foo5_post − ret_foo5_post ≤ 0 ∧ − ret_foo5_0 + ret_foo5_0 ≤ 0 ∧ ret_foo5_0 − ret_foo5_0 ≤ 0 ∧ − il_post + il_post ≤ 0 ∧ il_post − il_post ≤ 0 ∧ − il_0 + il_0 ≤ 0 ∧ il_0 − il_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 0 2 2: 1 + tmp_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_foo7_post + ret_foo7_post ≤ 0 ∧ ret_foo7_post − ret_foo7_post ≤ 0 ∧ − ret_foo7_0 + ret_foo7_0 ≤ 0 ∧ ret_foo7_0 − ret_foo7_0 ≤ 0 ∧ − ret_foo5_post + ret_foo5_post ≤ 0 ∧ ret_foo5_post − ret_foo5_post ≤ 0 ∧ − ret_foo5_0 + ret_foo5_0 ≤ 0 ∧ ret_foo5_0 − ret_foo5_0 ≤ 0 ∧ − il_post + il_post ≤ 0 ∧ il_post − il_post ≤ 0 ∧ − il_0 + il_0 ≤ 0 ∧ il_0 − il_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 3 3 0: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − il_0 + x4_post ≤ 0 ∧ il_0 − x4_post ≤ 0 ∧ − ret_foo5_post + tmp_post ≤ 0 ∧ ret_foo5_post − tmp_post ≤ 0 ∧ ret_foo5_0 − ret_foo5_post ≤ 0 ∧ − ret_foo5_0 + ret_foo5_post ≤ 0 ∧ tmp_0 − tmp_post ≤ 0 ∧ − tmp_0 + tmp_post ≤ 0 ∧ x4_0 − x4_post ≤ 0 ∧ − x4_0 + x4_post ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − ret_foo7_post + ret_foo7_post ≤ 0 ∧ ret_foo7_post − ret_foo7_post ≤ 0 ∧ − ret_foo7_0 + ret_foo7_0 ≤ 0 ∧ ret_foo7_0 − ret_foo7_0 ≤ 0 ∧ − il_post + il_post ≤ 0 ∧ il_post − il_post ≤ 0 ∧ − il_0 + il_0 ≤ 0 ∧ il_0 − il_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 4 4 5: − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_foo7_post + ret_foo7_post ≤ 0 ∧ ret_foo7_post − ret_foo7_post ≤ 0 ∧ − ret_foo7_0 + ret_foo7_0 ≤ 0 ∧ ret_foo7_0 − ret_foo7_0 ≤ 0 ∧ − ret_foo5_post + ret_foo5_post ≤ 0 ∧ ret_foo5_post − ret_foo5_post ≤ 0 ∧ − ret_foo5_0 + ret_foo5_0 ≤ 0 ∧ ret_foo5_0 − ret_foo5_0 ≤ 0 ∧ − il_post + il_post ≤ 0 ∧ il_post − il_post ≤ 0 ∧ − il_0 + il_0 ≤ 0 ∧ il_0 − il_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 6 5 7: 0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − il_0 + il_post ≤ 0 ∧ 1 + il_0 − il_post ≤ 0 ∧ il_0 − il_post ≤ 0 ∧ − il_0 + il_post ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_foo7_post + ret_foo7_post ≤ 0 ∧ ret_foo7_post − ret_foo7_post ≤ 0 ∧ − ret_foo7_0 + ret_foo7_0 ≤ 0 ∧ ret_foo7_0 − ret_foo7_0 ≤ 0 ∧ − ret_foo5_post + ret_foo5_post ≤ 0 ∧ ret_foo5_post − ret_foo5_post ≤ 0 ∧ − ret_foo5_0 + ret_foo5_0 ≤ 0 ∧ ret_foo5_0 − ret_foo5_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 8 6 4: tmp___0_0 ≤ 0 ∧ − tmp___0_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_foo7_post + ret_foo7_post ≤ 0 ∧ ret_foo7_post − ret_foo7_post ≤ 0 ∧ − ret_foo7_0 + ret_foo7_0 ≤ 0 ∧ ret_foo7_0 − ret_foo7_0 ≤ 0 ∧ − ret_foo5_post + ret_foo5_post ≤ 0 ∧ ret_foo5_post − ret_foo5_post ≤ 0 ∧ − ret_foo5_0 + ret_foo5_0 ≤ 0 ∧ ret_foo5_0 − ret_foo5_0 ≤ 0 ∧ − il_post + il_post ≤ 0 ∧ il_post − il_post ≤ 0 ∧ − il_0 + il_0 ≤ 0 ∧ il_0 − il_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 8 7 6: 1 − tmp___0_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_foo7_post + ret_foo7_post ≤ 0 ∧ ret_foo7_post − ret_foo7_post ≤ 0 ∧ − ret_foo7_0 + ret_foo7_0 ≤ 0 ∧ ret_foo7_0 − ret_foo7_0 ≤ 0 ∧ − ret_foo5_post + ret_foo5_post ≤ 0 ∧ ret_foo5_post − ret_foo5_post ≤ 0 ∧ − ret_foo5_0 + ret_foo5_0 ≤ 0 ∧ ret_foo5_0 − ret_foo5_0 ≤ 0 ∧ − il_post + il_post ≤ 0 ∧ il_post − il_post ≤ 0 ∧ − il_0 + il_0 ≤ 0 ∧ il_0 − il_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 8 8 6: 1 + tmp___0_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_foo7_post + ret_foo7_post ≤ 0 ∧ ret_foo7_post − ret_foo7_post ≤ 0 ∧ − ret_foo7_0 + ret_foo7_0 ≤ 0 ∧ ret_foo7_0 − ret_foo7_0 ≤ 0 ∧ − ret_foo5_post + ret_foo5_post ≤ 0 ∧ ret_foo5_post − ret_foo5_post ≤ 0 ∧ − ret_foo5_0 + ret_foo5_0 ≤ 0 ∧ ret_foo5_0 − ret_foo5_0 ≤ 0 ∧ − il_post + il_post ≤ 0 ∧ il_post − il_post ≤ 0 ∧ − il_0 + il_0 ≤ 0 ∧ il_0 − il_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 7 9 9: − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_foo7_post + ret_foo7_post ≤ 0 ∧ ret_foo7_post − ret_foo7_post ≤ 0 ∧ − ret_foo7_0 + ret_foo7_0 ≤ 0 ∧ ret_foo7_0 − ret_foo7_0 ≤ 0 ∧ − ret_foo5_post + ret_foo5_post ≤ 0 ∧ ret_foo5_post − ret_foo5_post ≤ 0 ∧ − ret_foo5_0 + ret_foo5_0 ≤ 0 ∧ ret_foo5_0 − ret_foo5_0 ≤ 0 ∧ − il_post + il_post ≤ 0 ∧ il_post − il_post ≤ 0 ∧ − il_0 + il_0 ≤ 0 ∧ il_0 − il_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 9 10 4: ___const_10_0 − il_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_foo7_post + ret_foo7_post ≤ 0 ∧ ret_foo7_post − ret_foo7_post ≤ 0 ∧ − ret_foo7_0 + ret_foo7_0 ≤ 0 ∧ ret_foo7_0 − ret_foo7_0 ≤ 0 ∧ − ret_foo5_post + ret_foo5_post ≤ 0 ∧ ret_foo5_post − ret_foo5_post ≤ 0 ∧ − ret_foo5_0 + ret_foo5_0 ≤ 0 ∧ ret_foo5_0 − ret_foo5_0 ≤ 0 ∧ − il_post + il_post ≤ 0 ∧ il_post − il_post ≤ 0 ∧ − il_0 + il_0 ≤ 0 ∧ il_0 − il_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 9 11 8: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − ___const_10_0 + il_0 ≤ 0 ∧ − il_0 + x6_post ≤ 0 ∧ il_0 − x6_post ≤ 0 ∧ − ret_foo7_post + tmp___0_post ≤ 0 ∧ ret_foo7_post − tmp___0_post ≤ 0 ∧ ret_foo7_0 − ret_foo7_post ≤ 0 ∧ − ret_foo7_0 + ret_foo7_post ≤ 0 ∧ tmp___0_0 − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_post ≤ 0 ∧ x6_0 − x6_post ≤ 0 ∧ − x6_0 + x6_post ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_foo5_post + ret_foo5_post ≤ 0 ∧ ret_foo5_post − ret_foo5_post ≤ 0 ∧ − ret_foo5_0 + ret_foo5_0 ≤ 0 ∧ ret_foo5_0 − ret_foo5_0 ≤ 0 ∧ − il_post + il_post ≤ 0 ∧ il_post − il_post ≤ 0 ∧ − il_0 + il_0 ≤ 0 ∧ il_0 − il_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 1 12 7: 0 ≤ 0 ∧ 0 ≤ 0 ∧ il_post ≤ 0 ∧ − il_post ≤ 0 ∧ il_0 − il_post ≤ 0 ∧ − il_0 + il_post ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_foo7_post + ret_foo7_post ≤ 0 ∧ ret_foo7_post − ret_foo7_post ≤ 0 ∧ − ret_foo7_0 + ret_foo7_0 ≤ 0 ∧ ret_foo7_0 − ret_foo7_0 ≤ 0 ∧ − ret_foo5_post + ret_foo5_post ≤ 0 ∧ ret_foo5_post − ret_foo5_post ≤ 0 ∧ − ret_foo5_0 + ret_foo5_0 ≤ 0 ∧ ret_foo5_0 − ret_foo5_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 2 13 1: ___const_10_0 − il_0 ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_foo7_post + ret_foo7_post ≤ 0 ∧ ret_foo7_post − ret_foo7_post ≤ 0 ∧ − ret_foo7_0 + ret_foo7_0 ≤ 0 ∧ ret_foo7_0 − ret_foo7_0 ≤ 0 ∧ − ret_foo5_post + ret_foo5_post ≤ 0 ∧ ret_foo5_post − ret_foo5_post ≤ 0 ∧ − ret_foo5_0 + ret_foo5_0 ≤ 0 ∧ ret_foo5_0 − ret_foo5_0 ≤ 0 ∧ − il_post + il_post ≤ 0 ∧ il_post − il_post ≤ 0 ∧ − il_0 + il_0 ≤ 0 ∧ il_0 − il_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 2 14 3: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − ___const_10_0 + il_0 ≤ 0 ∧ −1 − il_0 + il_post ≤ 0 ∧ 1 + il_0 − il_post ≤ 0 ∧ il_0 − il_post ≤ 0 ∧ − il_0 + il_post ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_foo7_post + ret_foo7_post ≤ 0 ∧ ret_foo7_post − ret_foo7_post ≤ 0 ∧ − ret_foo7_0 + ret_foo7_0 ≤ 0 ∧ ret_foo7_0 − ret_foo7_0 ≤ 0 ∧ − ret_foo5_post + ret_foo5_post ≤ 0 ∧ ret_foo5_post − ret_foo5_post ≤ 0 ∧ − ret_foo5_0 + ret_foo5_0 ≤ 0 ∧ ret_foo5_0 − ret_foo5_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 10 15 3: 0 ≤ 0 ∧ 0 ≤ 0 ∧ il_post ≤ 0 ∧ − il_post ≤ 0 ∧ il_0 − il_post ≤ 0 ∧ − il_0 + il_post ≤ 0 ∧ − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_foo7_post + ret_foo7_post ≤ 0 ∧ ret_foo7_post − ret_foo7_post ≤ 0 ∧ − ret_foo7_0 + ret_foo7_0 ≤ 0 ∧ ret_foo7_0 − ret_foo7_0 ≤ 0 ∧ − ret_foo5_post + ret_foo5_post ≤ 0 ∧ ret_foo5_post − ret_foo5_post ≤ 0 ∧ − ret_foo5_0 + ret_foo5_0 ≤ 0 ∧ ret_foo5_0 − ret_foo5_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 11 16 10: − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_foo7_post + ret_foo7_post ≤ 0 ∧ ret_foo7_post − ret_foo7_post ≤ 0 ∧ − ret_foo7_0 + ret_foo7_0 ≤ 0 ∧ ret_foo7_0 − ret_foo7_0 ≤ 0 ∧ − ret_foo5_post + ret_foo5_post ≤ 0 ∧ ret_foo5_post − ret_foo5_post ≤ 0 ∧ − ret_foo5_0 + ret_foo5_0 ≤ 0 ∧ ret_foo5_0 − ret_foo5_0 ≤ 0 ∧ − il_post + il_post ≤ 0 ∧ il_post − il_post ≤ 0 ∧ − il_0 + il_0 ≤ 0 ∧ il_0 − il_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0

## Proof

### 1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 3 17 3: − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_foo7_post + ret_foo7_post ≤ 0 ∧ ret_foo7_post − ret_foo7_post ≤ 0 ∧ − ret_foo7_0 + ret_foo7_0 ≤ 0 ∧ ret_foo7_0 − ret_foo7_0 ≤ 0 ∧ − ret_foo5_post + ret_foo5_post ≤ 0 ∧ ret_foo5_post − ret_foo5_post ≤ 0 ∧ − ret_foo5_0 + ret_foo5_0 ≤ 0 ∧ ret_foo5_0 − ret_foo5_0 ≤ 0 ∧ − il_post + il_post ≤ 0 ∧ il_post − il_post ≤ 0 ∧ − il_0 + il_0 ≤ 0 ∧ il_0 − il_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0 7 24 7: − x6_post + x6_post ≤ 0 ∧ x6_post − x6_post ≤ 0 ∧ − x6_0 + x6_0 ≤ 0 ∧ x6_0 − x6_0 ≤ 0 ∧ − x4_post + x4_post ≤ 0 ∧ x4_post − x4_post ≤ 0 ∧ − x4_0 + x4_0 ≤ 0 ∧ x4_0 − x4_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_foo7_post + ret_foo7_post ≤ 0 ∧ ret_foo7_post − ret_foo7_post ≤ 0 ∧ − ret_foo7_0 + ret_foo7_0 ≤ 0 ∧ ret_foo7_0 − ret_foo7_0 ≤ 0 ∧ − ret_foo5_post + ret_foo5_post ≤ 0 ∧ ret_foo5_post − ret_foo5_post ≤ 0 ∧ − ret_foo5_0 + ret_foo5_0 ≤ 0 ∧ ret_foo5_0 − ret_foo5_0 ≤ 0 ∧ − il_post + il_post ≤ 0 ∧ il_post − il_post ≤ 0 ∧ − il_0 + il_0 ≤ 0 ∧ il_0 − il_0 ≤ 0 ∧ − ___const_10_0 + ___const_10_0 ≤ 0 ∧ ___const_10_0 − ___const_10_0 ≤ 0
and for every transition t, a duplicate t is considered.

### 2 Transition Removal

We remove transitions 0, 4, 6, 10, 12, 13, 15, 16 using the following ranking functions, which are bounded by −21.

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

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

3* 20 3: x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0ret_foo7_post + ret_foo7_post ≤ 0ret_foo7_postret_foo7_post ≤ 0ret_foo7_0 + ret_foo7_0 ≤ 0ret_foo7_0ret_foo7_0 ≤ 0ret_foo5_post + ret_foo5_post ≤ 0ret_foo5_postret_foo5_post ≤ 0ret_foo5_0 + ret_foo5_0 ≤ 0ret_foo5_0ret_foo5_0 ≤ 0il_post + il_post ≤ 0il_postil_post ≤ 0il_0 + il_0 ≤ 0il_0il_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0

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

3 18 3_var_snapshot: x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0ret_foo7_post + ret_foo7_post ≤ 0ret_foo7_postret_foo7_post ≤ 0ret_foo7_0 + ret_foo7_0 ≤ 0ret_foo7_0ret_foo7_0 ≤ 0ret_foo5_post + ret_foo5_post ≤ 0ret_foo5_postret_foo5_post ≤ 0ret_foo5_0 + ret_foo5_0 ≤ 0ret_foo5_0ret_foo5_0 ≤ 0il_post + il_post ≤ 0il_postil_post ≤ 0il_0 + il_0 ≤ 0il_0il_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0

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

7* 27 7: x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0ret_foo7_post + ret_foo7_post ≤ 0ret_foo7_postret_foo7_post ≤ 0ret_foo7_0 + ret_foo7_0 ≤ 0ret_foo7_0ret_foo7_0 ≤ 0ret_foo5_post + ret_foo5_post ≤ 0ret_foo5_postret_foo5_post ≤ 0ret_foo5_0 + ret_foo5_0 ≤ 0ret_foo5_0ret_foo5_0 ≤ 0il_post + il_post ≤ 0il_postil_post ≤ 0il_0 + il_0 ≤ 0il_0il_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0

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

7 25 7_var_snapshot: x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0ret_foo7_post + ret_foo7_post ≤ 0ret_foo7_postret_foo7_post ≤ 0ret_foo7_0 + ret_foo7_0 ≤ 0ret_foo7_0ret_foo7_0 ≤ 0ret_foo5_post + ret_foo5_post ≤ 0ret_foo5_postret_foo5_post ≤ 0ret_foo5_0 + ret_foo5_0 ≤ 0ret_foo5_0ret_foo5_0 ≤ 0il_post + il_post ≤ 0il_postil_post ≤ 0il_0 + il_0 ≤ 0il_0il_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0

### 7 SCC Decomposition

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

### 7.1 SCC Subproblem 1/2

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

### 7.1.1 Transition Removal

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

 6: −4 + 7⋅___const_10_0 − 7⋅il_0 7: 2 + 7⋅___const_10_0 − 7⋅il_0 8: −1 + 7⋅___const_10_0 − 7⋅il_0 9: 7⋅___const_10_0 − 7⋅il_0 7_var_snapshot: 1 + 7⋅___const_10_0 − 7⋅il_0 7*: 2 + 7⋅___const_10_0 − 7⋅il_0
Hints:
 25 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, 7, 7, 0] ] 27 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, 7, 7, 0] ] 5 lexWeak[ [0, 0, 0, 7, 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, 7, 0] ] 7 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, 7, 7, 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, 7, 7, 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, 7, 7, 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, 7, 7, 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] ]

### 7.1.2 Transition Removal

We remove transitions 25, 27, 5, 7, 8, 9 using the following ranking functions, which are bounded by −5.

 6: −1 7: −3 8: 0 9: −5 7_var_snapshot: −4 7*: −2
Hints:
 25 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 27 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 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] ] 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] ] 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 9 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 7.1.3 Splitting Cut-Point Transitions

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

### 7.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 24.

### 7.1.3.1.1 Splitting Cut-Point Transitions

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

### 7.2 SCC Subproblem 2/2

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

### 7.2.1 Transition Removal

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

 0: 1 + 5⋅___const_10_0 − 5⋅il_0 2: 5⋅___const_10_0 − 5⋅il_0 3: 3 + 5⋅___const_10_0 − 5⋅il_0 3_var_snapshot: 2 + 5⋅___const_10_0 − 5⋅il_0 3*: 4 + 5⋅___const_10_0 − 5⋅il_0
Hints:
 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, 5, 5, 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, 5, 5, 0] ] 1 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 5, 0] ] 2 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 5, 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, 5, 5, 0] ] 14 lexStrict[ [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, 0, 0, 5, 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] ]

### 7.2.2 Transition Removal

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

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

### 7.2.3 Transition Removal

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

 0: tmp_0 2: 0 3: 0 3_var_snapshot: 0 3*: 0
Hints:
 1 lexStrict[ [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

### 7.2.4 Splitting Cut-Point Transitions

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

### 7.2.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 17.

### 7.2.4.1.1 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0