---

{ [Info:Type]. [es:EO+(Info)]. [X:EClass(Top)]. [f:sys-antecedent(es;X)].
  [c:Cut(X;f)]. [i:Id].
    (c(i)  {e:E(X)| loc(e) = i}  List) }

{ Proof }

---

Definitions occuring in Statement :  es-cut-at: c(i),  es-cut: Cut(X;f),  sys-antecedent: sys-antecedent(es;Sys),  es-E-interface: E(X),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-loc: loc(e),  Id: Id,  uall: [x:A]. B[x],  top: Top,  member: t  T,  set: {x:A| B[x]} ,  list: type List,  universe: Type,  equal: s = t
Definitions :  member: t  T,  so_lambda: x.t[x],  prop: ,  implies: P  Q,  all: x:A. B[x],  l_all: (xL.P[x]),  cand: A c B,  exists: x:A. B[x],  l_member: (x  l),  uall: [x:A]. B[x],  es-cut: Cut(X;f),  so_apply: x[s],  uimplies: b supposing a,  es-E-interface: E(X),  iff: P  Q,  and: P  Q,  rev_implies: P  Q,  nat: ,  subtype: S  T
Lemmas :  es-fset-at_wf-interface,  event-ordering+_inc,  es-loc_wf,  Id_wf,  es-E-interface_wf,  list-set-type2,  l_member_wf,  es-E-interface-strong-subtype,  es-E_wf,  subtype_rel_fset,  es-fset-at-property,  select_wf,  length_wf1

---

\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[f:sys-antecedent(es;X)].  \mforall{}[c:Cut(X;f)].  \mforall{}[i:Id].
    (c(i)  \mmember{}  \{e:E(X)|  loc(e)  =  i\}    List)


Date html generated: 2011_08_16-PM-05_48_16
Last ObjectModification: 2011_06_20-AM-01_34_17

Home Index