---

{ 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,  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],  rel_implies: R1 => R2,  predicate_implies: P1  P2
Definitions :  all: x:A. B[x],  uall: [x:A]. B[x],  prop: ,  implies: P  Q,  member: t  T,  guard: {T},  exists: x:A. B[x],  subtype: S  T,  suptype: suptype(S; T),  rev_implies: P  Q,  predicate_rev_implies: P1  P2,  rel_rev_implies: R1  R2,  label: ...$L... t,  rel_implies: R1 => R2,  uimplies: b supposing a,  predicate_implies: P1  P2
Lemmas :  rel_implies_wf,  es-E_wf,  predicate_implies_wf,  event_ordering_wf,  Q-R-pre-preserving_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: 2011_08_16-AM-11_07_48
Last ObjectModification: 2011_06_18-AM-09_41_11

Home Index