---

Step * 1 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 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)))
BY
{ (RepUR ``compose`` (-2) THEN Thin (-1)) }

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(λx.((fst(x)) * k);ps)))
⊢ ¬↑(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{}  mk\_mset(map((\mlambda{}k'.(k'  *  k))  o  (\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:
(RepUR  ``compose``  (-2)  THEN  Thin  (-1))

---

Home Index