---

Step * of Lemma es-pstar-q_functionality_wrt_iff

∀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
{ ((((UnivCD THENA Auto) THEN (InstLemma `es-pstar-q_wf` [⌈es⌉; ⌈e1⌉; ⌈e2⌉; ⌈p⌉; ⌈q⌉])⋅) THENA Auto)
   THEN (InstLemma `es-pstar-q_wf` [⌈es⌉; ⌈e1⌉; ⌈e2⌉; ⌈p'⌉; ⌈q'⌉])⋅
   THEN Auto) }

1
1. es : EO@i'
2. e1 : E@i
3. e2 : {e:E| loc(e) = loc(e1) ∈ Id} @i
4. [p] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
5. [q] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
6. [p'] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
7. [q'] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
8. ∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ (p[a;b] ⇐⇒ p'[a;b]))@i
9. ∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ (q[a;b] ⇐⇒ q'[a;b]))@i
10. [e1;e2]~([a,b].p[a;b])*[a,b].q[a;b] ∈ ℙ
11. [e1;e2]~([a,b].p'[a;b])*[a,b].q'[a;b] ∈ ℙ
12. [e1;e2]~([a,b].p[a;b])*[a,b].q[a;b]@i
⊢ [e1;e2]~([a,b].p'[a;b])*[a,b].q'[a;b]

2
1. es : EO@i'
2. e1 : E@i
3. e2 : {e:E| loc(e) = loc(e1) ∈ Id} @i
4. [p] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
5. [q] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
6. [p'] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
7. [q'] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
8. ∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ (p[a;b] ⇐⇒ p'[a;b]))@i
9. ∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ (q[a;b] ⇐⇒ q'[a;b]))@i
10. [e1;e2]~([a,b].p[a;b])*[a,b].q[a;b] ∈ ℙ
11. [e1;e2]~([a,b].p'[a;b])*[a,b].q'[a;b] ∈ ℙ
12. [e1;e2]~([a,b].p'[a;b])*[a,b].q'[a;b]@i
⊢ [e1;e2]~([a,b].p[a;b])*[a,b].q[a;b]

---

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{}{}\mRightarrow{}  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{}{}\mRightarrow{}  q'[a;b])))
        {}\mRightarrow{}  ([e1;e2]\msim{}([a,b].p[a;b])*[a,b].q[a;b]  \mLeftarrow{}{}\mRightarrow{}  [e1;e2]\msim{}([a,b].p'[a;b])*[a,b].q'[a;b]))


By

((((UnivCD  THENA  Auto)  THEN  (InstLemma  `es-pstar-q\_wf`  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}e1\mkleeneclose{};  \mkleeneopen{}e2\mkleeneclose{};  \mkleeneopen{}p\mkleeneclose{};  \mkleeneopen{}q\mkleeneclose{}])\mcdot{})  THENA  Auto)
  THEN  (InstLemma  `es-pstar-q\_wf`  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}e1\mkleeneclose{};  \mkleeneopen{}e2\mkleeneclose{};  \mkleeneopen{}p'\mkleeneclose{};  \mkleeneopen{}q'\mkleeneclose{}])\mcdot{}
  THEN  Auto)

---

Home Index