---

{ [Info:Type]. [es:EO+(Info)]. [X,Y:EClass(Top)]. [d:Top].
    (E((X'?d) when Y) = E(Y)) }

{ Proof }

---

Definitions occuring in Statement :  es-prior-class-when: (X'?d) when Y,  es-E-interface: E(X),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  uall: [x:A]. B[x],  top: Top,  universe: Type,  equal: s = t
Definitions :  uall: [x:A]. B[x],  es-E-interface: E(X),  member: t  T,  prop: ,  so_lambda: x y.t[x; y],  all: x:A. B[x],  so_apply: x[s1;s2],  subtype: S  T
Lemmas :  es-E_wf,  event-ordering+_inc,  is-prior-class-when,  assert_wf,  in-eclass_wf,  top_wf,  eclass_wf,  event-ordering+_wf

---

\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X,Y:EClass(Top)].  \mforall{}[d:Top].    (E((X'?d)  when  Y)  =  E(Y))


Date html generated: 2011_08_16-PM-05_40_51
Last ObjectModification: 2011_06_20-AM-01_30_14

Home Index