---

Step * 2 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. (pred(e2) <loc e1)
⊢ ∃e:{e:E| ¬↑first(e)} . (e1 = pred(e) ∈ E)
BY
{ ((Assert ⌈False⌉⋅ THEN Auto)
   THEN InstLemma `es-pred_property` [⌈es⌉;⌈e2⌉]⋅
   THEN Auto
   THEN (InstHyp [⌈e1⌉] (-1)⋅ THENA Auto)
   THEN D (-1)
   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.  (pred(e2)  <loc  e1)
\mvdash{}  \mexists{}e:\{e:E|  \mneg{}\muparrow{}first(e)\}  .  (e1  =  pred(e))


By

((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  InstLemma  `es-pred\_property`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}e1\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Auto)

---

Home Index