---

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

{ Proof }

---

Definitions occuring in Statement :  es-cut-add: c+e,  es-cut: Cut(X;f),  es-prior-interface: prior(X),  sys-antecedent: sys-antecedent(es;Sys),  es-E-interface: E(X),  eclass-val: X(e),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-eq: es-eq(es),  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  top: Top,  not: A,  implies: P  Q,  member: t  T,  apply: f a,  universe: Type,  equal: s = t,  fset-member: a  s
Definitions :  member: t  T,  all: x:A. B[x],  implies: P  Q,  or: P  Q,  and: P  Q,  guard: {T},  iff: P  Q,  false: False,  prop:
Lemmas :  nil_member,  l_member_wf

---

\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[f:sys-antecedent(es;X)].  \mforall{}[c:Cut(X;f)].
\mforall{}[e:E(X)].
    (c+e  \mmember{}  Cut(X;f))  supposing  (((\muparrow{}e  \mmember{}\msubb{}  prior(X))  {}\mRightarrow{}  prior(X)(e)  \mmember{}  c)  and  ((\mneg{}((f  e)  =  e))  {}\mRightarrow{}  f  e  \mmember{}  c))


Date html generated: 2011_08_16-PM-05_51_16
Last ObjectModification: 2011_06_20-AM-01_36_40

Home Index