---

Step * 1 1 1 1 of Lemma omral_dom_scale


1. g : OCMon
2. r : CDRng
3. r↓+gp ∈ DMon
4. k : |g|
5. v : |r|
6. ps : |omral(g;r)|
7. x : |(g↓oset)|
8. ¬↑(x
∈b msmap{g↓oset,g↓oset}(λk'.(k' * k);dom(ps)))
9. dom(ps) ∈ MSet{g↓oset}
⊢ ¬↑(x
∈b dom(<k,v>* ps))
BY
{ All (RepUR ``omral_dom oal_dom``)⋅ }

1
1. g : OCMon
2. r : CDRng
3. r↓+gp ∈ DMon
4. k : |g|
5. v : |r|
6. ps : |omral(g;r)|
7. x : |(g↓oset)|
8. ¬↑(x
∈b msmap{g↓oset,g↓oset}(λk'.(k' * k);mk_mset(map(λz.(fst(z));ps))))
9. mk_mset(map(λz.(fst(z));ps)) ∈ MSet{g↓oset}
⊢ ¬↑(x
∈b mk_mset(map(λz.(fst(z));<k,v>* ps)))

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  r\mdownarrow{}+gp  \mmember{}  DMon
4.  k  :  |g|
5.  v  :  |r|
6.  ps  :  |omral(g;r)|
7.  x  :  |(g\mdownarrow{}oset)|
8.  \mneg{}\muparrow{}(x
\mmember{}\msubb{}  msmap\{g\mdownarrow{}oset,g\mdownarrow{}oset\}(\mlambda{}k'.(k'  *  k);dom(ps)))
9.  dom(ps)  \mmember{}  MSet\{g\mdownarrow{}oset\}
\mvdash{}  \mneg{}\muparrow{}(x
\mmember{}\msubb{}  dom(<k,v>*  ps))


By

---

Latex:
All  (RepUR  ``omral\_dom  oal\_dom``)\mcdot{}

---

Home Index