---

{ [Info:Type]
    es:EO+(Info). X:EClass(Top). f:sys-antecedent(es;X). c:Cut(X;f).
    e,a:E(X).
      (a  c+e  (a = e)  a  c) }

{ Proof }

---

Definitions occuring in Statement :  es-cut-add: c+e,  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-eq: es-eq(es),  uall: [x:A]. B[x],  top: Top,  all: x:A. B[x],  iff: P  Q,  or: P  Q,  universe: Type,  equal: s = t,  fset-member: a  s
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  es-cut: Cut(X;f),  iff: P  Q,  es-cut-add: c+e,  or: P  Q,  member: t  T,  prop: ,  so_lambda: x y.t[x; y],  and: P  Q,  implies: P  Q,  rev_implies: P  Q,  sys-antecedent: sys-antecedent(es;Sys),  so_apply: x[s1;s2],  subtype: S  T
Lemmas :  es-E-interface_wf,  fset_wf,  fset-closed_wf,  es-eq_wf-interface,  es-interface-pred_wf2,  sys-antecedent_wf,  eclass_wf,  top_wf,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf,  fset-member_wf,  fset-union_wf,  fset-singleton_wf,  decidable__fset-member,  iff_functionality_wrt_iff,  iff_weakening_uiff,  or_functionality_wrt_uiff2,  member-fset-singleton,  member-fset-union

---

\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}f:sys-antecedent(es;X).  \mforall{}c:Cut(X;f).  \mforall{}e,a:E(X).
        (a  \mmember{}  c+e  \mLeftarrow{}{}\mRightarrow{}  (a  =  e)  \mvee{}  a  \mmember{}  c)


Date html generated: 2011_08_16-PM-05_51_25
Last ObjectModification: 2011_06_20-AM-01_36_48

Home Index