---

Step * 1 1 of Lemma es-pred_wf


1. the_es : EO
2. e : E
3. pred(e) ∈ es-base-E(the_es)
4. ¬↑(es-dom(the_es) pred(e))
⊢ ↑first(e)
BY
{ (Unfold `es-first` 0 THEN (InstLemma `es-eq-E-wf-base` [⌈the_es⌉]⋅ THENA Auto)) }

1
1. the_es : EO
2. e : E
3. pred(e) ∈ es-base-E(the_es)
4. ¬↑(es-dom(the_es) pred(e))
5. ∀[e,e':es-base-E(the_es)].  (e = e' ∈ 𝔹)
⊢ ↑(pred(e) = e ∨b(¬b(es-dom(the_es) pred(e))))

---

Latex:



1.  the$_{es}$  :  EO
2.  e  :  E
3.  pred(e)  \mmember{}  es-base-E(the$_{es}$)
4.  \mneg{}\muparrow{}(es-dom(the$_{es}$)  pred(e))
\mvdash{}  \muparrow{}first(e)


By

(Unfold  `es-first`  0  THEN  (InstLemma  `es-eq-E-wf-base`  [\mkleeneopen{}the$_{es}$\mkleeneclose{}]\mcdot{}  THENA  Aut\000Co))

---

Home Index