---

Step * of Lemma rng_lookup_before_start

∀g:OCMon. ∀r:CDRng. ∀k:|g|. ∀ps:|omral(g;r)|.  ((↑before(k;map(λz.(fst(z));ps))) ⇒ ((ps[k]) = 0 ∈ |r|))
BY
{ ((D 0 THENM D 0 
THENM AssertLemma `lookup_before_start` [] 
THENM With g↓oset (D (-1)) THENM With r↓+gp (D (-1))) THENA Auto) }

1
.....wf..... 
1. g : OCMon
2. r : CDRng
⊢ r↓+gp ∈ AbDMon

2
1. g : OCMon
2. r : CDRng
3. ∀k:|(g↓oset)|. ∀ps:|oal(g↓oset;r↓+gp)|.  ((↑before(k;map(λz.(fst(z));ps))) ⇒ ((ps[k]) = e ∈ |r↓+gp|))
⊢ ∀k:|g|. ∀ps:|omral(g;r)|.  ((↑before(k;map(λz.(fst(z));ps))) ⇒ ((ps[k]) = 0 ∈ |r|))

---

Latex:

---

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


By

---

Latex:
((D  0  THENM  D  0 
THENM  AssertLemma  `lookup\_before\_start`  [] 
THENM  With  g\mdownarrow{}oset  (D  (-1))  THENM  With  r\mdownarrow{}+gp  (D  (-1)))  THENA  Auto)

---

Home Index