---

Step * of Lemma es-pplus-le

∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[Q:{e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ]. ([e1,e2]~([a,b].Q[a;b])+ ⇒ e1 ≤loc e2 )
BY
{ ((InstLemma `es-pstar-q-le` [])
   THEN RepeatFor 4 (ParallelLast)
   THEN (SimpleInstHyp ⌈Q⌉ (-1))⋅
   THEN Auto
   THEN (D (-2))
   THEN Auto) }

---

Latex:


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


By

((InstLemma  `es-pstar-q-le`  [])
  THEN  RepeatFor  4  (ParallelLast)
  THEN  (SimpleInstHyp  \mkleeneopen{}Q\mkleeneclose{}  (-1))\mcdot{}
  THEN  Auto
  THEN  (D  (-2))
  THEN  Auto)

---

Home Index