---

{ [poss:EO  ']. [R:PossibleEvent(poss)  PossibleEvent(poss)  '].
    (Trans(PossibleEvent(poss))(R _1 _2)
     (e1,e2:PossibleEvent(poss).  (e1  e2  (R e1 e2)))
     ([P:PossibleEvent(poss)  ']
          e1,e2:PossibleEvent(poss).  (e1  e2  K(P)@e1  K(P)@e2))) }

{ Proof }

---

Definitions occuring in Statement :  poss-le: e1  e2,  es-knows: K(P)@e,  possible-event: PossibleEvent(poss),  event_ordering: EO,  trans: Trans(T;x,y.E[x; y]),  uall: [x:A]. B[x],  prop: ,  all: x:A. B[x],  implies: P  Q,  apply: f a,  function: x:A  B[x]
Definitions :  uall: [x:A]. B[x],  prop: ,  implies: P  Q,  all: x:A. B[x],  es-knows: K(P)@e,  member: t  T,  so_lambda: x y.t[x; y],  so_apply: x[s1;s2],  trans: Trans(T;x,y.E[x; y]),  guard: {T}
Lemmas :  possible-event_wf,  poss-le_wf,  trans_wf,  event_ordering_wf

---

\mforall{}[poss:EO  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}[R:PossibleEvent(poss)  {}\mrightarrow{}  PossibleEvent(poss)  {}\mrightarrow{}  \mBbbP{}'].
    (Trans(PossibleEvent(poss))(R  $_{1}$  $_{2}$)
    {}\mRightarrow{}  (\mforall{}e1,e2:PossibleEvent(poss).    (e1  \mleq{}  e2  {}\mRightarrow{}  (R  e1  e2)))
    {}\mRightarrow{}  (\mforall{}[P:PossibleEvent(poss)  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}e1,e2:PossibleEvent(poss).    (e1  \mleq{}  e2  {}\mRightarrow{}  K(P)@e1  {}\mRightarrow{}  K(P)@e2)))


Date html generated: 2011_08_16-AM-10_54_38
Last ObjectModification: 2011_06_18-AM-09_28_04

Home Index