---

Step * of Lemma oal_grp_wf1

∀s:LOSet. ∀g:OGrp.  (oal_grp(s;g) ∈ OMon)
BY
{ (Intros
   THEN (InstLemma `ocgrp_abdgrp` [⌜g⌝]⋅ THENA Auto)
   THEN (Assert g ∈ AbDMon BY
               (MemTypeCD THEN Try (BLemma `omon_inc`) THEN Auto THEN RepeatFor 3 (DVar `g') THEN Auto))
   THEN (Assert UniformLinorder(|oal_grp(s;g)|;x,y.↑(x ≤b y)) BY
               (Force `5` (Reduce 0) THEN Fold `oal_le` 0⋅
                THEN (((Unfold `ulinorder` 0 
                      THEN Backchain ``oal_le_connex``) THEN Auto)
                      THEN Try ((BLemma `ocgrp_abdgrp` THEN Auto))
                      THEN ((InstLemma `oal_le_is_order` [⌜s⌝;⌜g⌝]⋅ THEN Auto)
                            THEN (((D 0 THEN D -1) THEN Auto THEN D 0 THEN Auto) THEN BLemma `ocgrp_abdgrp` THEN Auto)⋅
                            )⋅)⋅
                ))) }

1
1. s : LOSet
2. g : OGrp
3. g ∈ AbDGrp
4. g ∈ AbDMon
5. UniformLinorder(|oal_grp(s;g)|;x,y.↑(x ≤b y))
⊢ oal_grp(s;g) ∈ OMon

---

Latex:

---

Latex:
\mforall{}s:LOSet.  \mforall{}g:OGrp.    (oal\_grp(s;g)  \mmember{}  OMon)


By

---

Latex:
(Intros
  THEN  (InstLemma  `ocgrp\_abdgrp`  [\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  g  \mmember{}  AbDMon  BY
                          (MemTypeCD
                            THEN  Try  (BLemma  `omon\_inc`)
                            THEN  Auto
                            THEN  RepeatFor  3  (DVar  `g')
                            THEN  Auto))
  THEN  (Assert  UniformLinorder(|oal\_grp(s;g)|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))  BY
                          (Force  `5`  (Reduce  0)  THEN  Fold  `oal\_le`  0\mcdot{}
                            THEN  (((Unfold  `ulinorder`  0 
                                        THEN  Backchain  ``oal\_le\_connex``)  THEN  Auto)
                                        THEN  Try  ((BLemma  `ocgrp\_abdgrp`  THEN  Auto))
                                        THEN  ((InstLemma  `oal\_le\_is\_order`  [\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THEN  Auto)
                                                    THEN  (((D  0  THEN  D  -1)  THEN  Auto  THEN  D  0  THEN  Auto)
                                                                THEN  BLemma  `ocgrp\_abdgrp`
                                                                THEN  Auto)\mcdot{}
                                                    )\mcdot{})\mcdot{}
                            )))

---

Home Index