---

Step * 1 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']
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
BY
{ (With ⌈e'⌉ (D 5)⋅ THEN Auto) }

---

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']
6.  e'  :  E@i
7.  e'  \mleq{}loc  e  @i
8.  loc(e')  =  loc(e)@i
9.  P[e']@i
10.  \mforall{}e'<e'.\mneg{}P[e']@i
\mvdash{}  False


By

(With  \mkleeneopen{}e'\mkleeneclose{}  (D  5)\mcdot{}  THEN  Auto)

---

Home Index