---

{ [Info:Type]. [es:EO+(Info)]. [T:Type]. [X:EClass(T)]. [i:Id]. [e:E].
    X@i(e) ~ X(e) supposing e  X@i }

{ Proof }

---

Definitions occuring in Statement :  es-interface-at: X@i,  eclass-val: X(e),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-E: E,  Id: Id,  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  universe: Type,  sqequal: s ~ t
Definitions :  es-interface-at: X@i,  eclass-val: X(e),  implies: P  Q,  and: P  Q,  prop: ,  member: t  T,  do-apply: do-apply(f;x),  ifthenelse: if b then t else f fi ,  bfalse: ff,  all: x:A. B[x],  btrue: tt,  so_lambda: x y.t[x; y],  iff: P  Q,  uall: [x:A]. B[x],  bool: ,  unit: Unit,  not: A,  false: False,  so_apply: x[s1;s2],  it: ,  subtype: S  T
Lemmas :  iff_weakening_uiff,  assert_wf,  in-eclass_wf,  es-interface-at_wf,  es-loc_wf,  is-interface-at,  eq_id_wf,  bool_wf,  uiff_transitivity,  eqtt_to_assert,  assert-eq-id,  not_wf,  bnot_wf,  eqff_to_assert,  assert_of_bnot,  not_functionality_wrt_uiff,  top_wf,  es-interface-top,  es-E_wf,  event-ordering+_inc,  Id_wf,  eclass_wf,  event-ordering+_wf

---

\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[i:Id].  \mforall{}[e:E].
    X@i(e)  \msim{}  X(e)  supposing  \muparrow{}e  \mmember{}\msubb{}  X@i


Date html generated: 2011_08_16-PM-04_30_44
Last ObjectModification: 2011_06_20-AM-00_52_47

Home Index