---

Step * 1 1 1 1 of Lemma omral_dom_action


1. g : OCMon
2. r : CDRng
3. v : |r|
4. ps : |omral(g;r)|
5. x : |(g↓oset)|
6. ↑(x
∈b msmap{g↓oset,g↓oset}(λk'.(k' * e);dom(ps)))
⊢ ↑(x
∈b dom(ps))
BY
{ ((RWH (AssertC (λk'.(k' * e)) = Id{|(g↓oset)|} ∈ (|g| ⟶ |g|)) 6 
THENM RWW "mset_map_id" 6) THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((RWH  (AssertC  (\mlambda{}k'.(k'  *  e))  =  Id\{|(g\mdownarrow{}oset)|\})  6 
THENM  RWW  "mset\_map\_id"  6)  THEN  Auto)

---

Home Index