---

Step * 1 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)
8. ∃a:E. (a ≤loc e  ∧ (↑(P es a)))@i
⊢ False
BY
{ (ExRepD THEN D -2) }

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@i
9. (a <loc e)@i
10. ↑(P es a)@i
⊢ False

2
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@i
9. a = e ∈ E@i
10. ↑(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)
8.  \mexists{}a:E.  (a  \mleq{}loc  e    \mwedge{}  (\muparrow{}(P  es  a)))@i
\mvdash{}  False


By

---

Latex:
(ExRepD  THEN  D  -2)

---

Home Index