---

{ [Info:Type]. es:EO+(Info). X:EClass(Top). e,e':E(X).  Dec(e = e') }

{ Proof }

---

Definitions occuring in Statement :  es-E-interface: E(X),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  decidable: Dec(P),  uall: [x:A]. B[x],  top: Top,  all: x:A. B[x],  universe: Type,  equal: s = t
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  member: t  T,  so_lambda: x y.t[x; y],  prop: ,  so_apply: x[s1;s2],  es-E-interface: E(X),  rev_implies: P  Q,  iff: P  Q,  implies: P  Q,  and: P  Q,  subtype: S  T
Lemmas :  es-E-interface_wf,  eclass_wf,  top_wf,  es-E_wf,  event-ordering+_wf,  deq_property,  es-eq_wf-interface,  assert_wf,  eqof_wf,  event-ordering+_inc,  es-eq_wf,  decidable__assert,  decidable_functionality,  iff_weakening_uiff

---

\mforall{}[Info:Type].  \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}e,e':E(X).    Dec(e  =  e')


Date html generated: 2011_08_16-AM-11_44_05
Last ObjectModification: 2011_06_20-AM-00_34_35

Home Index