---

Step * 1 of Lemma es-first-event_wf


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])))
⊢ l_find(≤loc(e);P) ∈ (∃e':{E| (e' ≤loc e  ∧ (↑(P e')) ∧ (∀e'':E. ((e'' <loc e') ⇒ (¬↑(P e'')))))})
  ∨ (↓∀e':E. (e' ≤loc e  ⇒ (¬↑(P e'))))
BY
{ ((DoSubsume THEN Auto)
   THEN Try (Complete (((MemTypeCD THEN Auto)
                        THEN RWO "member-es-le-before<" 0
                        THEN Auto
                        THEN (HypSubst' (-1) 0 THENA Auto)
                        THEN BLemma `select_member`
                        THEN Auto)))
   THEN DProdsAndUnions
   THEN MemCD
   THEN Try (Complete (Auto))) }

1
.....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'')))))}

2
.....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')))

---

Latex:



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])))
\mvdash{}  l\_find(\mleq{}loc(e);P)  \mmember{}  (\mexists{}e':\{E|  (e'  \mleq{}loc  e    \mwedge{}  (\muparrow{}(P  e'))  \mwedge{}  (\mforall{}e'':E.  ((e''  <loc  e')  {}\mRightarrow{}  (\mneg{}\muparrow{}(P  e'')))))\})
    \mvee{}  (\mdownarrow{}\mforall{}e':E.  (e'  \mleq{}loc  e    {}\mRightarrow{}  (\mneg{}\muparrow{}(P  e'))))


By

((DoSubsume  THEN  Auto)
  THEN  Try  (Complete  (((MemTypeCD  THEN  Auto)
                                            THEN  RWO  "member-es-le-before<"  0
                                            THEN  Auto
                                            THEN  (HypSubst'  (-1)  0  THENA  Auto)
                                            THEN  BLemma  `select\_member`
                                            THEN  Auto)))
  THEN  DProdsAndUnions
  THEN  MemCD
  THEN  Try  (Complete  (Auto)))

---

Home Index