---

Step * 1 of Lemma omral_scale_wf2


1. g : OCMon
2. r : CDRng
3. k : |g|
4. v : |r|
5. ps : |omral(g;r)|
⊢ <k,v>* ps ∈ |omral(g;r)|
BY
{ (Assert r↓+gp ∈ DMon BY
         (DVar `r' THEN MemTypeCD THEN Auto)) }

1
1. g : OCMon
2. r : CDRng
3. k : |g|
4. v : |r|
5. ps : |omral(g;r)|
6. r↓+gp ∈ DMon
⊢ <k,v>* ps ∈ |omral(g;r)|

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  k  :  |g|
4.  v  :  |r|
5.  ps  :  |omral(g;r)|
\mvdash{}  <k,v>*  ps  \mmember{}  |omral(g;r)|


By

---

Latex:
(Assert  r\mdownarrow{}+gp  \mmember{}  DMon  BY
              (DVar  `r'  THEN  MemTypeCD  THEN  Auto))

---

Home Index