---

Step * of Lemma es-pstar-q_functionality_wrt_rev_implies

∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[p',q',p,q:{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]}))
    ⇒ (∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ {q[a;b] ⇐ q'[a;b]}))
    ⇒ {[e1;e2]~([a,b].p[a;b])*[a,b].q[a;b] ⇐ [e1;e2]~([a,b].p'[a;b])*[a,b].q'[a;b]})
BY
{ ((InstLemma `es-pstar-q_functionality_wrt_implies` []) THEN Unfold `rev_implies` 0 THEN Trivial) }

---

Latex:


\mforall{}es:EO.  \mforall{}e1:E.  \mforall{}e2:\{e:E|  loc(e)  =  loc(e1)\}  .
    \mforall{}[p',q',p,q:\{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{}  (\mforall{}a,b:\{e:E|  loc(e)  =  loc(e1)\}  .    ((a  \mmember{}  [e1,  e2])  {}\mRightarrow{}  (b  \mmember{}  [e1,  e2])  {}\mRightarrow{}  \{q[a;b]  \mLeftarrow{}{}  q'[a;b]\}))
        {}\mRightarrow{}  \{[e1;e2]\msim{}([a,b].p[a;b])*[a,b].q[a;b]  \mLeftarrow{}{}  [e1;e2]\msim{}([a,b].p'[a;b])*[a,b].q'[a;b]\})


By

((InstLemma  `es-pstar-q\_functionality\_wrt\_implies`  [])  THEN  Unfold  `rev\_implies`  0  THEN  Trivial)

---

Home Index