---

Step * of Lemma es-pplus_functionality_wrt_iff

∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[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] ⇐⇒ q[a;b])))
    ⇒ ([e1,e2]~([a,b].p[a;b])+ ⇐⇒ [e1,e2]~([a,b].q[a;b])+))
BY
{ ((((((((InstLemma `es-pstar-q_functionality_wrt_iff` []) THEN RepeatFor 4 (ParallelLast) THEN (InstHyp [⌈p⌉] (-1))⋅)
        THENA Auto
        )
       THEN (Thin (-2))
       THEN ParallelLast
       THEN (SimpleInstHyp ⌈q⌉ (-1))⋅)
      THENA Auto
      )
     THEN Unfold `es-pplus` 0
     THEN D 0)
    THENA Auto
    )
   THEN ThinTrivial
   THEN ThinTrivial
   THEN Trivial) }

---

Latex:


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


By

((((((((InstLemma  `es-pstar-q\_functionality\_wrt\_iff`  [])
              THEN  RepeatFor  4  (ParallelLast)
              THEN  (InstHyp  [\mkleeneopen{}p\mkleeneclose{}]  (-1))\mcdot{})
            THENA  Auto
            )
          THEN  (Thin  (-2))
          THEN  ParallelLast
          THEN  (SimpleInstHyp  \mkleeneopen{}q\mkleeneclose{}  (-1))\mcdot{})
        THENA  Auto
        )
      THEN  Unfold  `es-pplus`  0
      THEN  D  0)
    THENA  Auto
    )
  THEN  ThinTrivial
  THEN  ThinTrivial
  THEN  Trivial)

---

Home Index