Nuprl 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})`

Proof

Definitions occuring in Statement :  Q-R-pre-preserving: `f is Q-R-pre-preserving on P` es-E: `E` event_ordering: `EO` predicate_implies: `P1 `` P2` rel_implies: `R1 => R2` uall: `∀[x:A]. B[x]` prop: `ℙ` guard: `{T}` all: `∀x:A. B[x]` implies: `P `` Q` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ─→ B[x]`
Lemmas :  Q-R-pre-preserving_wf es-E_wf exists_wf equal_wf subtype_rel_dep_function subtype_rel_self set_wf Q-R-pre-preserving_functionality_wrt_implies rel_implies_weakening rel_equivalent_weakening rel_equivalent_inversion predicate_implies_weakening predicate_equivalent_weakening predicate_equivalent_inversion
\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\})

Date html generated: 2015_07_17-AM-09_03_08
Last ObjectModification: 2015_01_27-PM-00_56_13

Home Index