LTS Termination Proof

by T2Cert

Input

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

  0	0	1:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − Index2_0 + ___const_100_0 ≤ 0 ∧ Sorted5_post ≤ 0 ∧ − Sorted5_post ≤ 0 ∧ −1 + i8_post ≤ 0 ∧ 1 − i8_post ≤ 0 ∧ Sorted5_0 − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_post ≤ 0 ∧ i8_0 − i8_post ≤ 0 ∧ − i8_0 + i8_post ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
  0	1	2:		0 ≤ 0 ∧ 0 ≤ 0 ∧ Index2_0 − ___const_100_0 ≤ 0 ∧ −1 − Index2_0 + Index2_post ≤ 0 ∧ 1 + Index2_0 − Index2_post ≤ 0 ∧ Index2_0 − Index2_post ≤ 0 ∧ − Index2_0 + Index2_post ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0
  2	2	0:		− i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
  3	3	4:		− i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
  5	4	3:		− i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
  6	5	7:		− i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
  7	6	1:		0 ≤ 0 ∧ 0 ≤ 0 ∧ Sorted5_0 ≤ 0 ∧ − Sorted5_0 ≤ 0 ∧ −1 − i8_0 + i8_post ≤ 0 ∧ 1 + i8_0 − i8_post ≤ 0 ∧ i8_0 − i8_post ≤ 0 ∧ − i8_0 + i8_post ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
  7	7	5:		1 − Sorted5_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
  7	8	5:		1 + Sorted5_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
  8	9	9:		0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − Index7_0 + Index7_post ≤ 0 ∧ 1 + Index7_0 − Index7_post ≤ 0 ∧ Index7_0 − Index7_post ≤ 0 ∧ − Index7_0 + Index7_post ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
  1	10	10:		− i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
  11	11	8:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ Sorted5_post ≤ 0 ∧ − Sorted5_post ≤ 0 ∧ Sorted5_0 − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_post ≤ 0 ∧ Temp6_0 − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_post ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
  11	12	8:		− i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
  12	13	11:		Index7_0 − ___const_100_0 + i8_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
  12	14	6:		1 − Index7_0 + ___const_100_0 − i8_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
  13	15	6:		1 − Index7_0 + ___const_99_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
  13	16	12:		Index7_0 − ___const_99_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
  9	17	13:		− i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
  10	18	3:		1 + ___const_99_0 − i8_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
  10	19	9:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − ___const_99_0 + i8_0 ≤ 0 ∧ −1 + Sorted5_post ≤ 0 ∧ 1 − Sorted5_post ≤ 0 ∧ −1 + Index7_post ≤ 0 ∧ 1 − Index7_post ≤ 0 ∧ Index7_0 − Index7_post ≤ 0 ∧ − Index7_0 + Index7_post ≤ 0 ∧ Sorted5_0 − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_post ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
  14	20	2:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ fact3_post − factor_post ≤ 0 ∧ − fact3_post + factor_post ≤ 0 ∧ −1 + Index2_post ≤ 0 ∧ 1 − Index2_post ≤ 0 ∧ Index2_0 − Index2_post ≤ 0 ∧ − Index2_0 + Index2_post ≤ 0 ∧ fact3_0 − fact3_post ≤ 0 ∧ − fact3_0 + fact3_post ≤ 0 ∧ factor_0 − factor_post ≤ 0 ∧ − factor_0 + factor_post ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0
  15	21	14:		− i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_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)		1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
  1		(1)		1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 ∧ Sorted5_0 ≤ 0 ∧ − Sorted5_0 ≤ 0
  2		(2)		1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
  3		(3)		1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
  4		(4)		1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
  5		(5)		1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
  6		(6)		1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
  7		(7)		1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
  8		(8)		1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
  9		(9)		1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
  10		(10)		1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 ∧ Sorted5_0 ≤ 0 ∧ − Sorted5_0 ≤ 0
  11		(11)		1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
  12		(12)		1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
  13		(13)		1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
  14		(14)		TRUE
  15		(15)		TRUE

• initial node: 15
• cover edges:
• transition edges:

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

2 Switch to Cooperation Termination Proof

3 Transition Removal

We remove transitions 0, 3, 4, 7, 8, 18, 20, 21 using the following ranking functions, which are bounded by −23.

4 Location Addition

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

1* 25 1: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0

5 Location Addition

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

1 23 1_var_snapshot: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0

6 Location Addition

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

2* 32 2: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0

7 Location Addition

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

2 30 2_var_snapshot: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0

8 Location Addition

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

9* 39 9: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0

9 Location Addition

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

9 37 9_var_snapshot: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − ___const_99_0 + ___const_99_0 ≤ 0 ∧ ___const_99_0 − ___const_99_0 ≤ 0 ∧ − ___const_100_0 + ___const_100_0 ≤ 0 ∧ ___const_100_0 − ___const_100_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0

10 SCC Decomposition

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

10.1 SCC Subproblem 1/2

Here we consider the SCC { 1, 6, 7, 8, 9, 10, 11, 12, 13, 1_var_snapshot, 1*, 9_var_snapshot, 9* }.

10.1.1 Transition Removal

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

10.1.2 Transition Removal

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

10.1.3 Transition Removal

We remove transitions 23, 25, 37, 39, 5, 6, 9, 10, 11, 12, 13, 14, 15, 17 using the following ranking functions, which are bounded by −6.

10.1.4 Splitting Cut-Point Transitions

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

10.1.4.1 Cut-Point Subproblem 1/2

10.1.4.1.1 Splitting Cut-Point Transitions

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

10.1.4.2 Cut-Point Subproblem 2/2

10.1.4.2.1 Splitting Cut-Point Transitions

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

10.2 SCC Subproblem 2/2

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

10.2.1 Transition Removal

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

10.2.2 Transition Removal

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

10.2.3 Splitting Cut-Point Transitions

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

10.2.3.1 Cut-Point Subproblem 1/1

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