LTS Termination Proof

by T2Cert

Input

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

  0	0	1:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −2 + n17_post ≤ 0 ∧ 2 − n17_post ≤ 0 ∧ ret18_post − tmp19_post ≤ 0 ∧ − ret18_post + tmp19_post ≤ 0 ∧ − ret18_post + ret_fn120_post ≤ 0 ∧ ret18_post − ret_fn120_post ≤ 0 ∧ − ret_fn120_post + tmp_post ≤ 0 ∧ ret_fn120_post − tmp_post ≤ 0 ∧ i1_post − tmp_post ≤ 0 ∧ − i1_post + tmp_post ≤ 0 ∧ −2 + n21_post ≤ 0 ∧ 2 − n21_post ≤ 0 ∧ ret22_post − tmp23_post ≤ 0 ∧ − ret22_post + tmp23_post ≤ 0 ∧ − ret22_post + ret_fn124_post ≤ 0 ∧ ret22_post − ret_fn124_post ≤ 0 ∧ − ret_fn124_post + tmp___0_post ≤ 0 ∧ ret_fn124_post − tmp___0_post ≤ 0 ∧ i2_post − tmp___0_post ≤ 0 ∧ − i2_post + tmp___0_post ≤ 0 ∧ −2 + n25_post ≤ 0 ∧ 2 − n25_post ≤ 0 ∧ ret26_post − tmp27_post ≤ 0 ∧ − ret26_post + tmp27_post ≤ 0 ∧ − ret26_post + ret_fn128_post ≤ 0 ∧ ret26_post − ret_fn128_post ≤ 0 ∧ − ret_fn128_post + tmp___1_post ≤ 0 ∧ ret_fn128_post − tmp___1_post ≤ 0 ∧ i3_post − tmp___1_post ≤ 0 ∧ − i3_post + tmp___1_post ≤ 0 ∧ −2 + n29_post ≤ 0 ∧ 2 − n29_post ≤ 0 ∧ ret30_post − tmp31_post ≤ 0 ∧ − ret30_post + tmp31_post ≤ 0 ∧ − ret30_post + ret_fn132_post ≤ 0 ∧ ret30_post − ret_fn132_post ≤ 0 ∧ − ret_fn132_post + tmp___2_post ≤ 0 ∧ ret_fn132_post − tmp___2_post ≤ 0 ∧ i4_post − tmp___2_post ≤ 0 ∧ − i4_post + tmp___2_post ≤ 0 ∧ −2 + n33_post ≤ 0 ∧ 2 − n33_post ≤ 0 ∧ ret34_post − tmp35_post ≤ 0 ∧ − ret34_post + tmp35_post ≤ 0 ∧ − ret34_post + ret_fn136_post ≤ 0 ∧ ret34_post − ret_fn136_post ≤ 0 ∧ − ret_fn136_post + tmp___3_post ≤ 0 ∧ ret_fn136_post − tmp___3_post ≤ 0 ∧ i5_post − tmp___3_post ≤ 0 ∧ − i5_post + tmp___3_post ≤ 0 ∧ −2 + n37_post ≤ 0 ∧ 2 − n37_post ≤ 0 ∧ ret38_post − tmp39_post ≤ 0 ∧ − ret38_post + tmp39_post ≤ 0 ∧ − ret38_post + ret_fn140_post ≤ 0 ∧ ret38_post − ret_fn140_post ≤ 0 ∧ − ret_fn140_post + tmp___4_post ≤ 0 ∧ ret_fn140_post − tmp___4_post ≤ 0 ∧ i6_post − tmp___4_post ≤ 0 ∧ − i6_post + tmp___4_post ≤ 0 ∧ −2 + n41_post ≤ 0 ∧ 2 − n41_post ≤ 0 ∧ ret42_post − tmp43_post ≤ 0 ∧ − ret42_post + tmp43_post ≤ 0 ∧ − ret42_post + ret_fn144_post ≤ 0 ∧ ret42_post − ret_fn144_post ≤ 0 ∧ − ret_fn144_post + tmp___5_post ≤ 0 ∧ ret_fn144_post − tmp___5_post ≤ 0 ∧ i7_post − tmp___5_post ≤ 0 ∧ − i7_post + tmp___5_post ≤ 0 ∧ −2 + n45_post ≤ 0 ∧ 2 − n45_post ≤ 0 ∧ ret46_post − tmp47_post ≤ 0 ∧ − ret46_post + tmp47_post ≤ 0 ∧ − ret46_post + ret_fn148_post ≤ 0 ∧ ret46_post − ret_fn148_post ≤ 0 ∧ − ret_fn148_post + tmp___6_post ≤ 0 ∧ ret_fn148_post − tmp___6_post ≤ 0 ∧ i8_post − tmp___6_post ≤ 0 ∧ − i8_post + tmp___6_post ≤ 0 ∧ i1_0 − i1_post ≤ 0 ∧ − i1_0 + i1_post ≤ 0 ∧ i2_0 − i2_post ≤ 0 ∧ − i2_0 + i2_post ≤ 0 ∧ i3_0 − i3_post ≤ 0 ∧ − i3_0 + i3_post ≤ 0 ∧ i4_0 − i4_post ≤ 0 ∧ − i4_0 + i4_post ≤ 0 ∧ i5_0 − i5_post ≤ 0 ∧ − i5_0 + i5_post ≤ 0 ∧ i6_0 − i6_post ≤ 0 ∧ − i6_0 + i6_post ≤ 0 ∧ i7_0 − i7_post ≤ 0 ∧ − i7_0 + i7_post ≤ 0 ∧ i8_0 − i8_post ≤ 0 ∧ − i8_0 + i8_post ≤ 0 ∧ n17_0 − n17_post ≤ 0 ∧ − n17_0 + n17_post ≤ 0 ∧ n21_0 − n21_post ≤ 0 ∧ − n21_0 + n21_post ≤ 0 ∧ n25_0 − n25_post ≤ 0 ∧ − n25_0 + n25_post ≤ 0 ∧ n29_0 − n29_post ≤ 0 ∧ − n29_0 + n29_post ≤ 0 ∧ n33_0 − n33_post ≤ 0 ∧ − n33_0 + n33_post ≤ 0 ∧ n37_0 − n37_post ≤ 0 ∧ − n37_0 + n37_post ≤ 0 ∧ n41_0 − n41_post ≤ 0 ∧ − n41_0 + n41_post ≤ 0 ∧ n45_0 − n45_post ≤ 0 ∧ − n45_0 + n45_post ≤ 0 ∧ ret18_0 − ret18_post ≤ 0 ∧ − ret18_0 + ret18_post ≤ 0 ∧ ret22_0 − ret22_post ≤ 0 ∧ − ret22_0 + ret22_post ≤ 0 ∧ ret26_0 − ret26_post ≤ 0 ∧ − ret26_0 + ret26_post ≤ 0 ∧ ret30_0 − ret30_post ≤ 0 ∧ − ret30_0 + ret30_post ≤ 0 ∧ ret34_0 − ret34_post ≤ 0 ∧ − ret34_0 + ret34_post ≤ 0 ∧ ret38_0 − ret38_post ≤ 0 ∧ − ret38_0 + ret38_post ≤ 0 ∧ ret42_0 − ret42_post ≤ 0 ∧ − ret42_0 + ret42_post ≤ 0 ∧ ret46_0 − ret46_post ≤ 0 ∧ − ret46_0 + ret46_post ≤ 0 ∧ ret_fn120_0 − ret_fn120_post ≤ 0 ∧ − ret_fn120_0 + ret_fn120_post ≤ 0 ∧ ret_fn124_0 − ret_fn124_post ≤ 0 ∧ − ret_fn124_0 + ret_fn124_post ≤ 0 ∧ ret_fn128_0 − ret_fn128_post ≤ 0 ∧ − ret_fn128_0 + ret_fn128_post ≤ 0 ∧ ret_fn132_0 − ret_fn132_post ≤ 0 ∧ − ret_fn132_0 + ret_fn132_post ≤ 0 ∧ ret_fn136_0 − ret_fn136_post ≤ 0 ∧ − ret_fn136_0 + ret_fn136_post ≤ 0 ∧ ret_fn140_0 − ret_fn140_post ≤ 0 ∧ − ret_fn140_0 + ret_fn140_post ≤ 0 ∧ ret_fn144_0 − ret_fn144_post ≤ 0 ∧ − ret_fn144_0 + ret_fn144_post ≤ 0 ∧ ret_fn148_0 − ret_fn148_post ≤ 0 ∧ − ret_fn148_0 + ret_fn148_post ≤ 0 ∧ tmp19_0 − tmp19_post ≤ 0 ∧ − tmp19_0 + tmp19_post ≤ 0 ∧ tmp23_0 − tmp23_post ≤ 0 ∧ − tmp23_0 + tmp23_post ≤ 0 ∧ tmp27_0 − tmp27_post ≤ 0 ∧ − tmp27_0 + tmp27_post ≤ 0 ∧ tmp31_0 − tmp31_post ≤ 0 ∧ − tmp31_0 + tmp31_post ≤ 0 ∧ tmp35_0 − tmp35_post ≤ 0 ∧ − tmp35_0 + tmp35_post ≤ 0 ∧ tmp39_0 − tmp39_post ≤ 0 ∧ − tmp39_0 + tmp39_post ≤ 0 ∧ tmp43_0 − tmp43_post ≤ 0 ∧ − tmp43_0 + tmp43_post ≤ 0 ∧ tmp47_0 − tmp47_post ≤ 0 ∧ − tmp47_0 + tmp47_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 ∧ tmp___1_0 − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_post ≤ 0 ∧ tmp___2_0 − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_post ≤ 0 ∧ tmp___3_0 − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_post ≤ 0 ∧ tmp___4_0 − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_post ≤ 0 ∧ tmp___5_0 − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_post ≤ 0 ∧ tmp___6_0 − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_post ≤ 0
  2	1	0:		− tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___6_post + tmp___6_post ≤ 0 ∧ tmp___6_post − tmp___6_post ≤ 0 ∧ − tmp___6_0 + tmp___6_0 ≤ 0 ∧ tmp___6_0 − tmp___6_0 ≤ 0 ∧ − tmp___5_post + tmp___5_post ≤ 0 ∧ tmp___5_post − tmp___5_post ≤ 0 ∧ − tmp___5_0 + tmp___5_0 ≤ 0 ∧ tmp___5_0 − tmp___5_0 ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − tmp47_post + tmp47_post ≤ 0 ∧ tmp47_post − tmp47_post ≤ 0 ∧ − tmp47_0 + tmp47_0 ≤ 0 ∧ tmp47_0 − tmp47_0 ≤ 0 ∧ − tmp43_post + tmp43_post ≤ 0 ∧ tmp43_post − tmp43_post ≤ 0 ∧ − tmp43_0 + tmp43_0 ≤ 0 ∧ tmp43_0 − tmp43_0 ≤ 0 ∧ − tmp39_post + tmp39_post ≤ 0 ∧ tmp39_post − tmp39_post ≤ 0 ∧ − tmp39_0 + tmp39_0 ≤ 0 ∧ tmp39_0 − tmp39_0 ≤ 0 ∧ − tmp35_post + tmp35_post ≤ 0 ∧ tmp35_post − tmp35_post ≤ 0 ∧ − tmp35_0 + tmp35_0 ≤ 0 ∧ tmp35_0 − tmp35_0 ≤ 0 ∧ − tmp31_post + tmp31_post ≤ 0 ∧ tmp31_post − tmp31_post ≤ 0 ∧ − tmp31_0 + tmp31_0 ≤ 0 ∧ tmp31_0 − tmp31_0 ≤ 0 ∧ − tmp27_post + tmp27_post ≤ 0 ∧ tmp27_post − tmp27_post ≤ 0 ∧ − tmp27_0 + tmp27_0 ≤ 0 ∧ tmp27_0 − tmp27_0 ≤ 0 ∧ − tmp23_post + tmp23_post ≤ 0 ∧ tmp23_post − tmp23_post ≤ 0 ∧ − tmp23_0 + tmp23_0 ≤ 0 ∧ tmp23_0 − tmp23_0 ≤ 0 ∧ − tmp19_post + tmp19_post ≤ 0 ∧ tmp19_post − tmp19_post ≤ 0 ∧ − tmp19_0 + tmp19_0 ≤ 0 ∧ tmp19_0 − tmp19_0 ≤ 0 ∧ − ret_fn148_post + ret_fn148_post ≤ 0 ∧ ret_fn148_post − ret_fn148_post ≤ 0 ∧ − ret_fn148_0 + ret_fn148_0 ≤ 0 ∧ ret_fn148_0 − ret_fn148_0 ≤ 0 ∧ − ret_fn144_post + ret_fn144_post ≤ 0 ∧ ret_fn144_post − ret_fn144_post ≤ 0 ∧ − ret_fn144_0 + ret_fn144_0 ≤ 0 ∧ ret_fn144_0 − ret_fn144_0 ≤ 0 ∧ − ret_fn140_post + ret_fn140_post ≤ 0 ∧ ret_fn140_post − ret_fn140_post ≤ 0 ∧ − ret_fn140_0 + ret_fn140_0 ≤ 0 ∧ ret_fn140_0 − ret_fn140_0 ≤ 0 ∧ − ret_fn136_post + ret_fn136_post ≤ 0 ∧ ret_fn136_post − ret_fn136_post ≤ 0 ∧ − ret_fn136_0 + ret_fn136_0 ≤ 0 ∧ ret_fn136_0 − ret_fn136_0 ≤ 0 ∧ − ret_fn132_post + ret_fn132_post ≤ 0 ∧ ret_fn132_post − ret_fn132_post ≤ 0 ∧ − ret_fn132_0 + ret_fn132_0 ≤ 0 ∧ ret_fn132_0 − ret_fn132_0 ≤ 0 ∧ − ret_fn128_post + ret_fn128_post ≤ 0 ∧ ret_fn128_post − ret_fn128_post ≤ 0 ∧ − ret_fn128_0 + ret_fn128_0 ≤ 0 ∧ ret_fn128_0 − ret_fn128_0 ≤ 0 ∧ − ret_fn124_post + ret_fn124_post ≤ 0 ∧ ret_fn124_post − ret_fn124_post ≤ 0 ∧ − ret_fn124_0 + ret_fn124_0 ≤ 0 ∧ ret_fn124_0 − ret_fn124_0 ≤ 0 ∧ − ret_fn120_post + ret_fn120_post ≤ 0 ∧ ret_fn120_post − ret_fn120_post ≤ 0 ∧ − ret_fn120_0 + ret_fn120_0 ≤ 0 ∧ ret_fn120_0 − ret_fn120_0 ≤ 0 ∧ − ret46_post + ret46_post ≤ 0 ∧ ret46_post − ret46_post ≤ 0 ∧ − ret46_0 + ret46_0 ≤ 0 ∧ ret46_0 − ret46_0 ≤ 0 ∧ − ret42_post + ret42_post ≤ 0 ∧ ret42_post − ret42_post ≤ 0 ∧ − ret42_0 + ret42_0 ≤ 0 ∧ ret42_0 − ret42_0 ≤ 0 ∧ − ret38_post + ret38_post ≤ 0 ∧ ret38_post − ret38_post ≤ 0 ∧ − ret38_0 + ret38_0 ≤ 0 ∧ ret38_0 − ret38_0 ≤ 0 ∧ − ret34_post + ret34_post ≤ 0 ∧ ret34_post − ret34_post ≤ 0 ∧ − ret34_0 + ret34_0 ≤ 0 ∧ ret34_0 − ret34_0 ≤ 0 ∧ − ret30_post + ret30_post ≤ 0 ∧ ret30_post − ret30_post ≤ 0 ∧ − ret30_0 + ret30_0 ≤ 0 ∧ ret30_0 − ret30_0 ≤ 0 ∧ − ret26_post + ret26_post ≤ 0 ∧ ret26_post − ret26_post ≤ 0 ∧ − ret26_0 + ret26_0 ≤ 0 ∧ ret26_0 − ret26_0 ≤ 0 ∧ − ret22_post + ret22_post ≤ 0 ∧ ret22_post − ret22_post ≤ 0 ∧ − ret22_0 + ret22_0 ≤ 0 ∧ ret22_0 − ret22_0 ≤ 0 ∧ − ret18_post + ret18_post ≤ 0 ∧ ret18_post − ret18_post ≤ 0 ∧ − ret18_0 + ret18_0 ≤ 0 ∧ ret18_0 − ret18_0 ≤ 0 ∧ − n45_post + n45_post ≤ 0 ∧ n45_post − n45_post ≤ 0 ∧ − n45_0 + n45_0 ≤ 0 ∧ n45_0 − n45_0 ≤ 0 ∧ − n41_post + n41_post ≤ 0 ∧ n41_post − n41_post ≤ 0 ∧ − n41_0 + n41_0 ≤ 0 ∧ n41_0 − n41_0 ≤ 0 ∧ − n37_post + n37_post ≤ 0 ∧ n37_post − n37_post ≤ 0 ∧ − n37_0 + n37_0 ≤ 0 ∧ n37_0 − n37_0 ≤ 0 ∧ − n33_post + n33_post ≤ 0 ∧ n33_post − n33_post ≤ 0 ∧ − n33_0 + n33_0 ≤ 0 ∧ n33_0 − n33_0 ≤ 0 ∧ − n29_post + n29_post ≤ 0 ∧ n29_post − n29_post ≤ 0 ∧ − n29_0 + n29_0 ≤ 0 ∧ n29_0 − n29_0 ≤ 0 ∧ − n25_post + n25_post ≤ 0 ∧ n25_post − n25_post ≤ 0 ∧ − n25_0 + n25_0 ≤ 0 ∧ n25_0 − n25_0 ≤ 0 ∧ − n21_post + n21_post ≤ 0 ∧ n21_post − n21_post ≤ 0 ∧ − n21_0 + n21_0 ≤ 0 ∧ n21_0 − n21_0 ≤ 0 ∧ − n17_post + n17_post ≤ 0 ∧ n17_post − n17_post ≤ 0 ∧ − n17_0 + n17_0 ≤ 0 ∧ n17_0 − n17_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i6_post + i6_post ≤ 0 ∧ i6_post − i6_post ≤ 0 ∧ − i6_0 + i6_0 ≤ 0 ∧ i6_0 − i6_0 ≤ 0 ∧ − i5_post + i5_post ≤ 0 ∧ i5_post − i5_post ≤ 0 ∧ − i5_0 + i5_0 ≤ 0 ∧ i5_0 − i5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − i3_post + i3_post ≤ 0 ∧ i3_post − i3_post ≤ 0 ∧ − i3_0 + i3_0 ≤ 0 ∧ i3_0 − i3_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0 ∧ − i1_post + i1_post ≤ 0 ∧ i1_post − i1_post ≤ 0 ∧ − i1_0 + i1_0 ≤ 0 ∧ i1_0 − i1_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)		TRUE
  1		(1)		−2 + n17_post ≤ 0 ∧ 2 − n17_post ≤ 0 ∧ −2 + n21_post ≤ 0 ∧ 2 − n21_post ≤ 0 ∧ −2 + n25_post ≤ 0 ∧ 2 − n25_post ≤ 0 ∧ −2 + n29_post ≤ 0 ∧ 2 − n29_post ≤ 0 ∧ −2 + n33_post ≤ 0 ∧ 2 − n33_post ≤ 0 ∧ −2 + n37_post ≤ 0 ∧ 2 − n37_post ≤ 0 ∧ −2 + n41_post ≤ 0 ∧ 2 − n41_post ≤ 0 ∧ −2 + n45_post ≤ 0 ∧ 2 − n45_post ≤ 0 ∧ −2 + n17_0 ≤ 0 ∧ 2 − n17_0 ≤ 0 ∧ −2 + n21_0 ≤ 0 ∧ 2 − n21_0 ≤ 0 ∧ −2 + n25_0 ≤ 0 ∧ 2 − n25_0 ≤ 0 ∧ −2 + n29_0 ≤ 0 ∧ 2 − n29_0 ≤ 0 ∧ −2 + n33_0 ≤ 0 ∧ 2 − n33_0 ≤ 0 ∧ −2 + n37_0 ≤ 0 ∧ 2 − n37_0 ≤ 0 ∧ −2 + n41_0 ≤ 0 ∧ 2 − n41_0 ≤ 0 ∧ −2 + n45_0 ≤ 0 ∧ 2 − n45_0 ≤ 0
  2		(2)		TRUE

• initial node: 2
• cover edges:
• transition edges:

  0	0 1
  2	1 0

2 Switch to Cooperation Termination Proof

3 Transition Removal

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

4 SCC Decomposition

There exist no SCC in the program graph.

Tool configuration

T2Cert

• version: 1.0