include "basic_2/rt_transition/lpr_lpr.ma".
include "basic_2/rt_computation/cpms_lsubr.ma".
include "basic_2/rt_computation/cpms_fpbg.ma".
include "basic_2/rt_transition/lpr_lpr.ma".
include "basic_2/rt_computation/cpms_lsubr.ma".
include "basic_2/rt_computation/cpms_fpbg.ma".
elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ]
-L0 -V0 -T0 -X0 #U #HVU #HTU
lapply (cpms_trans … HV2 … HVU) -V <plus_O_n >minus_plus #H2
elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ]
-L0 -V0 -T0 -X0 #U #HVU #HTU
lapply (cpms_trans … HV2 … HVU) -V <plus_O_n >minus_plus #H2
elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ]
-L0 -V0 -T0 -X0 #U #HVU #HTU
lapply (cpms_trans … HV2 … HVU) -V <plus_O_n >minus_plus #H2
elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ]
-L0 -V0 -T0 -X0 #U #HVU #HTU
lapply (cpms_trans … HV2 … HVU) -V <plus_O_n >minus_plus #H2