---

Step * of Lemma es-pred-causl

∀the_es:EO. ∀j:E.  (pred(j) < j) supposing ¬↑first(j)
BY
{ (Use_ES_Axioms THEN Auto THEN (InstHyp [⌜pred(j)⌝; ⌜j⌝] 11)⋅ THEN Auto THEN BLemma `es-pred-locl` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}the$_{es}$:EO.  \mforall{}j:E.    (pred(j)  <  j)  supposing  \mneg{}\muparrow{}first(j)


By

---

Latex:
(Use\_ES\_Axioms
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}pred(j)\mkleeneclose{};  \mkleeneopen{}j\mkleeneclose{}]  11)\mcdot{}
  THEN  Auto
  THEN  BLemma  `es-pred-locl`
  THEN  Auto)

---

Home Index