LTS Termination Proof

by T2Cert

Input

• Initial Location: 14
• Transitions: (pre-variables and post-variables)

  0	0	1:		− 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0
  2	1	3:		___const_50_0 − i_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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0
  2	2	4:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − ___const_50_0 + i_0 ≤ 0 ∧ −1 − i_0 + i_post ≤ 0 ∧ 1 + i_0 − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 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 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0
  5	3	6:		− 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0
  7	4	4:		0 ≤ 0 ∧ 0 ≤ 0 ∧ ___const_50_0 − i13_0 ≤ 0 ∧ i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 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 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0
  7	5	8:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − ___const_50_0 + i13_0 ≤ 0 ∧ −1 − i13_0 + i13_post ≤ 0 ∧ 1 + i13_0 − i13_post ≤ 0 ∧ i13_0 − i13_post ≤ 0 ∧ − i13_0 + i13_post ≤ 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0
  9	6	10:		− 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0
  11	7	8:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ ___const_50_0 − i11_0 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0 ∧ i13_post ≤ 0 ∧ − i13_post ≤ 0 ∧ i13_0 − i13_post ≤ 0 ∧ − i13_0 + i13_post ≤ 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0
  11	8	12:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − ___const_50_0 + i11_0 ≤ 0 ∧ −1 − i11_0 + i11_post ≤ 0 ∧ 1 + i11_0 − i11_post ≤ 0 ∧ i11_0 − i11_post ≤ 0 ∧ − i11_0 + i11_post ≤ 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0
  12	9	11:		− 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0
  10	10	12:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ ___const_50_0 − i_0 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i11_post ≤ 0 ∧ − i11_post ≤ 0 ∧ i11_0 − i11_post ≤ 0 ∧ − i11_0 + i11_post ≤ 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0
  10	11	9:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − ___const_50_0 + i_0 ≤ 0 ∧ −1 − i_0 + i_post ≤ 0 ∧ 1 + i_0 − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 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 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0
  8	12	7:		− 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0
  6	13	9:		0 ≤ 0 ∧ 0 ≤ 0 ∧ ___const_50_0 − i9_0 ≤ 0 ∧ i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 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 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0
  6	14	5:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − ___const_50_0 + i9_0 ≤ 0 ∧ −1 − i9_0 + i9_post ≤ 0 ∧ 1 + i9_0 − i9_post ≤ 0 ∧ i9_0 − i9_post ≤ 0 ∧ − i9_0 + i9_post ≤ 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0
  4	15	2:		− 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0
  1	16	5:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ ___const_50_0 − i7_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i9_post ≤ 0 ∧ − i9_post ≤ 0 ∧ i9_0 − i9_post ≤ 0 ∧ − i9_0 + i9_post ≤ 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0
  1	17	0:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − ___const_50_0 + i7_0 ≤ 0 ∧ −1 − i7_0 + i7_post ≤ 0 ∧ 1 + i7_0 − i7_post ≤ 0 ∧ i7_0 − i7_post ≤ 0 ∧ − i7_0 + i7_post ≤ 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0
  13	18	0:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i7_post ≤ 0 ∧ − i7_post ≤ 0 ∧ i7_0 − i7_post ≤ 0 ∧ − i7_0 + i7_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ tmp_0 − tmp_post ≤ 0 ∧ − tmp_0 + tmp_post ≤ 0 ∧ tmp___0_0 − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_post ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0
  14	19	13:		− 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0

Proof

1 Invariant Updates

The following invariants are asserted.

The invariants are proved as follows.

IMPACT Invariant Proof

• nodes (location) invariant:

  0		(0)		i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0
  1		(1)		i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0
  2		(2)		i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0
  3		(3)		i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0
  4		(4)		i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0
  5		(5)		i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0
  6		(6)		i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0
  7		(7)		i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0
  8		(8)		i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0
  9		(9)		i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0
  10		(10)		i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0
  11		(11)		i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0
  12		(12)		i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0
  13		(13)		TRUE
  14		(14)		TRUE

• initial node: 14
• cover edges:
• transition edges:

  0	0 1
  1	16 5
  1	17 0
  2	1 3
  2	2 4
  4	15 2
  5	3 6
  6	13 9
  6	14 5
  7	4 4
  7	5 8
  8	12 7
  9	6 10
  10	10 12
  10	11 9
  11	7 8
  11	8 12
  12	9 11
  13	18 0
  14	19 13

2 Switch to Cooperation Termination Proof

3 Transition Removal

We remove transitions 1, 4, 7, 10, 13, 16, 18, 19 using the following ranking functions, which are bounded by −33.

4 Location Addition

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

0* 23 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0

5 Location Addition

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

0 21 0_var_snapshot: − 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0

6 Location Addition

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

4* 30 4: − 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0

7 Location Addition

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

4 28 4_var_snapshot: − 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0

8 Location Addition

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

5* 37 5: − 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0

9 Location Addition

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

5 35 5_var_snapshot: − 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0

10 Location Addition

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

8* 44 8: − 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0

11 Location Addition

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

8 42 8_var_snapshot: − 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0

12 Location Addition

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

9* 51 9: − 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0

13 Location Addition

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

9 49 9_var_snapshot: − 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0

14 Location Addition

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

12* 58 12: − 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0

15 Location Addition

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

12 56 12_var_snapshot: − 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 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0 ∧ − ___const_50_0 + ___const_50_0 ≤ 0 ∧ ___const_50_0 − ___const_50_0 ≤ 0

16 SCC Decomposition

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

16.1 SCC Subproblem 1/6

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

16.1.1 Transition Removal

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

16.1.2 Transition Removal

We remove transitions 28, 30, 15 using the following ranking functions, which are bounded by −1.

16.1.3 Splitting Cut-Point Transitions

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

16.1.3.1 Cut-Point Subproblem 1/1

16.1.3.1.1 Splitting Cut-Point Transitions

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

16.2 SCC Subproblem 2/6

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

16.2.1 Transition Removal

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

16.2.2 Transition Removal

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

16.2.3 Splitting Cut-Point Transitions

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

16.2.3.1 Cut-Point Subproblem 1/1

16.2.3.1.1 Splitting Cut-Point Transitions

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

16.3 SCC Subproblem 3/6

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

16.3.1 Transition Removal

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

16.3.2 Transition Removal

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

16.3.3 Transition Removal

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

16.3.4 Splitting Cut-Point Transitions

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

16.3.4.1 Cut-Point Subproblem 1/1

16.3.4.1.1 Splitting Cut-Point Transitions

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

16.4 SCC Subproblem 4/6

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

16.4.1 Transition Removal

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

16.4.2 Transition Removal

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

16.4.3 Transition Removal

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

16.4.4 Splitting Cut-Point Transitions

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

16.4.4.1 Cut-Point Subproblem 1/1

16.4.4.1.1 Splitting Cut-Point Transitions

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

16.5 SCC Subproblem 5/6

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

16.5.1 Transition Removal

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

16.5.2 Transition Removal

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

16.5.3 Splitting Cut-Point Transitions

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

16.5.3.1 Cut-Point Subproblem 1/1

16.5.3.1.1 Splitting Cut-Point Transitions

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

16.6 SCC Subproblem 6/6

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

16.6.1 Transition Removal

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

16.6.2 Transition Removal

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

16.6.3 Transition Removal

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

16.6.4 Splitting Cut-Point Transitions

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

16.6.4.1 Cut-Point Subproblem 1/1

16.6.4.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert

• version: 1.0