---

Step * of Lemma es-pplus-trivial

∀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 ≤loc e2  ⇒ Q[e1;e2] ⇒ [e1,e2]~([a,b].Q[a;b])+)
BY
{ ((InstLemma `es-pstar-q-trivial` [])
   THEN Unfold `es-pplus` 0
   THEN RepeatFor 4 (ParallelLast)
   THEN (SimpleInstHyp ⌈Q⌉ (-1))⋅
   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  \mleq{}loc  e2    {}\mRightarrow{}  Q[e1;e2]  {}\mRightarrow{}  [e1,e2]\msim{}([a,b].Q[a;b])+)


By

((InstLemma  `es-pstar-q-trivial`  [])
  THEN  Unfold  `es-pplus`  0
  THEN  RepeatFor  4  (ParallelLast)
  THEN  (SimpleInstHyp  \mkleeneopen{}Q\mkleeneclose{}  (-1))\mcdot{}
  THEN  Auto)

---

Home Index