### Nuprl Lemma : Q-R-pre-preserving_functionality_wrt_implies

`∀es:EO`
`  ∀[P1,P2:E ─→ ℙ]. ∀[Q1,R1,Q2,R2:E ─→ E ─→ ℙ].`
`    ∀f:{e:E| P1 e}  ─→ E`
`      (P1 `` P2 `` Q1 `` Q2 `` 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_rev_implies: `P1 `` P2` rel_rev_implies: `R1 `` R2` rel_implies: `R1 => R2` uall: `∀[x:A]. B[x]` prop: `ℙ` guard: `{T}` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ─→ B[x]` equal: `s = t ∈ T`
Lemmas :  subtype_rel_sets es-E_wf set_wf all_wf exists_wf equal_wf event_ordering_wf
\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
(P1  \mLeftarrow{}{}  P2
{}\mRightarrow{}  Q1  \mLeftarrow{}{}  Q2
{}\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_01
Last ObjectModification: 2015_01_27-PM-00_55_14

Home Index