---

{ [Info:Type]. [es:EO+(Info)]. [X:EClass(Top)]. [f:sys-antecedent(es;X)].
  [c:Cut(X;f)]. [e:E(X)].
    ((c+e(loc(e)) = (c(loc(e)) @ [e]))
        (c+e(loc(e)) = (X)(e))
        ([i:Id]. c+e(i) = c(i) supposing (i = loc(e)))) supposing 
       ((e  c) and 
       ((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-at: c(i),  es-cut: Cut(X;f),  es-prior-interface: prior(X),  es-interface-predecessors: (X)(e),  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-loc: loc(e),  es-eq: es-eq(es),  Id: Id,  append: as @ bs,  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  top: Top,  not: A,  implies: P  Q,  and: P  Q,  set: {x:A| B[x]} ,  apply: f a,  cons: [car / cdr],  nil: [],  list: type List,  universe: Type,  equal: s = t,  fset-member: a  s
Definitions :  all: x:A. B[x],  member: t  T,  prop: ,  trans: Trans(T;x,y.E[x; y]),  implies: P  Q,  true: True,  ifthenelse: if b then t else f fi ,  btrue: tt,  anti_sym: AntiSym(T;x,y.R[x; y]),  assert: b,  es-E-interface: E(X),  set-equal: set-equal(T;x;y),  so_lambda: x.t[x],  rev_implies: P  Q,  iff: P  Q,  or: P  Q,  cand: A c B,  subtype: S  T,  and: P  Q,  guard: {T},  es-cut-add: c+e,  l_all: (xL.P[x]),  not: A,  decidable: Dec(P),  es-le: e loc e' ,  false: False,  exists: x:A. B[x],  uimplies: b supposing a,  uall: [x:A]. B[x],  sq_type: SQType(T),  so_apply: x[s],  es-cut: Cut(X;f),  uiff: uiff(P;Q)
Lemmas :  es-cut-at_wf,  append_wf,  es-le_wf,  event-ordering+_inc,  es-loc_wf,  Id_wf,  es-E-interface_wf,  sorted-by-unique,  es-le_transitivity,  assert_elim,  in-eclass_wf,  assert_wf,  bool_subtype_base,  bool_wf,  subtype_base_sq,  es-causle_weakening_locl,  es-causle_antisymmetry,  es-cut-at-property,  member_append,  l_member-settype,  member_singleton,  or_functionality_wrt_iff,  iff_functionality_wrt_iff,  fset-member_wf-cut,  l_member_wf,  es-eq_wf-interface,  decidable__fset-member,  decidable__equal_Id,  decidable__cand,  es-eq_wf,  es-E_wf,  fset-member_wf,  fset-singleton_wf,  member-fset-union,  member-fset-singleton,  iff_weakening_uiff,  es-cut-at-property1,  list-set-type2,  sq_stable__equal,  property-from-l_member,  es-locl_wf,  es-le-not-locl,  es-cut-locl-closed,  sorted-by-append1,  l_disjoint_singleton,  and_functionality_wrt_uiff3,  no_repeats-single,  not_wf,  no_repeats-append,  l_disjoint_wf,  guard_wf,  no_repeats_wf,  no_repeats-settype,  es-interface-predecessors_wf,  member-interface-predecessors,  or_functionality_wrt_uiff2,  and_functionality_wrt_iff,  fset-union_wf,  decidable__equal_es-E-interface,  decidable__es-le,  decidable__es-locl,  assert_witness,  es-is-prior-interface,  es-le-prior-interface-val,  es-prior-interface_wf,  eclass-val_wf2,  es-cut-le-closed,  es-interface-predecessors-sorted-by-le,  es-interface-predecessors-no_repeats

---

\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(loc(e))  =  (c(loc(e))  @  [e]))
          \mwedge{}  (c+e(loc(e))  =  \mleq{}(X)(e))
          \mwedge{}  (\mforall{}[i:Id].  c+e(i)  =  c(i)  supposing  \mneg{}(i  =  loc(e))))  supposing 
          ((\mneg{}e  \mmember{}  c)  and 
          ((\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_41
Last ObjectModification: 2011_06_20-AM-01_36_56

Home Index