---

Step * 1 of Lemma es-pred_wf

.....set predicate..... 
1. the_es : EO
2. e : E
3. ¬↑first(e)
⊢ ↑(es-dom(the_es) pred(e))
BY
{ ((InstLemma `es-pred-wf-base` [⌈the_es⌉;⌈e⌉]⋅ THENA Auto) THEN SupposeNot THEN D -3) }

1
1. the_es : EO
2. e : E
3. pred(e) ∈ es-base-E(the_es)
4. ¬↑(es-dom(the_es) pred(e))
⊢ ↑first(e)

---

Latex:


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


By

((InstLemma  `es-pred-wf-base`  [\mkleeneopen{}the$_{es}$\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  SupposeNot  TH\000CEN  D  -3)

---

Home Index