include "pointer_list_standard.ma".
(* KASHIMA'S "ST" COMPUTATION ***********************************************)
include "pointer_list_standard.ma".
(* KASHIMA'S "ST" COMPUTATION ***********************************************)
@(ex2_intro … HM) -M -A2 /3 width=1/
| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ * #rb #HB12 #Hrb * #ra #HA12 #Hra
lapply (lsreds_trans … HM (dx:::ra) (@B1.A2) ?) /2 width=1/ -A1 #HM
@(ex2_intro … HM) -M -A2 /3 width=1/
| #s #M #B1 #B2 #A1 #A2 #Hs #HM #_ #_ * #rb #HB12 #Hrb * #ra #HA12 #Hra
lapply (lsreds_trans … HM (dx:::ra) (@B1.A2) ?) /2 width=1/ -A1 #HM