---

Step * of Lemma before_all_imp_before

∀a:LOSet. ∀b:AbMon. ∀k:|a|. ∀ps:(|a| × |b|) List.
  ((↑(∀bx(:|a|) ∈ map(λz.(fst(z));ps). (x <b k))) ⇒ (↑before(k;map(λz.(fst(z));ps))))
BY
{ ((CDToVarThen `ps' D) THENA Auto) }

1
1. a : LOSet
2. b : AbMon
3. k : |a|
⊢ (↑(∀bx(:|a|) ∈ map(λz.(fst(z));[]). (x <b k))) ⇒ (↑before(k;map(λz.(fst(z));[])))

2
1. a : LOSet
2. b : AbMon
3. k : |a|
4. u : |a| × |b|
5. v : (|a| × |b|) List
⊢ (↑(∀bx(:|a|) ∈ map(λz.(fst(z));[u / v]). (x <b k))) ⇒ (↑before(k;map(λz.(fst(z));[u / v])))

---

Latex:

---

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


By

---

Latex:
((CDToVarThen  `ps'  D)  THENA  Auto)

---

Home Index