---

Step * of Lemma es-pred?_wf

∀[es:EO]. ∀[e:E].  (es-pred?(es;e) ∈ {e':E| (e' <loc e) ∧ (e' = pred(e) ∈ E)} ?)
BY
{ ProveWfLemma }

1
1. es : EO
2. e : E
3. ↑first(e)
4. e' : E
5. (e' <loc e)
⊢ ¬↑first(e)

2
1. es : EO
2. e : E
3. ¬↑first(e)
⊢ pred(e) ∈ {e':E| (e' <loc e) ∧ (e' = pred(e) ∈ E)} 

---

Latex:


\mforall{}[es:EO].  \mforall{}[e:E].    (es-pred?(es;e)  \mmember{}  \{e':E|  (e'  <loc  e)  \mwedge{}  (e'  =  pred(e))\}  ?)


By

ProveWfLemma

---

Home Index