---

Step * of Lemma alle-lt-iff

∀es:EO. ∀e':E.
  ∀[P:{e:E| loc(e) = loc(e') ∈ Id}  ─→ ℙ]. (∀e<e'.P[e] ⇐⇒ P[pred(e')] ∧ ∀e<pred(e').P[e] supposing ¬↑first(e'))
BY
{ (Unfold `alle-lt` 0 THEN Auto) }

1
1. es : EO@i'
2. e' : E@i
3. [P] : {e:E| loc(e) = loc(e') ∈ Id}  ─→ ℙ
4. P[pred(e')] ∧ (∀e:E. ((e <loc pred(e')) ⇒ P[e])) supposing ¬↑first(e')@i
5. e : E@i
6. (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<e'.P[e]  \mLeftarrow{}{}\mRightarrow{}  P[pred(e')]  \mwedge{}  \mforall{}e<pred(e').P[e]  supposing  \mneg{}\muparrow{}first(e'))


By

(Unfold  `alle-lt`  0  THEN  Auto)

---

Home Index