---

Step * 1 1 1 1 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
9. e' ≤loc e 
10. P[e']
11. loc(e') = i ∈ Id
12. ∃e'@0:E. (e'@0 ≤loc e'  ∧ e'@0 is first@ i s.t.  e.P[e])
⊢ ∃e'≤e.e' is first@ i s.t.  e'.P[e']
BY
{ (D (-1) THEN RenameVar `x' (-2) THEN With ⌈x⌉ (D 0)⋅ THEN Auto) }

---

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.  e'  :  E
9.  e'  \mleq{}loc  e 
10.  P[e']
11.  loc(e')  =  i
12.  \mexists{}e'@0:E.  (e'@0  \mleq{}loc  e'    \mwedge{}  e'@0  is  first@  i  s.t.    e.P[e])
\mvdash{}  \mexists{}e'\mleq{}e.e'  is  first@  i  s.t.    e'.P[e']


By

(D  (-1)  THEN  RenameVar  `x'  (-2)  THEN  With  \mkleeneopen{}x\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index