---

Step * of Lemma rng_before_all_imp_before

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

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}r:CRng.  \mforall{}k:|g|.  \mforall{}ps:(|g|  \mtimes{}  |r|)  List.
    ((\muparrow{}(\mforall{}\msubb{}x(:|g|)  \mmember{}  map(\mlambda{}z.(fst(z));ps).  (x  <\msubb{}  k)))  {}\mRightarrow{}  (\muparrow{}before(k;map(\mlambda{}z.(fst(z));ps))))


By

---

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

---

Home Index