---

Step * of Lemma es-pplus_functionality_wrt_rev_implies

∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[p,p':{e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ].
    ((∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ {p[a;b] ⇐ p'[a;b]}))
    ⇒ {[e1,e2]~([a,b].p[a;b])+ ⇐ [e1,e2]~([a,b].p'[a;b])+})
BY
{ ((InstLemma `es-pstar-q_functionality_wrt_rev_implies` [])
   THEN Auto
   THEN Unfold `es-pplus` 0
   THEN (InstHyp [⌈es⌉; ⌈e1⌉; ⌈e2⌉; ⌈p'⌉; ⌈p'⌉; ⌈p⌉; ⌈p⌉] 1)⋅
   THEN Try (Trivial)
   THEN Unfold `guard` 0
   THEN Trivial) }

---

Latex:


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


By

((InstLemma  `es-pstar-q\_functionality\_wrt\_rev\_implies`  [])
  THEN  Auto
  THEN  Unfold  `es-pplus`  0
  THEN  (InstHyp  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}e1\mkleeneclose{};  \mkleeneopen{}e2\mkleeneclose{};  \mkleeneopen{}p'\mkleeneclose{};  \mkleeneopen{}p'\mkleeneclose{};  \mkleeneopen{}p\mkleeneclose{};  \mkleeneopen{}p\mkleeneclose{}]  1)\mcdot{}
  THEN  Try  (Trivial)
  THEN  Unfold  `guard`  0
  THEN  Trivial)

---

Home Index