---

Step * 1 1 1 1 1 of Lemma Q-R-pre-preserving-rewrite-test


1. es : EO@i'
2. [P1] : E ─→ ℙ
3. [P2] : E ─→ ℙ
4. [Q1] : E ─→ E ─→ ℙ
5. [R1] : E ─→ E ─→ ℙ
6. [Q2] : E ─→ E ─→ ℙ
7. [R2] : E ─→ E ─→ ℙ
8. f : {e:E| P1 e}  ─→ E@i
9. P2 ⇒ P1@i
10. Q2 => Q1@i
11. R1 => R2@i
12. f is Q1-R1-pre-preserving on P1@i
13. Q2 => Q1
⊢ Q2 => Q1
BY
{ (RepeatFor 2 (ParallelOp (-4)) THEN ParallelLast) }

---

Latex:



1.  es  :  EO@i'
2.  [P1]  :  E  {}\mrightarrow{}  \mBbbP{}
3.  [P2]  :  E  {}\mrightarrow{}  \mBbbP{}
4.  [Q1]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
5.  [R1]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
6.  [Q2]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
7.  [R2]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
8.  f  :  \{e:E|  P1  e\}    {}\mrightarrow{}  E@i
9.  P2  {}\mRightarrow{}  P1@i
10.  Q2  =>  Q1@i
11.  R1  =>  R2@i
12.  f  is  Q1-R1-pre-preserving  on  P1@i
13.  Q2  =>  Q1
\mvdash{}  Q2  =>  Q1


By

(RepeatFor  2  (ParallelOp  (-4))  THEN  ParallelLast)

---

Home Index