---

Step * 1 1 1 of Lemma es-local-pred-property2


1. [Info] : Type
2. es : EO+(Info)@i'
3. e : E@i
4. P : {e':E| (e' <loc e)}  ─→ 𝔹@i
5. last(P) e ∈ (∃e':{E| ((e' <loc e) ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑(P e'')))))})
   ∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑(P e')))}))
6. x : E@i
7. \\%4 : (x <loc e) ∧ (↑(P x)) ∧ (∀e'':E. ((x <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑(P e''))))@i
8. True@i
⊢ (x <loc e)
BY
{ (Unhide THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  e  :  E@i
4.  P  :  \{e':E|  (e'  <loc  e)\}    {}\mrightarrow{}  \mBbbB{}@i
5.  last(P)  e  \mmember{}  (\mexists{}e':\{E|  ((e'  <loc  e)
                                                \mwedge{}  (\muparrow{}(P  e'))
                                                \mwedge{}  (\mforall{}e'':E.  ((e'  <loc  e'')  {}\mRightarrow{}  (e''  <loc  e)  {}\mRightarrow{}  (\mneg{}\muparrow{}(P  e'')))))\})
      \mvee{}  (\mneg{}(\mexists{}e':\{E|  ((e'  <loc  e)  \mwedge{}  (\muparrow{}(P  e')))\}))
6.  x  :  E@i
7.  \mbackslash{}\mbackslash{}\%4  :  (x  <loc  e)  \mwedge{}  (\muparrow{}(P  x))  \mwedge{}  (\mforall{}e'':E.  ((x  <loc  e'')  {}\mRightarrow{}  (e''  <loc  e)  {}\mRightarrow{}  (\mneg{}\muparrow{}(P  e''))))@i
8.  True@i
\mvdash{}  (x  <loc  e)


By

---

Latex:
(Unhide  THEN  Auto)\mcdot{}

---

Home Index