---

Step * 2 1 of Lemma rng_lookup_before_start


1. g : OCMon
2. r : CDRng
3. ∀k:|g|. ∀ps:|omral(g;r)|.  ((↑before(k;map(λz.(fst(z));ps))) ⇒ ((ps[k]) = 0 ∈ |r|))
⊢ ∀k:|g|. ∀ps:|omral(g;r)|.  ((↑before(k;map(λz.(fst(z));ps))) ⇒ ((ps[k]) = 0 ∈ |r|))
BY
{ Trivial }

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  \mforall{}k:|g|.  \mforall{}ps:|omral(g;r)|.    ((\muparrow{}before(k;map(\mlambda{}z.(fst(z));ps)))  {}\mRightarrow{}  ((ps[k])  =  0))
\mvdash{}  \mforall{}k:|g|.  \mforall{}ps:|omral(g;r)|.    ((\muparrow{}before(k;map(\mlambda{}z.(fst(z));ps)))  {}\mRightarrow{}  ((ps[k])  =  0))


By

---

Latex:
Trivial

---

Home Index