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 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 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 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 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 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 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 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 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 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 9 10 4: 10 − 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 9 11 8: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −9 + 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 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 2 13 1: 10 − 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 2 14 3: 0 ≤ 0 ∧ 0 ≤ 0 ∧ −9 + 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 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 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

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 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
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

3 Location Addition

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

4 Location Addition

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

5 Location Addition

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

6 Location Addition

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

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 −73.

 6: −1 − 8⋅il_0 7: 2 − 8⋅il_0 8: −1 − 8⋅il_0 9: −8⋅il_0 7_var_snapshot: 1 − 8⋅il_0 7*: 3 − 8⋅il_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

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 −46.

 0: 1 − 5⋅il_0 2: −5⋅il_0 3: 3 − 5⋅il_0 3_var_snapshot: 2 − 5⋅il_0 3*: 4 − 5⋅il_0

7.2.2 Transition Removal

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

 0: −1 2: −2 3: 1 3_var_snapshot: 0 3*: 2

7.2.3 Splitting Cut-Point Transitions

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

7.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 17.

7.2.3.1.1 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0