---

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

.....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. R1 => R2
⊢ ...GenFormulaCondC: failed... R1 => R2
BY
{ (Unfold `label` 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
13. R1 => R2
⊢ R1 => R2

---

Latex:


.....debug..... 
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.  R1  =>  R2
\mvdash{}  ...GenFormulaCondC:  failed...  R1  =>  R2


By

(Unfold  `label`  0  THEN  Auto)\mcdot{}

---

Home Index