---

Step * of Lemma es-interval-induction

∀es:EO. ∀i:Id.
  ∀[P:e1:{e:E| loc(e) = i ∈ Id}  ─→ {e2:E| loc(e2) = i ∈ Id}  ─→ ℙ]
    (∀e1@i.∀e2≥e1.(∀e:E. ((e1 <loc e) ⇒ e ≤loc e2  ⇒ P[e;e2])) ⇒ P[e1;e2] ⇒ ∀e1@i.∀e2≥e1.P[e1;e2])
BY
{ ((Repeat ((D 0 THENA Complete (Auto))) THEN D 0) THENA (Unfold `alle-ge` 0 THEN Auto)) }

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

---

Latex:


\mforall{}es:EO.  \mforall{}i:Id.
    \mforall{}[P:e1:\{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \{e2:E|  loc(e2)  =  i\}    {}\mrightarrow{}  \mBbbP{}]
        (\mforall{}e1@i.\mforall{}e2\mgeq{}e1.(\mforall{}e:E.  ((e1  <loc  e)  {}\mRightarrow{}  e  \mleq{}loc  e2    {}\mRightarrow{}  P[e;e2]))  {}\mRightarrow{}  P[e1;e2]
        {}\mRightarrow{}  \mforall{}e1@i.\mforall{}e2\mgeq{}e1.P[e1;e2])


By

((Repeat  ((D  0  THENA  Complete  (Auto)))  THEN  D  0)  THENA  (Unfold  `alle-ge`  0  THEN  Auto))

---

Home Index