- lapply (cpcs_lpr_conf … HL12 … HW120) -HW120 #HW120
- elim (IH3 … HVW1 … HV12 … HL12) // [2: /2 width=1/ ] -HVW1 #W2 #HVW2 #HW102
- lapply (cpcs_canc_sn … HW102 … HW120) -W10 #HW220
- lapply (IH1 … HV12 … HL12) // [ /2 width=1/ ] #HV2 -HV1
- lapply (IH1 … HW20 … W20 … HL12) // [ /2 width=1/ ] -HW20 #HW20
- lapply (IH1 … HT20 … HT202 … (L2.ⓛW20) ?) [1,2: /2 width=1/ ] -HT20 #HT2
- lapply (IH2 … HVW2) //
+ lapply (cpcs_cpr_strap1 … HW120 … HW202) -HW120 #HW102
+ lapply (lpr_cpcs_conf … HL12 … HW102) -HW102 #HW102
+ elim (IH3 … HVW1 … HV12 … HL12) // [2: /2 width=1/ ] -HVW1 #W3 #HV2W3 #HW103
+ lapply (cpcs_canc_sn … HW103 … HW102) -W10 #HW32
+ lapply (IH1 … HV12 … HL12) // [ /2 width=1/ ] -HV1 #HV2
+ lapply (IH1 … HW202 … HL12) // [ /2 width=1/ ] -HW20 #HW2
+ lapply (IH1 … HT20 … HT202 … (L2.ⓛW2) ?) [1,2: /2 width=1/ ] -HT20 #HT2
+ lapply (IH2 … HV2W3) //