---

Step * 1 2 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)
⊢ (↑(#(≤(P) es pred(e)) =z 1) ⇐⇒ ∃a:E. (a ≤loc e  ∧ (↑(P es a))))
∧ only(≤(P) es pred(e)) ≤loc e 
  ∧ (↑(P es only(≤(P) es pred(e))))
  ∧ (∀e'':E. (e'' ≤loc e  ⇒ (only(≤(P) es pred(e)) <loc e'') ⇒ (¬↑(P es e'')))) 
  supposing ↑(#(≤(P) es pred(e)) =z 1)
BY
{ ((InstHyp [⌈pred(e)⌉] (-3)⋅ THENA Auto) THEN Folds ``in-eclass eclass-val`` 0 THEN ParallelLast) }

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. ≤(P)(pred(e)) ≤loc pred(e) 
   ∧ (↑(P es ≤(P)(pred(e))))
   ∧ (∀e'':E. (e'' ≤loc pred(e)  ⇒ (≤(P)(pred(e)) <loc e'') ⇒ (¬↑(P es e'')))) 
   supposing ↑pred(e) ∈b ≤(P)
9. ↑pred(e) ∈b ≤(P) ⇐⇒ ∃a:E. (a ≤loc pred(e)  ∧ (↑(P es a)))
⊢ ↑pred(e) ∈b ≤(P) ⇐⇒ ∃a:E. (a ≤loc e  ∧ (↑(P es a)))

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. ↑pred(e) ∈b ≤(P) ⇐⇒ ∃a:E. (a ≤loc pred(e)  ∧ (↑(P es a)))
9. ≤(P)(pred(e)) ≤loc pred(e) 
   ∧ (↑(P es ≤(P)(pred(e))))
   ∧ (∀e'':E. (e'' ≤loc pred(e)  ⇒ (≤(P)(pred(e)) <loc e'') ⇒ (¬↑(P es e'')))) 
   supposing ↑pred(e) ∈b ≤(P)
⊢ ≤(P)(pred(e)) ≤loc e 
  ∧ (↑(P es ≤(P)(pred(e))))
  ∧ (∀e'':E. (e'' ≤loc e  ⇒ (≤(P)(pred(e)) <loc e'') ⇒ (¬↑(P es e'')))) 
  supposing ↑pred(e) ∈b ≤(P)

---

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.  \mneg{}\muparrow{}first(e)
\mvdash{}  (\muparrow{}(\#(\mleq{}(P)  es  pred(e))  =\msubz{}  1)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:E.  (a  \mleq{}loc  e    \mwedge{}  (\muparrow{}(P  es  a))))
\mwedge{}  only(\mleq{}(P)  es  pred(e))  \mleq{}loc  e 
    \mwedge{}  (\muparrow{}(P  es  only(\mleq{}(P)  es  pred(e))))
    \mwedge{}  (\mforall{}e'':E.  (e''  \mleq{}loc  e    {}\mRightarrow{}  (only(\mleq{}(P)  es  pred(e))  <loc  e'')  {}\mRightarrow{}  (\mneg{}\muparrow{}(P  es  e'')))) 
    supposing  \muparrow{}(\#(\mleq{}(P)  es  pred(e))  =\msubz{}  1)


By

---

Latex:
((InstHyp  [\mkleeneopen{}pred(e)\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)  THEN  Folds  ``in-eclass  eclass-val``  0  THEN  ParallelLast)

---

Home Index