---

{ [Info:Type]. [es:EO+(Info)]. [X:EClass(Top)]. [i:Id]. [s:FSet{E(X)}].
    (s@i  E(X) List) }

{ Proof }

---

Definitions occuring in Statement :  es-E-interface: E(X),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-fset-at: s@i,  Id: Id,  uall: [x:A]. B[x],  top: Top,  member: t  T,  list: type List,  universe: Type,  fset: FSet{s}
Definitions :  prop: ,  member: t  T,  implies: P  Q,  all: x:A. B[x],  l_all: (xL.P[x]),  ifthenelse: if b then t else f fi ,  btrue: tt,  true: True,  squash: T,  assert: b,  rev_implies: P  Q,  uimplies: b supposing a,  uall: [x:A]. B[x],  iff: P  Q,  and: P  Q,  guard: {T},  sq_type: SQType(T),  es-E-interface: E(X),  subtype: S  T
Lemmas :  event-ordering+_inc,  es-fset-at_wf,  l_member_wf,  es-E-interface-strong-subtype,  es-E_wf,  es-E-interface_wf,  subtype_rel_fset,  es-fset-at-property,  assert_elim,  bool_subtype_base,  bool_wf,  subtype_base_sq,  in-eclass_wf,  assert_wf,  es-eq_wf,  strong-subtype-fset-member-type

---

\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[i:Id].  \mforall{}[s:FSet\{E(X)\}].    (s@i  \mmember{}  E(X)  List)


Date html generated: 2011_08_16-PM-05_45_46
Last ObjectModification: 2011_06_20-AM-01_33_07

Home Index