---

Step * of Lemma lookup_oal_cons

∀a:LOSet. ∀b:OCMon. ∀k,kp:|a|. ∀vp:|b|. ∀ps:|oal(a;b)|.
  ((↑before(kp;map(λz.(fst(z));ps))) ⇒ (([<kp, vp> / ps][k]) = ((when kp (=b) k. vp) * (ps[k])) ∈ |b|))
BY
{ ((RepD) THENA Auto) }

1
1. a : LOSet
2. b : OCMon
3. k : |a|
4. kp : |a|
5. vp : |b|
6. ps : |oal(a;b)|
7. ↑before(kp;map(λz.(fst(z));ps))
⊢ ([<kp, vp> / ps][k]) = ((when kp (=b) k. vp) * (ps[k])) ∈ |b|

---

Latex:

---

Latex:
\mforall{}a:LOSet.  \mforall{}b:OCMon.  \mforall{}k,kp:|a|.  \mforall{}vp:|b|.  \mforall{}ps:|oal(a;b)|.
    ((\muparrow{}before(kp;map(\mlambda{}z.(fst(z));ps)))  {}\mRightarrow{}  (([<kp,  vp>  /  ps][k])  =  ((when  kp  (=\msubb{})  k.  vp)  *  (ps[k]))))


By

---

Latex:
((RepD)  THENA  Auto)

---

Home Index