---

Step * 1 1 1 of Lemma omral_times_dom


1. g : OCMon
2. r : CDRng
3. qs : {ps:(|g| × |r|) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(0 ∈b map(λx.(snd(x));ps)))} 
4. r↓+gp ∈ AbDMon
5. g ∈ DMon
6. x : |g|
7. ↑(x
∈b 0{g↓oset})
⊢ ↑(x
∈b 0{g↓oset} × dom(qs))
BY
{ ((RWH (LemmaC `mset_mem_char`) (-1)) THENA Auto) 
THEN Eval ``oset_of_ocmon`` (-1) THEN Trivial⋅ }

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  qs  :  \{ps:(|g|  \mtimes{}  |r|)  List|  (\muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));ps)))  \mwedge{}  (\mneg{}\muparrow{}(0  \mmember{}\msubb{}  map(\mlambda{}x.(snd(x));ps)))\} 
4.  r\mdownarrow{}+gp  \mmember{}  AbDMon
5.  g  \mmember{}  DMon
6.  x  :  |g|
7.  \muparrow{}(x
\mmember{}\msubb{}  0\{g\mdownarrow{}oset\})
\mvdash{}  \muparrow{}(x
\mmember{}\msubb{}  0\{g\mdownarrow{}oset\}  \mtimes{}  dom(qs))


By

---

Latex:
((RWH  (LemmaC  `mset\_mem\_char`)  (-1))  THENA  Auto) 
THEN  Eval  ``oset\_of\_ocmon``  (-1)  THEN  Trivial\mcdot{}

---

Home Index