---

Step * 1 2 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. ∀i:ℕ||≤loc(e)||. (¬↑(P ≤loc(e)[i]))@i
⊢ (λx.Ax) %2 ∈ ↓∀e':E. (e' ≤loc e  ⇒ (¬↑(P e')))
BY
{ (Reduce 0⋅
   THEN MemTypeCD
   THEN Auto
   THEN (FLemma `member-es-le-before` [-1] THENA Auto)
   THEN D -1
   THEN InstHyp [⌈i⌉] (-5)⋅
   THEN Auto) }

---

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.  \mforall{}i:\mBbbN{}||\mleq{}loc(e)||.  (\mneg{}\muparrow{}(P  \mleq{}loc(e)[i]))@i
\mvdash{}  (\mlambda{}x.Ax)  \%2  \mmember{}  \mdownarrow{}\mforall{}e':E.  (e'  \mleq{}loc  e    {}\mRightarrow{}  (\mneg{}\muparrow{}(P  e')))


By

(Reduce  0\mcdot{}
  THEN  MemTypeCD
  THEN  Auto
  THEN  (FLemma  `member-es-le-before`  [-1]  THENA  Auto)
  THEN  D  -1
  THEN  InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-5)\mcdot{}
  THEN  Auto)

---

Home Index