---

Step * 2 1 1 of Lemma es-first-at-since-iff

.....antecedent..... 
1. es : EO@i'
2. i : Id@i
3. e : E@i
4. [P] : {e:E| loc(e) = i ∈ Id}  ─→ ℙ
5. [R] : {e:E| loc(e) = i ∈ Id}  ─→ ℙ
6. ∀e:E. Dec(R[e]) supposing loc(e) = i ∈ Id@i
7. loc(e) = i ∈ Id@i
8. P[e]@i
9. ¬R[e]@i
10. P[e]
11. ¬R[e]
12. e' : E@i
13. (e' <loc e)@i
14. P[e']@i
⊢ ∃e'':E. ((e'' <loc e) c∧ P[e''])
BY
{ ((InstConcl [e'])⋅ THEN Auto)⋅ }

---

Latex:


.....antecedent..... 
1.  es  :  EO@i'
2.  i  :  Id@i
3.  e  :  E@i
4.  [P]  :  \{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}
5.  [R]  :  \{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}
6.  \mforall{}e:E.  Dec(R[e])  supposing  loc(e)  =  i@i
7.  loc(e)  =  i@i
8.  P[e]@i
9.  \mneg{}R[e]@i
10.  P[e]
11.  \mneg{}R[e]
12.  e'  :  E@i
13.  (e'  <loc  e)@i
14.  P[e']@i
\mvdash{}  \mexists{}e'':E.  ((e''  <loc  e)  c\mwedge{}  P[e''])


By

((InstConcl  [e'])\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index