---

Step * 1 1 of Lemma es-first-event_wf

.....subterm..... T:t
1:n
1. es : EO
2. e : E
3. P : {e':E| e' ≤loc e }  ─→ 𝔹
4. l_find(≤loc(e);P) ∈ (∃x:{E| (∃i:ℕ||≤loc(e)||. ((x = ≤loc(e)[i] ∈ E) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P ≤loc(e)[j])))))})
   ∨ (↓∀i:ℕ||≤loc(e)||. (¬↑(P ≤loc(e)[i])))
5. l_find(≤loc(e);P)
= l_find(≤loc(e);P)
∈ ((∃x:{E| (∃i:ℕ||≤loc(e)||. ((x = ≤loc(e)[i] ∈ E) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P ≤loc(e)[j])))))})
  ∨ (↓∀i:ℕ||≤loc(e)||. (¬↑(P ≤loc(e)[i]))))
6. x1 : E@i
7. i : ℕ||≤loc(e)||@i
8. x1 = ≤loc(e)[i] ∈ E@i
9. ↑(P x1)@i
10. ∀j:ℕi. (¬↑(P ≤loc(e)[j]))@i
⊢ x1 ∈ ∃e':{E| (e' ≤loc e  ∧ (↑(P e')) ∧ (∀e'':E. ((e'' <loc e') ⇒ (¬↑(P e'')))))}
BY
{ Thin 5 }

1
1. es : EO
2. e : E
3. P : {e':E| e' ≤loc e }  ─→ 𝔹
4. l_find(≤loc(e);P) ∈ (∃x:{E| (∃i:ℕ||≤loc(e)||. ((x = ≤loc(e)[i] ∈ E) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P ≤loc(e)[j])))))})
   ∨ (↓∀i:ℕ||≤loc(e)||. (¬↑(P ≤loc(e)[i])))
5. x1 : E@i
6. i : ℕ||≤loc(e)||@i
7. x1 = ≤loc(e)[i] ∈ E@i
8. ↑(P x1)@i
9. ∀j:ℕi. (¬↑(P ≤loc(e)[j]))@i
⊢ x1 ∈ ∃e':{E| (e' ≤loc e  ∧ (↑(P e')) ∧ (∀e'':E. ((e'' <loc e') ⇒ (¬↑(P e'')))))}

---

Latex:


.....subterm.....  T:t
1:n
1.  es  :  EO
2.  e  :  E
3.  P  :  \{e':E|  e'  \mleq{}loc  e  \}    {}\mrightarrow{}  \mBbbB{}
4.  l\_find(\mleq{}loc(e);P)  \mmember{}  (\mexists{}x:\{E|  (\mexists{}i:\mBbbN{}||\mleq{}loc(e)||
                                                                  ((x  =  \mleq{}loc(e)[i])  \mwedge{}  (\muparrow{}(P  x))  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(P  \mleq{}loc(e)[j])))))\})
      \mvee{}  (\mdownarrow{}\mforall{}i:\mBbbN{}||\mleq{}loc(e)||.  (\mneg{}\muparrow{}(P  \mleq{}loc(e)[i])))
5.  l\_find(\mleq{}loc(e);P)  =  l\_find(\mleq{}loc(e);P)
6.  x1  :  E@i
7.  i  :  \mBbbN{}||\mleq{}loc(e)||@i
8.  x1  =  \mleq{}loc(e)[i]@i
9.  \muparrow{}(P  x1)@i
10.  \mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(P  \mleq{}loc(e)[j]))@i
\mvdash{}  x1  \mmember{}  \mexists{}e':\{E|  (e'  \mleq{}loc  e    \mwedge{}  (\muparrow{}(P  e'))  \mwedge{}  (\mforall{}e'':E.  ((e''  <loc  e')  {}\mRightarrow{}  (\mneg{}\muparrow{}(P  e'')))))\}


By

Thin  5

---

Home Index