---

Step * 1 of Lemma omral_minus_wf

.....equality..... 
1. g : OCMon
2. r : CDRng
3. ps : |omral(g;r)|
⊢ |omral(g;r)| ~ |oal(g↓set;r↓+gp)|
BY
{ (Reduce 0 THEN Repeat (SqEqCDWithUnfolding)) }

---

Latex:

---

Latex:
.....equality..... 
1.  g  :  OCMon
2.  r  :  CDRng
3.  ps  :  |omral(g;r)|
\mvdash{}  |omral(g;r)|  \msim{}  |oal(g\mdownarrow{}set;r\mdownarrow{}+gp)|


By

---

Latex:
(Reduce  0  THEN  Repeat  (SqEqCDWithUnfolding))

---

Home Index