---

Step * 2 2 1 1 of Lemma es-pstar-q_functionality_wrt_iff

.....assertion..... 
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
13. ∀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]})
BY
{ (Unfold `guard` 0 THEN ParallelOp 9 THEN RepeatFor 3 (ParallelLast) THEN Auto) }

---

Latex:


.....assertion..... 
1.  es  :  EO@i'
2.  e1  :  E@i
3.  e2  :  \{e:E|  loc(e)  =  loc(e1)\}  @i
4.  [p]  :  \{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \mBbbP{}
5.  [q]  :  \{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \mBbbP{}
6.  [p']  :  \{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \mBbbP{}
7.  [q']  :  \{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \mBbbP{}
8.  \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]))@i
9.  \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]))@i
10.  [e1;e2]\msim{}([a,b].p[a;b])*[a,b].q[a;b]  \mmember{}  \mBbbP{}
11.  [e1;e2]\msim{}([a,b].p'[a;b])*[a,b].q'[a;b]  \mmember{}  \mBbbP{}
12.  [e1;e2]\msim{}([a,b].p'[a;b])*[a,b].q'[a;b]@i
13.  \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]\})
\mvdash{}  \mforall{}a,b:\{e:E|  loc(e)  =  loc(e1)\}  .    ((a  \mmember{}  [e1,  e2])  {}\mRightarrow{}  (b  \mmember{}  [e1,  e2])  {}\mRightarrow{}  \{q'[a;b]  {}\mRightarrow{}  q[a;b]\})


By

(Unfold  `guard`  0  THEN  ParallelOp  9  THEN  RepeatFor  3  (ParallelLast)  THEN  Auto)

---

Home Index