LTS Termination Proof

by T2Cert

Input

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

  0	0	1:		− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0
  2	1	3:		− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0
  4	2	5:		−1 + N6_0 − j7_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0
  4	3	6:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 2 − N6_0 + j7_0 ≤ 0 ∧ −1 − j7_0 + j7_post ≤ 0 ∧ 1 + j7_0 − j7_post ≤ 0 ∧ j7_0 − j7_post ≤ 0 ∧ − j7_0 + j7_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0
  7	4	8:		− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0
  9	5	7:		0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − i8_0 + i8_post ≤ 0 ∧ 1 + i8_0 − i8_post ≤ 0 ∧ i8_0 − i8_post ≤ 0 ∧ − i8_0 + i8_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0
  10	6	9:		0 ≤ 0 ∧ 0 ≤ 0 ∧ − i8_0 + min9_post ≤ 0 ∧ i8_0 − min9_post ≤ 0 ∧ min9_0 − min9_post ≤ 0 ∧ − min9_0 + min9_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0
  10	7	9:		− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0
  8	8	2:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ N6_0 − i8_0 ≤ 0 ∧ −1 − j7_0 + j7_post ≤ 0 ∧ 1 + j7_0 − j7_post ≤ 0 ∧ j7_0 − j7_post ≤ 0 ∧ − j7_0 + j7_post ≤ 0 ∧ t10_0 − t10_post ≤ 0 ∧ − t10_0 + t10_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0
  8	9	10:		1 − N6_0 + i8_0 ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0
  6	10	4:		− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0
  3	11	6:		0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 + N6_0 − j7_0 ≤ 0 ∧ j7_post ≤ 0 ∧ − j7_post ≤ 0 ∧ j7_0 − j7_post ≤ 0 ∧ − j7_0 + j7_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0
  3	12	7:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 2 − N6_0 + j7_0 ≤ 0 ∧ − j7_0 + min9_post ≤ 0 ∧ j7_0 − min9_post ≤ 0 ∧ −1 + i8_post − j7_0 ≤ 0 ∧ 1 − i8_post + j7_0 ≤ 0 ∧ i8_0 − i8_post ≤ 0 ∧ − i8_0 + i8_post ≤ 0 ∧ min9_0 − min9_post ≤ 0 ∧ − min9_0 + min9_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0
  1	13	2:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ N_0 − i_0 ≤ 0 ∧ N6_post − N_0 ≤ 0 ∧ − N6_post + N_0 ≤ 0 ∧ j7_post ≤ 0 ∧ − j7_post ≤ 0 ∧ N6_0 − N6_post ≤ 0 ∧ − N6_0 + N6_post ≤ 0 ∧ j7_0 − j7_post ≤ 0 ∧ − j7_0 + j7_post ≤ 0 ∧ − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0
  1	14	0:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − N_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 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0
  11	15	0:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ tmp_0 − tmp_post ≤ 0 ∧ − tmp_0 + tmp_post ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0
  12	16	11:		− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0

Proof

1 Switch to Cooperation Termination Proof

2 Transition Removal

We remove transitions 2, 11, 13, 15, 16 using the following ranking functions, which are bounded by −23.

3 Location Addition

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

0* 20 0: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0

4 Location Addition

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

0 18 0_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0

5 Location Addition

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

2* 27 2: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0

6 Location Addition

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

2 25 2_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0

7 Location Addition

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

6* 34 6: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0

8 Location Addition

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

6 32 6_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0

9 Location Addition

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

7* 41 7: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0

10 Location Addition

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

7 39 7_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0

11 SCC Decomposition

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

11.1 SCC Subproblem 1/3

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

11.1.1 Transition Removal

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

11.1.2 Transition Removal

We remove transitions 32, 34, 10 using the following ranking functions, which are bounded by −1.

11.1.3 Splitting Cut-Point Transitions

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

11.1.3.1 Cut-Point Subproblem 1/1

11.1.3.1.1 Splitting Cut-Point Transitions

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

11.2 SCC Subproblem 2/3

Here we consider the SCC { 2, 3, 7, 8, 9, 10, 2_var_snapshot, 2*, 7_var_snapshot, 7* }.

11.2.1 Transition Removal

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

11.2.2 Transition Removal

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

11.2.3 Transition Removal

We remove transitions 25, 27, 39, 41, 1, 4, 5, 6, 7, 8 using the following ranking functions, which are bounded by −3.

11.2.4 Splitting Cut-Point Transitions

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

11.2.4.1 Cut-Point Subproblem 1/2

11.2.4.1.1 Splitting Cut-Point Transitions

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

11.2.4.2 Cut-Point Subproblem 2/2

11.2.4.2.1 Splitting Cut-Point Transitions

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

11.3 SCC Subproblem 3/3

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

11.3.1 Transition Removal

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

11.3.2 Transition Removal

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

11.3.3 Splitting Cut-Point Transitions

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

11.3.3.1 Cut-Point Subproblem 1/1

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