---

Step * 1 of Lemma es-pred-exists-between


1. es : EO@i'
2. e1 : E@i
3. e2 : E@i
4. ∀e':E. ((e' < e2) ⇒ (e1 <loc e') ⇒ (∃e:{e:E| ¬↑first(e)} . (e1 = pred(e) ∈ E)))
5. (e1 <loc e2)@i
6. (e1 <loc pred(e2))
⊢ ∃e:{e:E| ¬↑first(e)} . (e1 = pred(e) ∈ E)
BY
{ (InstHyp [⌈pred(e2)⌉] (-3)⋅ THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  e1  :  E@i
3.  e2  :  E@i
4.  \mforall{}e':E.  ((e'  <  e2)  {}\mRightarrow{}  (e1  <loc  e')  {}\mRightarrow{}  (\mexists{}e:\{e:E|  \mneg{}\muparrow{}first(e)\}  .  (e1  =  pred(e))))
5.  (e1  <loc  e2)@i
6.  (e1  <loc  pred(e2))
\mvdash{}  \mexists{}e:\{e:E|  \mneg{}\muparrow{}first(e)\}  .  (e1  =  pred(e))


By

(InstHyp  [\mkleeneopen{}pred(e2)\mkleeneclose{}]  (-3)\mcdot{}  THEN  Auto)

---

Home Index