---

Step * 1 1 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])))
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'')))))}
BY
{ ((Assert ⌈(x1 ∈ ≤loc(e))⌉⋅ THENA (UnfoldTopAb 0 THEN InstConcl [⌈i⌉]⋅ THEN Auto))
   THEN (FLemma `member-es-le-before` [-1] THENA Auto)
   THEN (MemTypeCD THEN Auto)
   THEN (Assert ⌈e'' ≤loc e ⌉⋅ THENA Auto)
   THEN (RWO "member-es-le-before<" (-1) THENA Auto)
   THEN D (-1))⋅ }

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
10. (x1 ∈ ≤loc(e))
11. x1 ≤loc e 
12. x1 ≤loc e 
13. ↑(P x1)
14. e'' : E@i
15. (e'' <loc x1)@i
16. i1 : ℕ
17. i1 < ||≤loc(e)|| c∧ (e'' = ≤loc(e)[i1] ∈ 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])))
5.  x1  :  E@i
6.  i  :  \mBbbN{}||\mleq{}loc(e)||@i
7.  x1  =  \mleq{}loc(e)[i]@i
8.  \muparrow{}(P  x1)@i
9.  \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

((Assert  \mkleeneopen{}(x1  \mmember{}  \mleq{}loc(e))\mkleeneclose{}\mcdot{}  THENA  (UnfoldTopAb  0  THEN  InstConcl  [\mkleeneopen{}i\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  (FLemma  `member-es-le-before`  [-1]  THENA  Auto)
  THEN  (MemTypeCD  THEN  Auto)
  THEN  (Assert  \mkleeneopen{}e''  \mleq{}loc  e  \mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (RWO  "member-es-le-before<"  (-1)  THENA  Auto)
  THEN  D  (-1))\mcdot{}

---

Home Index