---

Step * 2 1 3 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
{ (((Force `5` (Eval ``rels_iso`` 0)) THEN Auto) THEN BLemma `ocgrp_abdgrp` 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  \mleq{}\mleq{}\msubb{}  y;x,y.\muparrow{}x  \mleq{}\mleq{}\msubb{}  y;\mlambda{}z.z)


By

---

Latex:
(((Force  `5`  (Eval  ``rels\_iso``  0))  THEN  Auto)  THEN  BLemma  `ocgrp\_abdgrp`  THEN  Auto)

---

Home Index