---

Step * of Lemma es-pplus-partition

∀es:EO. ∀e1,e2,b:E.
  ∀[Q:{e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ]
    ((e1 <loc b) ⇒ b ≤loc e2  ⇒ [e1,pred(b)]~([a,b].Q[a;b])+ ⇒ [b,e2]~([a,b].Q[a;b])+ ⇒ [e1,e2]~([a,b].Q[a;b])+)
BY
{ (Auto THEN Auto THEN (All (Unfold `es-pplus`)) THEN (Using [`b',⌈b⌉] (BLemma `es-pstar-q-partition`))⋅ THEN Auto) }

---

Latex:


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


By

(Auto
  THEN  Auto
  THEN  (All  (Unfold  `es-pplus`))
  THEN  (Using  [`b',\mkleeneopen{}b\mkleeneclose{}]  (BLemma  `es-pstar-q-partition`))\mcdot{}
  THEN  Auto)

---

Home Index