---

Step * 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. i1 < ||≤loc(e)|| c∧ (e'' = ≤loc(e)[i1] ∈ E)
⊢ ¬↑(P e'')
BY
{ (ExRepD THEN StrongHypSubst (-1) 0 THEN BackThruSomeHyp) }

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
⊢ i1 < i

---

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  :  \mBbbN{}
17.  i1  <  ||\mleq{}loc(e)||  c\mwedge{}  (e''  =  \mleq{}loc(e)[i1])
\mvdash{}  \mneg{}\muparrow{}(P  e'')


By

(ExRepD  THEN  StrongHypSubst  (-1)  0  THEN  BackThruSomeHyp)

---

Home Index