---

Step * 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
⊢ ∃e'≤e.e' is first@ i s.t.  e'.P[e']
BY
{ (InstLemma `es-first-at-exists` [⌈es⌉;⌈i⌉;⌈P⌉;⌈e'⌉]⋅ THENA 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
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']

---

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
\mvdash{}  \mexists{}e'\mleq{}e.e'  is  first@  i  s.t.    e'.P[e']


By

(InstLemma  `es-first-at-exists`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index