---

Step * 2 of Lemma rng_lookup_before_start


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|))
BY
{ AbReduceIf (\e t.not is_term `oalist` (subterm t 1)) 3 
THEN Fold `omralist` 3 }

1
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|))

---

Latex:

---

Latex:

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


By

---

Latex:
AbReduceIf  (\mbackslash{}e  t.not  is\_term  `oalist`  (subterm  t  1))  3 
THEN  Fold  `omralist`  3

---

Home Index