---

{ [poss:EO  ']. [R:PossibleEvent(poss)  PossibleEvent(poss)  '].
  [P:PossibleEvent(poss)  ']. [e:PossibleEvent(poss)].
    (K(P)@e  ') }

{ Proof }

---

Definitions occuring in Statement :  es-knows: K(P)@e,  possible-event: PossibleEvent(poss),  event_ordering: EO,  uall: [x:A]. B[x],  prop: ,  member: t  T,  function: x:A  B[x]
Definitions :  uall: [x:A]. B[x],  prop: ,  member: t  T,  es-knows: K(P)@e,  all: x:A. B[x],  implies: P  Q
Lemmas :  possible-event_wf,  event_ordering_wf

---

\mforall{}[poss:EO  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}[R:PossibleEvent(poss)  {}\mrightarrow{}  PossibleEvent(poss)  {}\mrightarrow{}  \mBbbP{}'].
\mforall{}[P:PossibleEvent(poss)  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}[e:PossibleEvent(poss)].
    (K(P)@e  \mmember{}  \mBbbP{}')


Date html generated: 2011_08_16-AM-10_54_03
Last ObjectModification: 2011_06_18-AM-09_27_22

Home Index