- 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) //
- [ @(ygt_yprs_trans … G1 G1 … L1 L1 … V1) (**) (* auto /4 width=5/ is a bit slow even with trace *)
- [ /2 width=1 by fsupp_ygt/
- | /3 width=1 by cprs_lpr_yprs, cpr_cprs/
- ]
- ] #HW3
- elim (snv_fwd_ssta … HW2) #l0 #U2 #HWU2
- elim (ssta_fwd_correct … HV2W3) <minus_plus_m_m #U3 #HWU3
- elim (ssta_cpcs_lpr_aux … IH1 IH3 … HWU3 … HWU2 … HW32 … L2) // -IH3
- [2: /4 width=5 by ygt_yprs_trans, fsupp_ygt, cprs_lpr_yprs, cpr_cprs/
- |3: @(ygt_yprs_trans … G1 G1 L1 L2 … V2) (**) (* auto not tried *)
- [ @(ygt_yprs_trans … G1 G1 L1 L1 … V1)
- [ /2 width=1 by fsupp_ygt/
- | /3 width=1 by cprs_lpr_yprs, cpr_cprs/
- ]
- | /3 width=2 by ypr_ssta, ypr_yprs/
- ]
- ] #H #_ destruct -IH2 -U3
- lapply (IH4 … HT2 (L2.ⓓⓝW2.V2) ?)
- [ /3 width=5/
- | @(ygt_yprs_trans … G1 G1 … (L1.ⓛW20) … T2) (**) (* auto /5 width=5/ is too slow even with trace timeout=35 *)
- [ /4 width=5 by ygt_yprs_trans, fsupp_ygt, ypr_yprs, ypr_cpr/
- | /4 width=1 by ypr_yprs, ypr_lpr, lpr_pair/
- ]
- ] -L1 -V1 -T20 -U2 /3 width=4/
+ lapply (IH1 … HV12 … HL12) /2 width=1 by fsupp_ygt/ -HV1 #HV2
+ lapply (IH1 … HW202 … HL12) /2 width=1 by fsupp_ygt/ -HW20 #HW2
+ lapply (IH1 … HT20 … HT202 … (L2.ⓛW2) ?) /2 width=1 by fsupp_ygt, lpr_pair/ -HT20 #HT2
+ lapply (snv_ssta_aux … IH4 … HlV2 … HV2W3)
+ /3 width=5 by ygt_yprs_trans, fsupp_ygt, cpr_lpr_yprs/ #HW3
+ lapply (lsubsv_snv_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /3 width=3 by snv_bind, snv_cast/
+ @(lsubsv_abbr … l) /3 width=7 by fsupp_ygt/ #W #W0 #l0 #Hl0 #HV2W #HW20
+ lapply (lsstas_ssta_conf_pos … HV2W3 … HV2W) -HV2W #HW3W
+ @(lsstas_cpcs_lpr_aux … IH1 IH2 IH3 … HlW3 … HW3W … HlW2 … HW20 … HW32) //
+ [ /3 width=9 by ygt_yprs_trans, fsupp_ygt, cpr_lpr_ssta_yprs/
+ | /3 width=5 by ygt_yprs_trans, fsupp_ygt, cpr_lpr_yprs/
+ ]