---

{ [Info:Type]
    es:EO+(Info). X:EClass(Top). f:sys-antecedent(es;X).
      [P:Cut(X;f)  ]
        (((R:E(X)  E(X)  
            (Linorder(E(X);x,y.R[x;y])  (x,y:E(X).  Dec(R[x;y]))))
          (c:Cut(X;f). SqStable(P[c])))
         P[{}]
         (c:Cut(X;f). e:E(X).
              (P[c]  P[c+e] supposing add-cut-conditions(c;e)))
         {c:Cut(X;f). P[c]}) }

{ Proof }

---

Definitions occuring in Statement :  add-cut-conditions: add-cut-conditions(c;e),  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),  linorder: Linorder(T;x,y.R[x; y]),  sq_stable: SqStable(P),  decidable: Dec(P),  uimplies: b supposing a,  uall: [x:A]. B[x],  top: Top,  prop: ,  guard: {T},  so_apply: x[s1;s2],  so_apply: x[s],  all: x:A. B[x],  exists: x:A. B[x],  implies: P  Q,  or: P  Q,  and: P  Q,  function: x:A  B[x],  universe: Type,  empty-fset: {}
Definitions :  so_lambda: x y.t[x; y],  cand: A c B,  member: t  T,  uimplies: b supposing a,  so_apply: x[s],  so_apply: x[s1;s2],  and: P  Q,  exists: x:A. B[x],  or: P  Q,  implies: P  Q,  prop: ,  all: x:A. B[x],  uall: [x:A]. B[x],  top: Top,  es-cut: Cut(X;f),  true: True,  squash: T,  add-cut-conditions: add-cut-conditions(c;e),  rev_implies: P  Q,  iff: P  Q,  guard: {T},  Id: Id,  es-E-interface: E(X),  sys-antecedent: sys-antecedent(es;Sys),  decidable: Dec(P),  sq_stable: SqStable(P),  ifthenelse: if b then t else f fi ,  btrue: tt,  bfalse: ff,  sq_type: SQType(T),  es-locl: (e <loc e'),  false: False,  not: A,  subtype: S  T
Lemmas :  event-ordering+_wf,  es-E_wf,  top_wf,  eclass_wf,  sys-antecedent_wf,  sq_stable_wf,  decidable_wf,  linorder_wf,  empty-fset_wf-cut,  es-cut-add_wf,  add-cut-conditions_wf,  es-E-interface_wf,  es-cut_wf,  not_wf,  eclass-val_wf2,  fset-member_wf-cut,  event-ordering+_inc,  es-interface-subtype_rel2,  es-prior-interface_wf,  in-eclass_wf,  assert_wf,  es-eq_wf-interface,  decidable__fset-member,  es-interface-pred_wf2,  fset-closed_wf,  member-fset-singleton,  fset-singleton_wf,  fset-member_wf,  iff_weakening_uiff,  decidable__fset-closed,  sq_stable_from_decidable,  es-cut-add-at,  es-loc_wf,  Id_wf,  es-interface-predecessors-step,  bnot_wf,  bool_wf,  bool_cases,  subtype_base_sq,  bool_subtype_base,  eqtt_to_assert,  uiff_transitivity,  eqff_to_assert,  assert_of_bnot,  es-interface-predecessors_wf,  es-E-interface-subtype_rel,  length_wf1,  es-cut-at_wf,  general-append-cancellation,  atom2_subtype_base,  es-prior-interface-val,  member-cut-add

---

\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}f:sys-antecedent(es;X).
        \mforall{}[P:Cut(X;f)  {}\mrightarrow{}  \mBbbP{}]
            (((\mexists{}R:E(X)  {}\mrightarrow{}  E(X)  {}\mrightarrow{}  \mBbbP{}.  (Linorder(E(X);x,y.R[x;y])  \mwedge{}  (\mforall{}x,y:E(X).    Dec(R[x;y]))))
              \mvee{}  (\mforall{}c:Cut(X;f).  SqStable(P[c])))
            {}\mRightarrow{}  P[\{\}]
            {}\mRightarrow{}  (\mforall{}c:Cut(X;f).  \mforall{}e:E(X).    (P[c]  {}\mRightarrow{}  P[c+e]  supposing  add-cut-conditions(c;e)))
            {}\mRightarrow{}  \{\mforall{}c:Cut(X;f).  P[c]\})


Date html generated: 2011_08_16-PM-05_53_14
Last ObjectModification: 2011_06_20-AM-01_37_46

Home Index