---

{ 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,  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,  rel_implies: R1 => R2,  predicate_rev_implies: P1  P2,  rel_rev_implies: R1  R2
Definitions :  all: x:A. B[x],  uall: [x:A]. B[x],  prop: ,  implies: P  Q,  predicate_rev_implies: P1  P2,  rel_rev_implies: R1  R2,  exists: x:A. B[x],  rel_implies: R1 => R2,  guard: {T},  Q-R-pre-preserving: f is Q-R-pre-preserving on P,  predicate_implies: P1  P2,  infix_ap: x f y,  member: t  T
Lemmas :  es-E_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: 2011_08_16-AM-11_07_41
Last ObjectModification: 2011_06_18-AM-09_41_05

Home Index