---

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

{ Proof }

---

Definitions occuring in Statement :  es-interface-predecessors: (X)(e),  es-E-interface: E(X),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-E: E,  uiff: uiff(P;Q),  uall: [x:A]. B[x],  top: Top,  list: type List,  universe: Type,  equal: s = t
Definitions :  uall: [x:A]. B[x],  uiff: uiff(P;Q),  member: t  T,  and: P  Q,  uimplies: b supposing a,  prop: ,  all: x:A. B[x],  subtype: S  T,  so_lambda: x y.t[x; y],  squash: T,  true: True,  es-E-interface: E(X),  so_apply: x[s1;s2],  iff: P  Q,  implies: P  Q
Lemmas :  es-E-interface_wf,  es-interface-predecessors_wf,  Id_wf,  es-loc_wf,  es-E_wf,  eclass_wf,  top_wf,  event-ordering+_wf,  event-ordering+_inc,  es-interface-predecessors-iseg,  iseg_weakening,  iseg_wf,  es-causle_antisymmetry,  es-causle_weakening_locl

---

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


Date html generated: 2011_08_16-PM-05_18_18
Last ObjectModification: 2011_06_20-AM-01_19_51

Home Index