---

Step * 1 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))
5. ∀[e,e':es-base-E(the_es)].  (e = e' ∈ 𝔹)
⊢ ↑(pred(e) = e ∨b(¬b(es-dom(the_es) pred(e))))
BY
{ (RW assert_pushdownC 0 THEN Auto) }

---

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))
5.  \mforall{}[e,e':es-base-E(the$_{es}$)].    (e  =  e'  \mmember{}  \mBbbB{})
\mvdash{}  \muparrow{}(pred(e)  =  e  \mvee{}\msubb{}(\mneg{}\msubb{}(es-dom(the$_{es}$)  pred(e))))


By

(RW  assert\_pushdownC  0  THEN  Auto)

---

Home Index