---

Step * 1 1 of Lemma oal_omcp_wf


1. s : LOSet@i'
2. g : OGrp@i'
⊢ <oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)> ∈ mcopower_sig{i:l}(s;g↓hgrp)
BY
{ ((Assert g↓hgrp ∈ AbMon BY Auto) THEN (MemTypeD (-1) THENA Auto) THEN Unfold `mcopower_sig` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
\mvdash{}  <oal\_hgp(s;g),  \mlambda{}k,v.  inj(k,v),  \mlambda{}h,f.  umap(h,f)>  \mmember{}  mcopower\_sig\{i:l\}(s;g\mdownarrow{}hgrp)


By

---

Latex:
((Assert  g\mdownarrow{}hgrp  \mmember{}  AbMon  BY
                Auto)
  THEN  (MemTypeD  (-1)  THENA  Auto)
  THEN  Unfold  `mcopower\_sig`  0
  THEN  Auto)

---

Home Index