---

Step * of Lemma existse-le-iff

∀es:EO. ∀e':E.  ∀[P:{e:E| loc(e) = loc(e') ∈ Id}  ─→ ℙ]. (∃e≤e'.P[e] ⇐⇒ P[e'] ∨ ∃e<e'.P[e])
BY
{ Auto ⋅ }

1
1. es : EO@i'
2. e' : E@i
3. [P] : {e:E| loc(e) = loc(e') ∈ Id}  ─→ ℙ
4. ∃e≤e'.P[e]@i
⊢ P[e'] ∨ ∃e<e'.P[e]

2
1. es : EO@i'
2. e' : E@i
3. [P] : {e:E| loc(e) = loc(e') ∈ Id}  ─→ ℙ
4. P[e'] ∨ ∃e<e'.P[e]@i
⊢ ∃e≤e'.P[e]

---

Latex:


\mforall{}es:EO.  \mforall{}e':E.    \mforall{}[P:\{e:E|  loc(e)  =  loc(e')\}    {}\mrightarrow{}  \mBbbP{}].  (\mexists{}e\mleq{}e'.P[e]  \mLeftarrow{}{}\mRightarrow{}  P[e']  \mvee{}  \mexists{}e<e'.P[e])


By

Auto  \mcdot{}

---

Home Index