---

Step * 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
⊢ {f is Q1-R1-pre-preserving on P1 ⇒ f is Q2-R2-pre-preserving on P2}
BY
{ (Unfold `guard` 0 THEN Auto) }

1
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
⊢ f is Q2-R2-pre-preserving on P2

---

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
\mvdash{}  \{f  is  Q1-R1-pre-preserving  on  P1  {}\mRightarrow{}  f  is  Q2-R2-pre-preserving  on  P2\}


By

(Unfold  `guard`  0  THEN  Auto)

---

Home Index