---

Step * of Lemma es-pstar-q-le

∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[p,q:{e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ].
    ([e1;e2]~([a,b].p[a;b])*[a,b].q[a;b] ⇒ e1 ≤loc e2 )
BY
{ (Auto THEN (D (-1)) THEN ExRepD) }

1
1. es : EO@i'
2. e1 : E@i
3. e2 : {e:E| loc(e) = loc(e1) ∈ Id} @i
4. [p] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
5. [q] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
6. m : ℕ+@i
7. f : ℕm ─→ {e:E| loc(e) = loc(e1) ∈ Id} @i
8. (f 0) = e1 ∈ E@i
9. f (m - 1) ≤loc e2 @i
10. ∀i:ℕm - 1. (f i <loc f (i + 1))@i
11. ∀i:ℕm - 1. p[f i;pred(f (i + 1))]@i
12. q[f (m - 1);e2]@i
⊢ e1 ≤loc e2 

---

Latex:


\mforall{}es:EO.  \mforall{}e1:E.  \mforall{}e2:\{e:E|  loc(e)  =  loc(e1)\}  .
    \mforall{}[p,q:\{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \mBbbP{}].
        ([e1;e2]\msim{}([a,b].p[a;b])*[a,b].q[a;b]  {}\mRightarrow{}  e1  \mleq{}loc  e2  )


By

(Auto  THEN  (D  (-1))  THEN  ExRepD)

---

Home Index