---

{ es:EO. s:FSet{E}. i:Id.  Dec(i  locs(s)) }

{ Proof }

---

Definitions occuring in Statement :  es-fset-loc: i  locs(s),  es-E: E,  event_ordering: EO,  Id: Id,  decidable: Dec(P),  all: x:A. B[x],  fset: FSet{s}
Definitions :  all: x:A. B[x],  es-fset-loc: i  locs(s),  member: t  T,  top: Top,  subtype: S  T,  implies: P  Q
Lemmas :  decidable__not,  assert_wf,  null_wf3,  es-fset-at_wf,  top_wf,  es-E_wf,  decidable__assert,  Id_wf,  fset_wf,  event_ordering_wf

---

\mforall{}es:EO.  \mforall{}s:FSet\{E\}.  \mforall{}i:Id.    Dec(i  \mmember{}  locs(s))


Date html generated: 2011_08_16-AM-11_05_40
Last ObjectModification: 2010_09_24-PM-08_51_47

Home Index