---

Step * of Lemma rng_before_imp_before_all

∀g:OCMon. ∀r:CDRng. ∀k:|g|. ∀ps:|omral(g;r)|.
  ((↑before(k;map(λz.(fst(z));ps))) ⇒ (↑(∀bx(:|g|) ∈ map(λz.(fst(z));ps). (x <b k))))
BY
{ ProveSpecializedLemma `before_imp_before_all` 2 [parm{i};g↓oset;r↓+gp
... }

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

---

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{}  (\muparrow{}(\mforall{}\msubb{}x(:|g|)  \mmember{}  map(\mlambda{}z.(fst(z));ps).  (x  <\msubb{}  k))))


By

---

Latex:
ProveSpecializedLemma  `before\_imp\_before\_all`  2  [parm\{i\};g\mdownarrow{}oset;r\mdownarrow{}+gp
...

---

Home Index