LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
1 67 1: tresh_post + tresh_post ≤ 0tresh_posttresh_post ≤ 0tresh_0 + tresh_0 ≤ 0tresh_0tresh_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___9_post + tmp___9_post ≤ 0tmp___9_posttmp___9_post ≤ 0tmp___9_0 + tmp___9_0 ≤ 0tmp___9_0tmp___9_0 ≤ 0tmp___8_post + tmp___8_post ≤ 0tmp___8_posttmp___8_post ≤ 0tmp___8_0 + tmp___8_0 ≤ 0tmp___8_0tmp___8_0 ≤ 0tmp___7_post + tmp___7_post ≤ 0tmp___7_posttmp___7_post ≤ 0tmp___7_0 + tmp___7_0 ≤ 0tmp___7_0tmp___7_0 ≤ 0tmp___6_post + tmp___6_post ≤ 0tmp___6_posttmp___6_post ≤ 0tmp___6_0 + tmp___6_0 ≤ 0tmp___6_0tmp___6_0 ≤ 0tmp___5_post + tmp___5_post ≤ 0tmp___5_posttmp___5_post ≤ 0tmp___5_0 + tmp___5_0 ≤ 0tmp___5_0tmp___5_0 ≤ 0tmp___4_post + tmp___4_post ≤ 0tmp___4_posttmp___4_post ≤ 0tmp___4_0 + tmp___4_0 ≤ 0tmp___4_0tmp___4_0 ≤ 0tmp___3_post + tmp___3_post ≤ 0tmp___3_posttmp___3_post ≤ 0tmp___3_0 + tmp___3_0 ≤ 0tmp___3_0tmp___3_0 ≤ 0tmp___2_post + tmp___2_post ≤ 0tmp___2_posttmp___2_post ≤ 0tmp___2_0 + tmp___2_0 ≤ 0tmp___2_0tmp___2_0 ≤ 0tmp___1_post + tmp___1_post ≤ 0tmp___1_posttmp___1_post ≤ 0tmp___1_0 + tmp___1_0 ≤ 0tmp___1_0tmp___1_0 ≤ 0tmp___11_post + tmp___11_post ≤ 0tmp___11_posttmp___11_post ≤ 0tmp___11_0 + tmp___11_0 ≤ 0tmp___11_0tmp___11_0 ≤ 0tmp___10_post + tmp___10_post ≤ 0tmp___10_posttmp___10_post ≤ 0tmp___10_0 + tmp___10_0 ≤ 0tmp___10_0tmp___10_0 ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0theta_post + theta_post ≤ 0theta_posttheta_post ≤ 0theta_0 + theta_0 ≤ 0theta_0theta_0 ≤ 0tau_post + tau_post ≤ 0tau_posttau_post ≤ 0tau_0 + tau_0 ≤ 0tau_0tau_0 ≤ 0t_post + t_post ≤ 0t_postt_post ≤ 0t_0 + t_0 ≤ 0t_0t_0 ≤ 0sm_post + sm_post ≤ 0sm_postsm_post ≤ 0sm_0 + sm_0 ≤ 0sm_0sm_0 ≤ 0s_post + s_post ≤ 0s_posts_post ≤ 0s_0 + s_0 ≤ 0s_0s_0 ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0iq_post + iq_post ≤ 0iq_postiq_post ≤ 0iq_0 + iq_0 ≤ 0iq_0iq_0 ≤ 0ip_post + ip_post ≤ 0ip_postip_post ≤ 0ip_0 + ip_0 ≤ 0ip_0ip_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0h_post + h_post ≤ 0h_posth_post ≤ 0h_0 + h_0 ≤ 0h_0h_0 ≤ 0g_post + g_post ≤ 0g_postg_post ≤ 0g_0 + g_0 ≤ 0g_0g_0 ≤ 0c_post + c_post ≤ 0c_postc_post ≤ 0c_0 + c_0 ≤ 0c_0c_0 ≤ 0___const_50_0 + ___const_50_0 ≤ 0___const_50_0___const_50_0 ≤ 0
2 74 2: tresh_post +