LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
3 54 3: tmp29_post + tmp29_post ≤ 0tmp29_posttmp29_post ≤ 0tmp29_0 + tmp29_0 ≤ 0tmp29_0tmp29_0 ≤ 0tmp223_post + tmp223_post ≤ 0tmp223_posttmp223_post ≤ 0tmp223_0 + tmp223_0 ≤ 0tmp223_0tmp223_0 ≤ 0tmp18_post + tmp18_post ≤ 0tmp18_posttmp18_post ≤ 0tmp18_0 + tmp18_0 ≤ 0tmp18_0tmp18_0 ≤ 0tmp122_post + tmp122_post ≤ 0tmp122_posttmp122_post ≤ 0tmp122_0 + tmp122_0 ≤ 0tmp122_0tmp122_0 ≤ 0ret_icrc31_post + ret_icrc31_post ≤ 0ret_icrc31_postret_icrc31_post ≤ 0ret_icrc31_0 + ret_icrc31_0 ≤ 0ret_icrc31_0ret_icrc31_0 ≤ 0ret_icrc17_post + ret_icrc17_post ≤ 0ret_icrc17_postret_icrc17_post ≤ 0ret_icrc17_0 + ret_icrc17_0 ≤ 0ret_icrc17_0ret_icrc17_0 ≤ 0ret_icrc11330_post + ret_icrc11330_post ≤ 0ret_icrc11330_postret_icrc11330_post ≤ 0ret_icrc11330_0 + ret_icrc11330_0 ≤ 0ret_icrc11330_0ret_icrc11330_0 ≤ 0ret_icrc11316_post + ret_icrc11316_post ≤ 0ret_icrc11316_postret_icrc11316_post ≤ 0ret_icrc11316_0 + ret_icrc11316_0 ≤ 0ret_icrc11316_0ret_icrc11316_0 ≤ 0onech1027_post + onech1027_post ≤ 0onech1027_postonech1027_post ≤ 0onech1027_0 + onech1027_0 ≤ 0onech1027_0onech1027_0 ≤ 0onech1013_post + onech1013_post ≤ 0onech1013_postonech1013_post ≤ 0onech1013_0 + onech1013_0 ≤ 0onech1013_0onech1013_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0len5_post + len5_post ≤ 0len5_postlen5_post ≤ 0len5_0 + len5_0 ≤ 0len5_0len5_0 ≤ 0len19_post + len19_post ≤ 0len19_postlen19_post ≤ 0len19_0 + len19_0 ≤ 0len19_0len19_0 ≤ 0jrev7_post + jrev7_post ≤ 0jrev7_postjrev7_post ≤ 0jrev7_0 + jrev7_0 ≤ 0jrev7_0jrev7_0 ≤ 0jrev21_post + jrev21_post ≤ 0jrev21_postjrev21_post ≤ 0jrev21_0 + jrev21_0 ≤ 0jrev21_0jrev21_0 ≤ 0jinit6_post + jinit6_post ≤ 0jinit6_postjinit6_post ≤ 0jinit6_0 + jinit6_0 ≤ 0jinit6_0jinit6_0 ≤ 0jinit20_post + jinit20_post ≤ 0jinit20_postjinit20_post ≤ 0jinit20_0 + jinit20_0 ≤ 0jinit20_0jinit20_0 ≤ 0j24_post + j24_post ≤ 0j24_postj24_post ≤ 0j24_0 + j24_0 ≤ 0j24_0j24_0 ≤ 0j10_post + j10_post ≤ 0j10_postj10_post ≤ 0j10_0 + j10_0 ≤ 0j10_0j10_0 ≤ 0init_post + init_post ≤ 0init_postinit_post ≤ 0init_0 + init_0 ≤ 0init_0init_0 ≤ 0i2_post + i2_post ≤ 0i2_posti2_post ≤ 0i2_0 + i2_0 ≤ 0i2_0i2_0 ≤ 0i1_post + i1_post ≤ 0i1_posti1_post ≤ 0i1_0 + i1_0 ≤ 0i1_0i1_0 ≤ 0i1128_post + i1128_post ≤ 0i1128_posti1128_post ≤ 0i1128_0 + i1128_0 ≤ 0i1128_0i1128_0 ≤ 0i1114_post + i1114_post ≤ 0i1114_posti1114_post ≤ 0i1114_0 + i1114_0 ≤ 0i1114_0i1114_0 ≤ 0