---

Step * 1 1 1 of Lemma oal_grp_wf2


1. s : LOSet@i'
2. g : OGrp@i'
3. oal_grp(s;g) ∈ AbGrp
4. oal_grp(s;g) ∈ OMon
⊢ oal_grp(s;g) ∈ OCMon
BY
{ (Unfold `omon` -1 THEN (MemTypeHD (-1)⋅ THENA Auto) THEN Fold `member` (-2) THEN MemTypeCD) }

1
1. s : LOSet@i'
2. g : OGrp@i'
3. oal_grp(s;g) ∈ AbGrp
4. oal_grp(s;g) ∈ AbMon
5. UniformLinorder(|oal_grp(s;g)|;x,y.↑(x ≤b y))
∧ (=b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|oal_grp(s;g)| ⟶ |oal_grp(s;g)| ⟶ 𝔹))
⊢ oal_grp(s;g) ∈ AbMon

2
.....set predicate..... 
1. s : LOSet@i'
2. g : OGrp@i'
3. oal_grp(s;g) ∈ AbGrp
4. oal_grp(s;g) ∈ AbMon
5. UniformLinorder(|oal_grp(s;g)|;x,y.↑(x ≤b y))
∧ (=b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|oal_grp(s;g)| ⟶ |oal_grp(s;g)| ⟶ 𝔹))
⊢ (UniformLinorder(|oal_grp(s;g)|;x,y.↑(x ≤b y))
  ∧ (=b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|oal_grp(s;g)| ⟶ |oal_grp(s;g)| ⟶ 𝔹)))
∧ Cancel(|oal_grp(s;g)|;|oal_grp(s;g)|;*)
∧ (∀[z:|oal_grp(s;g)|]. monot(|oal_grp(s;g)|;x,y.↑(x ≤b y);λw.(z * w)))

3
.....wf..... 
1. s : LOSet@i'
2. g : OGrp@i'
3. oal_grp(s;g) ∈ AbGrp
4. oal_grp(s;g) ∈ AbMon
5. UniformLinorder(|oal_grp(s;g)|;x,y.↑(x ≤b y))
∧ (=b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|oal_grp(s;g)| ⟶ |oal_grp(s;g)| ⟶ 𝔹))
6. g1 : AbMon
⊢ (UniformLinorder(|g1|;x,y.↑(x ≤b y)) ∧ (=b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|g1| ⟶ |g1| ⟶ 𝔹)))
  ∧ Cancel(|g1|;|g1|;*)
  ∧ (∀[z:|g1|]. monot(|g1|;x,y.↑(x ≤b y);λw.(z * w))) ∈ Type

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
3.  oal\_grp(s;g)  \mmember{}  AbGrp
4.  oal\_grp(s;g)  \mmember{}  OMon
\mvdash{}  oal\_grp(s;g)  \mmember{}  OCMon


By

---

Latex:
(Unfold  `omon`  -1  THEN  (MemTypeHD  (-1)\mcdot{}  THENA  Auto)  THEN  Fold  `member`  (-2)  THEN  MemTypeCD)

---

Home Index