---

Step * 2 of Lemma es-first-at-exists2


1. es : EO@i'
2. i : Id@i
3. [P] : {e:E| loc(e) = i ∈ Id}  ─→ ℙ
4. ∀e:{e:E| loc(e) = i ∈ Id} . Dec(P[e])@i
5. e : E@i
6. loc(e) = i ∈ Id
7. ¬∀e'≤e.¬P[e']
8. ¬∃e'≤e.P[e']
⊢ ∃e'≤e.e' is first@ i s.t.  e'.P[e']
BY
{ (D (-2) THEN RepeatFor 2 ((D 0 THEN Auto))) }

1
1. es : EO@i'
2. i : Id@i
3. P : {e:E| loc(e) = i ∈ Id}  ─→ ℙ
4. ∀e:{e:E| loc(e) = i ∈ Id} . Dec(P[e])@i
5. e : E@i
6. loc(e) = i ∈ Id
7. ¬∃e'≤e.P[e']
8. e' : E@i
9. e' ≤loc e @i
10. P[e']@i
⊢ False

---

Latex:



1.  es  :  EO@i'
2.  i  :  Id@i
3.  [P]  :  \{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}e:\{e:E|  loc(e)  =  i\}  .  Dec(P[e])@i
5.  e  :  E@i
6.  loc(e)  =  i
7.  \mneg{}\mforall{}e'\mleq{}e.\mneg{}P[e']
8.  \mneg{}\mexists{}e'\mleq{}e.P[e']
\mvdash{}  \mexists{}e'\mleq{}e.e'  is  first@  i  s.t.    e'.P[e']


By

(D  (-2)  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index