---

Step * 1 1 1 of Lemma omral_dom_scale


1. g : OCMon
2. r : CDRng
3. k : |g|
4. v : |r|
5. ps : |omral(g;r)|
6. x : |(g↓oset)|
7. ¬↑(x
∈b msmap{g↓oset,g↓oset}(λk'.(k' * k);dom(ps)))
⊢ ¬↑(x
∈b dom(<k,v>* ps))
BY
{ ((Assert r↓+gp ∈ DMon BY
          (DVar `r' THEN MemTypeCD THEN Auto))
   THEN PromoteHyp (-1) 3
   THEN (Assert dom(ps) ∈ MSet{g↓oset} BY
               Auto)) }

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);dom(ps)))
9. dom(ps) ∈ MSet{g↓oset}
⊢ ¬↑(x
∈b dom(<k,v>* ps))

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  r\mdownarrow{}+gp  \mmember{}  DMon  BY
                (DVar  `r'  THEN  MemTypeCD  THEN  Auto))
  THEN  PromoteHyp  (-1)  3
  THEN  (Assert  dom(ps)  \mmember{}  MSet\{g\mdownarrow{}oset\}  BY
                          Auto))

---

Home Index