---

Step * of Lemma es-pplus_functionality_wrt_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_implies` [])
         THEN RepeatFor 4 (ParallelLast)
         THEN (InstHyp [⌈p⌉] (-1))⋅)
        THENA Auto
        )
       THEN (Thin (-2))
       THEN ParallelLast
       THEN (SimpleInstHyp ⌈p'⌉ (-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,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]  {}\mRightarrow{}  p'[a;b]\}))
        {}\mRightarrow{}  \{[e1,e2]\msim{}([a,b].p[a;b])+  {}\mRightarrow{}  [e1,e2]\msim{}([a,b].p'[a;b])+\})


By

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

---

Home Index