---

{ [T:Type]. [es:EO']. [e:E]. [v1,v2:T]. [hdr:Name]. [locs:bag(Id)].
    (v1  Base(hdr;locs;T)(e)  v2  Base(hdr;locs;T)(e)  (v1 = v2)) }

{ Proof }

---

Definitions occuring in Statement :  base-headers-msg-val-loc: Base(hdr;locs;typ),  Message: Message,  classrel: v  X(e),  event-ordering+: EO+(Info),  es-E: E,  Id: Id,  name: Name,  uall: [x:A]. B[x],  implies: P  Q,  universe: Type,  equal: s = t,  bag: bag(T)
Definitions :  CollapseTHENA: Error :CollapseTHENA,  D: Error :D,  CollapseTHEN: Error :CollapseTHEN,  ExRepD: Error :ExRepD,  Auto: Error :Auto,  name: Name,  member: t  T,  isect: x:A. B[x],  uall: [x:A]. B[x],  es-E: E,  event_ordering: EO,  event-ordering+: EO+(Info),  Message: Message,  equal: s = t,  function: x:A  B[x],  implies: P  Q,  universe: Type,  bag: bag(T),  Id: Id,  lambda: x.A[x],  classrel: v  X(e),  base-headers-msg-val-loc: Base(hdr;locs;typ),  axiom: Ax,  prop: ,  all: x:A. B[x],  subtype: S  T,  uiff: uiff(P;Q),  and: P  Q,  product: x:A  B[x],  uimplies: b supposing a,  squash: T,  set: {x:A| B[x]} ,  true: True,  bag-member: bag-member(T;x;bs),  assert: b
Lemmas :  base-classrel,  event-ordering+_inc,  event-ordering+_wf,  es-E_wf,  name_wf,  Id_wf,  bag_wf,  classrel_wf,  base-headers-msg-val-loc_wf,  Message_wf

---

\mforall{}[T:Type].  \mforall{}[es:EO'].  \mforall{}[e:E].  \mforall{}[v1,v2:T].  \mforall{}[hdr:Name].  \mforall{}[locs:bag(Id)].
    (v1  \mmember{}  Base(hdr;locs;T)(e)  {}\mRightarrow{}  v2  \mmember{}  Base(hdr;locs;T)(e)  {}\mRightarrow{}  (v1  =  v2))


Date html generated: 2011_08_17-PM-06_25_19
Last ObjectModification: 2011_06_16-AM-11_34_24

Home Index