LTS Termination Proof

by T2Cert

Input

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

  0	0	1:		___const_5_0 − i2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0
  0	1	2:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − ___const_5_0 + i2_0 ≤ 0 ∧ j3_post ≤ 0 ∧ − j3_post ≤ 0 ∧ j3_0 − j3_post ≤ 0 ∧ − j3_0 + j3_post ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0
  3	2	0:		− x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0
  2	3	4:		− x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0
  1	4	5:		− x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0
  6	5	7:		− x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0
  8	6	9:		0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − l5_0 + l5_post ≤ 0 ∧ 1 + l5_0 − l5_post ≤ 0 ∧ l5_0 − l5_post ≤ 0 ∧ − l5_0 + l5_post ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0
  9	7	10:		− x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0
  11	8	8:		− x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0
  11	9	1:		− x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0
  11	10	8:		− x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0
  10	11	6:		0 ≤ 0 ∧ 0 ≤ 0 ∧ ___const_5_0 − l5_0 ≤ 0 ∧ −1 − k4_0 + k4_post ≤ 0 ∧ 1 + k4_0 − k4_post ≤ 0 ∧ k4_0 − k4_post ≤ 0 ∧ − k4_0 + k4_post ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0
  10	12	11:		1 − ___const_5_0 + l5_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0
  7	13	2:		0 ≤ 0 ∧ 0 ≤ 0 ∧ ___const_5_0 − k4_0 ≤ 0 ∧ −1 − j3_0 + j3_post ≤ 0 ∧ 1 + j3_0 − j3_post ≤ 0 ∧ j3_0 − j3_post ≤ 0 ∧ − j3_0 + j3_post ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0
  7	14	9:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − ___const_5_0 + k4_0 ≤ 0 ∧ l5_post ≤ 0 ∧ − l5_post ≤ 0 ∧ l5_0 − l5_post ≤ 0 ∧ − l5_0 + l5_post ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0
  4	15	3:		0 ≤ 0 ∧ 0 ≤ 0 ∧ ___const_5_0 − j3_0 ≤ 0 ∧ −1 − i2_0 + i2_post ≤ 0 ∧ 1 + i2_0 − i2_post ≤ 0 ∧ i2_0 − i2_post ≤ 0 ∧ − i2_0 + i2_post ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0
  4	16	6:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − ___const_5_0 + j3_0 ≤ 0 ∧ k4_post ≤ 0 ∧ − k4_post ≤ 0 ∧ k4_0 − k4_post ≤ 0 ∧ − k4_0 + k4_post ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0
  12	17	3:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − ___const_400_0 + x1_post ≤ 0 ∧ ___const_400_0 − x1_post ≤ 0 ∧ i2_post ≤ 0 ∧ − i2_post ≤ 0 ∧ i2_0 − i2_post ≤ 0 ∧ − i2_0 + i2_post ≤ 0 ∧ x1_0 − x1_post ≤ 0 ∧ − x1_0 + x1_post ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0
  13	18	12:		− x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0

Proof

1 Switch to Cooperation Termination Proof

2 Transition Removal

We remove transitions 0, 4, 9, 17, 18 using the following ranking functions, which are bounded by −21.

3 Location Addition

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

2* 22 2: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0

4 Location Addition

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

2 20 2_var_snapshot: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0

5 Location Addition

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

3* 29 3: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0

6 Location Addition

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

3 27 3_var_snapshot: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0

7 Location Addition

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

6* 36 6: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0

8 Location Addition

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

6 34 6_var_snapshot: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0

9 Location Addition

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

9* 43 9: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0

10 Location Addition

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

9 41 9_var_snapshot: − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − l5_post + l5_post ≤ 0 ∧ l5_post − l5_post ≤ 0 ∧ − l5_0 + l5_0 ≤ 0 ∧ l5_0 − l5_0 ≤ 0 ∧ − k4_post + k4_post ≤ 0 ∧ k4_post − k4_post ≤ 0 ∧ − k4_0 + k4_0 ≤ 0 ∧ k4_0 − k4_0 ≤ 0 ∧ − j3_post + j3_post ≤ 0 ∧ j3_post − j3_post ≤ 0 ∧ − j3_0 + j3_0 ≤ 0 ∧ j3_0 − j3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0 ∧ − ___const_400_0 + ___const_400_0 ≤ 0 ∧ ___const_400_0 − ___const_400_0 ≤ 0

11 SCC Decomposition

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

11.1 SCC Subproblem 1/1

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

11.1.1 Transition Removal

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

11.1.2 Transition Removal

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

11.1.3 Transition Removal

We remove transitions 20, 22, 27, 29, 2, 3, 13, 15 using the following ranking functions, which are bounded by −3.

11.1.4 Transition Removal

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

11.1.5 Transition Removal

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

11.1.6 Transition Removal

We remove transitions 34, 36, 41, 43, 5, 6, 7, 8, 10, 11 using the following ranking functions, which are bounded by −3.

11.1.7 Splitting Cut-Point Transitions

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

11.1.7.1 Cut-Point Subproblem 1/4

11.1.7.1.1 Splitting Cut-Point Transitions

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

11.1.7.2 Cut-Point Subproblem 2/4

11.1.7.2.1 Splitting Cut-Point Transitions

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

11.1.7.3 Cut-Point Subproblem 3/4

11.1.7.3.1 Splitting Cut-Point Transitions

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

11.1.7.4 Cut-Point Subproblem 4/4

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