---

Step * of Lemma alle-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
{ (Unfolds ``alle-lt alle-le`` 0 THEN Auto THEN Try ((BackThruSomeHyp THEN Complete (Auto)))) }

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

---

Latex:


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


By

(Unfolds  ``alle-lt  alle-le``  0  THEN  Auto  THEN  Try  ((BackThruSomeHyp  THEN  Complete  (Auto))))

---

Home Index