---

Step * 1 1 of Lemma es-local-le-pred-property


1. [Info] : Type
2. P : es:EO+(Info) ─→ E ─→ 𝔹@i'
3. es : EO+(Info)@i'
4. e : E@i
5. ∀e1:E
     ((e1 < e)
     ⇒ ((↑e1 ∈b ≤(P) ⇐⇒ ∃a:E. (a ≤loc e1  ∧ (↑(P es a))))
        ∧ ≤(P)(e1) ≤loc e1  ∧ (↑(P es ≤(P)(e1))) ∧ (∀e'':E. (e'' ≤loc e1  ⇒ (≤(P)(e1) <loc e'') ⇒ (¬↑(P es e'')))) 
          supposing ↑e1 ∈b ≤(P)))
6. ¬↑(P es e)
7. ↑first(e)
⊢ (False ⇐⇒ ∃a:E. (a ≤loc e  ∧ (↑(P es a))))
∧ only({}) ≤loc e  ∧ (↑(P es only({}))) ∧ (∀e'':E. (e'' ≤loc e  ⇒ (only({}) <loc e'') ⇒ (¬↑(P es e'')))) 
  supposing False
BY
{ Auto }

1
1. Info : Type
2. P : es:EO+(Info) ─→ E ─→ 𝔹@i'
3. es : EO+(Info)@i'
4. e : E@i
5. ∀e1:E
     ((e1 < e)
     ⇒ ((↑e1 ∈b ≤(P) ⇐⇒ ∃a:E. (a ≤loc e1  ∧ (↑(P es a))))
        ∧ ≤(P)(e1) ≤loc e1  ∧ (↑(P es ≤(P)(e1))) ∧ (∀e'':E. (e'' ≤loc e1  ⇒ (≤(P)(e1) <loc e'') ⇒ (¬↑(P es e'')))) 
          supposing ↑e1 ∈b ≤(P)))
6. ¬↑(P es e)
7. ↑first(e)
8. ∃a:E. (a ≤loc e  ∧ (↑(P es a)))@i
⊢ False

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  P  :  es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbB{}@i'
3.  es  :  EO+(Info)@i'
4.  e  :  E@i
5.  \mforall{}e1:E
          ((e1  <  e)
          {}\mRightarrow{}  ((\muparrow{}e1  \mmember{}\msubb{}  \mleq{}(P)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:E.  (a  \mleq{}loc  e1    \mwedge{}  (\muparrow{}(P  es  a))))
                \mwedge{}  \mleq{}(P)(e1)  \mleq{}loc  e1 
                    \mwedge{}  (\muparrow{}(P  es  \mleq{}(P)(e1)))
                    \mwedge{}  (\mforall{}e'':E.  (e''  \mleq{}loc  e1    {}\mRightarrow{}  (\mleq{}(P)(e1)  <loc  e'')  {}\mRightarrow{}  (\mneg{}\muparrow{}(P  es  e'')))) 
                    supposing  \muparrow{}e1  \mmember{}\msubb{}  \mleq{}(P)))
6.  \mneg{}\muparrow{}(P  es  e)
7.  \muparrow{}first(e)
\mvdash{}  (False  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:E.  (a  \mleq{}loc  e    \mwedge{}  (\muparrow{}(P  es  a))))
\mwedge{}  only(\{\})  \mleq{}loc  e 
    \mwedge{}  (\muparrow{}(P  es  only(\{\})))
    \mwedge{}  (\mforall{}e'':E.  (e''  \mleq{}loc  e    {}\mRightarrow{}  (only(\{\})  <loc  e'')  {}\mRightarrow{}  (\mneg{}\muparrow{}(P  es  e'')))) 
    supposing  False


By

---

Latex:
Auto

---

Home Index