---

Step * of Lemma before_imp_before_all

∀a:LOSet. ∀b:AbDMon. ∀k:|a|. ∀ps:|oal(a;b)|.
  ((↑before(k;map(λz.(fst(z));ps))) ⇒ (↑(∀bx(:|a|) ∈ map(λz.(fst(z));ps). (x <b k))))
BY
{ ((RepD) THENA Auto) }

1
1. a : LOSet@i'
2. b : AbDMon@i'
3. k : |a|@i
4. ps : |oal(a;b)|@i
5. ↑before(k;map(λz.(fst(z));ps))@i
⊢ ↑(∀bx(:|a|) ∈ map(λz.(fst(z));ps)
       (x <b k))

---

Latex:

---

Latex:
\mforall{}a:LOSet.  \mforall{}b:AbDMon.  \mforall{}k:|a|.  \mforall{}ps:|oal(a;b)|.
    ((\muparrow{}before(k;map(\mlambda{}z.(fst(z));ps)))  {}\mRightarrow{}  (\muparrow{}(\mforall{}\msubb{}x(:|a|)  \mmember{}  map(\mlambda{}z.(fst(z));ps).  (x  <\msubb{}  k))))


By

---

Latex:
((RepD)  THENA  Auto)

---

Home Index