---

Step * 2 of Lemma es-pred?_wf


1. es : EO
2. e : E
3. ¬↑first(e)
⊢ pred(e) ∈ {e':E| (e' <loc e) ∧ (e' = pred(e) ∈ E)} 
BY
{ (InstLemma `es-pred_property` [⌈es⌉;⌈e⌉]⋅ THEN Auto) }

---

Latex:



1.  es  :  EO
2.  e  :  E
3.  \mneg{}\muparrow{}first(e)
\mvdash{}  pred(e)  \mmember{}  \{e':E|  (e'  <loc  e)  \mwedge{}  (e'  =  pred(e))\} 


By

(InstLemma  `es-pred\_property`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index