---

{ [Info:Type]. [es:EO+(Info)]. [X,Y:EClass(Top)].
    ([e:E]. uiff(e  prior(X);e  prior(Y)))
     ([e:E]. prior(Y)(e) = prior(X)(e) supposing e  prior(X)) 
    supposing e:E. (e  X  e  Y) }

{ Proof }

---

Definitions occuring in Statement :  es-prior-interface: prior(X),  eclass-val: X(e),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-E: E,  assert: b,  uiff: uiff(P;Q),  uimplies: b supposing a,  uall: [x:A]. B[x],  top: Top,  all: x:A. B[x],  iff: P  Q,  and: P  Q,  universe: Type,  equal: s = t
Definitions :  uall: [x:A]. B[x],  top: Top,  uimplies: b supposing a,  all: x:A. B[x],  iff: P  Q,  and: P  Q,  uiff: uiff(P;Q),  member: t  T,  cand: A c B,  implies: P  Q,  exists: x:A. B[x],  rev_implies: P  Q,  prop: ,  so_lambda: x y.t[x; y],  or: P  Q,  so_apply: x[s1;s2],  subtype: S  T,  guard: {T}
Lemmas :  is-prior-interface,  es-locl_wf,  assert_wf,  in-eclass_wf,  assert_witness,  es-prior-interface_wf,  es-interface-subtype_rel2,  es-E-interface_wf,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf,  top_wf,  iff_wf,  eclass_wf,  es-prior-interface-equal,  eclass-val_wf2,  es-E-interface-subtype_rel

---

\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X,Y:EClass(Top)].
    (\mforall{}[e:E].  uiff(\muparrow{}e  \mmember{}\msubb{}  prior(X);\muparrow{}e  \mmember{}\msubb{}  prior(Y)))
    \mwedge{}  (\mforall{}[e:E].  prior(Y)(e)  =  prior(X)(e)  supposing  \muparrow{}e  \mmember{}\msubb{}  prior(X)) 
    supposing  \mforall{}e:E.  (\muparrow{}e  \mmember{}\msubb{}  X  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}e  \mmember{}\msubb{}  Y)


Date html generated: 2011_08_16-PM-04_47_25
Last ObjectModification: 2011_06_20-AM-01_05_18

Home Index