---

Step * 1 of Lemma es-first-at-exists-cases


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

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

---

Latex:



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


By

((D  0  THENA  Auto)  THEN  RepeatFor  2  ((D  -1  THEN  ExRepD)))

---

Home Index