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