---

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

∀es:EO
  ∀[P1,P2:E ─→ ℙ]. ∀[Q1,R1,Q2,R2:E ─→ E ─→ ℙ].
    ∀f:{e:E| P1 e}  ─→ E
      (P2 ⇒ P1 ⇒ Q2 => Q1 ⇒ R1 => R2 ⇒ {f is Q1-R1-pre-preserving on P1 ⇒ f is Q2-R2-pre-preserving on P2})
BY
{ 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
⊢ {f is Q1-R1-pre-preserving on P1 ⇒ f is Q2-R2-pre-preserving on P2}

---

Latex:


\mforall{}es:EO
    \mforall{}[P1,P2:E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Q1,R1,Q2,R2:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].
        \mforall{}f:\{e:E|  P1  e\}    {}\mrightarrow{}  E
            (P2  {}\mRightarrow{}  P1
            {}\mRightarrow{}  Q2  =>  Q1
            {}\mRightarrow{}  R1  =>  R2
            {}\mRightarrow{}  \{f  is  Q1-R1-pre-preserving  on  P1  {}\mRightarrow{}  f  is  Q2-R2-pre-preserving  on  P2\})


By

Auto

---

Home Index