---

Step * 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)
⊢ (↑(#(if first(e) then {} else ≤(P) es pred(e) fi ) =z 1) ⇐⇒ ∃a:E. (a ≤loc e  ∧ (↑(P es a))))
∧ only(if first(e) then {} else ≤(P) es pred(e) fi ) ≤loc e 
  ∧ (↑(P es only(if first(e) then {} else ≤(P) es pred(e) fi )))
  ∧ (∀e'':E. (e'' ≤loc e  ⇒ (only(if first(e) then {} else ≤(P) es pred(e) fi ) <loc e'') ⇒ (¬↑(P es e'')))) 
  supposing ↑(#(if first(e) then {} else ≤(P) es pred(e) fi ) =z 1)
BY
{ OldAutoSplit }

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)
⊢ (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

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)
⊢ (↑(#(≤(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)

---

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


By

---

Latex:
OldAutoSplit

---

Home Index