---

Step * 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
⊢ f is Q2-R2-pre-preserving on P1
BY
{ (RWO "10" 0 THEN Auto)⋅ }

1
.....debug..... 
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
⊢ ...GenFormulaCondC: failed... Q2 => Q1

2
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 Q1-R2-pre-preserving on P1

---

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


By

(RWO  "10"  0  THEN  Auto)\mcdot{}

---

Home Index