---

Step * 1 1 1 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
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. 0 ≤ i1
18. i1 < ||≤loc(e)||
19. e'' = ≤loc(e)[i1] ∈ E
20. ≤loc(e)[i1] before ≤loc(e)[i] ∈ ≤loc(e) ⇐⇒ (≤loc(e)[i1] <loc ≤loc(e)[i]) ∧ ≤loc(e)[i] ≤loc e 
⊢ i1 < i
BY
{ (D (-1) THEN Thin (-2) THEN (D (-1) THENA Auto))⋅ }

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. 0 ≤ i1
18. i1 < ||≤loc(e)||
19. e'' = ≤loc(e)[i1] ∈ E
20. ≤loc(e)[i1] before ≤loc(e)[i] ∈ ≤loc(e)
⊢ i1 < i

---

Latex:

---

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
10.  (x1  \mmember{}  \mleq{}loc(e))
11.  x1  \mleq{}loc  e 
12.  x1  \mleq{}loc  e 
13.  \muparrow{}(P  x1)
14.  e''  :  E@i
15.  (e''  <loc  x1)@i
16.  i1  :  \mBbbZ{}
17.  0  \mleq{}  i1
18.  i1  <  ||\mleq{}loc(e)||
19.  e''  =  \mleq{}loc(e)[i1]
20.  \mleq{}loc(e)[i1]  before  \mleq{}loc(e)[i]  \mmember{}  \mleq{}loc(e)  \mLeftarrow{}{}\mRightarrow{}  (\mleq{}loc(e)[i1]  <loc  \mleq{}loc(e)[i])  \mwedge{}  \mleq{}loc(e)[i]  \mleq{}loc  e 
\mvdash{}  i1  <  i


By

---

Latex:
(D  (-1)  THEN  Thin  (-2)  THEN  (D  (-1)  THENA  Auto))\mcdot{}

---

Home Index