Step
*
1
2
1
1
of Lemma
es-first-at-exists
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. ∀e1:E. ((e1 < e)
⇒ P[e1]
⇒ (∃e':E. (e' ≤loc e1 ∧ e' is first@ i s.t. e.P[e])) supposing loc(e1) = i ∈ Id)
7. loc(e) = i ∈ Id
8. P[e]@i
9. ¬∃e<e.P[e]
10. e ≤loc e
11. P[e]
12. e' : E@i
13. (e' <loc e)@i
14. P[e']@i
⊢ False
BY
{ OnMaybeHyp 9 (\h. (D h THEN With ⌈e'⌉ (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. \mforall{}e1:E
((e1 < e)
{}\mRightarrow{} P[e1] {}\mRightarrow{} (\mexists{}e':E. (e' \mleq{}loc e1 \mwedge{} e' is first@ i s.t. e.P[e])) supposing loc(e1) = i)
7. loc(e) = i
8. P[e]@i
9. \mneg{}\mexists{}e<e.P[e]
10. e \mleq{}loc e
11. P[e]
12. e' : E@i
13. (e' <loc e)@i
14. P[e']@i
\mvdash{} False
By
OnMaybeHyp 9 (\mbackslash{}h. (D h THEN With \mkleeneopen{}e'\mkleeneclose{} (D 0)\mcdot{} THEN Auto))
Home
Index