---

Step * 2 1 2 of Lemma oal_hgp_wf2


1. s : LOSet@i'
2. g : OGrp@i'
3. g↓hgrp ∈ AbDMon
4. g ∈ AbDMon
⊢ RelsIso(|oal(s;g↓hgrp)|;|oal(s;g)|;x,y.↑(x (=b) y);x,y.↑(x (=b) y);λz.z)
BY
{ ((RWN 2 oal_add_hgrp_of_ocgrpC 0 
THEN Force `5` (Eval ``rels_iso`` 0)) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
3.  g\mdownarrow{}hgrp  \mmember{}  AbDMon
4.  g  \mmember{}  AbDMon
\mvdash{}  RelsIso(|oal(s;g\mdownarrow{}hgrp)|;|oal(s;g)|;x,y.\muparrow{}(x  (=\msubb{})  y);x,y.\muparrow{}(x  (=\msubb{})  y);\mlambda{}z.z)


By

---

Latex:
((RWN  2  oal\_add\_hgrp\_of\_ocgrpC  0 
THEN  Force  `5`  (Eval  ``rels\_iso``  0))  THEN  Auto)

---

Home Index