---

Step * 1 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);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)))
BY
{ ((RWH (LemmaC `mset_map_char`) (-2)⋅ THENM ((RWH (LemmaWithC [`C',|g|] `map_map`) (-2)) THENA Auto))
   THEN Auto
   THEN Try (Complete ((RepUR ``mk_mset mset`` (-1)
                        THEN ((Assert map(λz.(fst(z));ps) ∈ |g| List BY Auto) THEN Reduce 0 THEN 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 mk_mset(map((λk'.(k' * k)) o (λ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);mk\_mset(map(\mlambda{}z.(fst(z));ps))))
9.  mk\_mset(map(\mlambda{}z.(fst(z));ps))  \mmember{}  MSet\{g\mdownarrow{}oset\}
\mvdash{}  \mneg{}\muparrow{}(x
\mmember{}\msubb{}  mk\_mset(map(\mlambda{}z.(fst(z));<k,v>*  ps)))


By

---

Latex:
((RWH  (LemmaC  `mset\_map\_char`)  (-2)\mcdot{}  THENM  ((RWH  (LemmaWithC  [`C',|g|]  `map\_map`)  (-2))  THENA  Auto))
  THEN  Auto
  THEN  Try  (Complete  ((RepUR  ``mk\_mset  mset``  (-1)
                                            THEN  ((Assert  map(\mlambda{}z.(fst(z));ps)  \mmember{}  |g|  List  BY  Auto)  THEN  Reduce  0  THEN  Auto)
                                            )\mcdot{})))\mcdot{}

---

Home Index