---

{ [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]))))
         P[{}]
         (c:Cut(X;f). e:E(X).
              (P[c]
               (P[c+e]) supposing 
                    (prior(X)(e)  c supposing e  prior(X) and 
                    f e  c supposing ((f e) = e))))
         (c:Cut(X;f). P[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),  linorder: Linorder(T;x,y.R[x; y]),  assert: b,  decidable: Dec(P),  uimplies: b supposing a,  uall: [x:A]. B[x],  top: Top,  prop: ,  so_apply: x[s1;s2],  so_apply: x[s],  all: x:A. B[x],  exists: x:A. B[x],  not: A,  implies: P  Q,  and: P  Q,  apply: f a,  function: x:A  B[x],  universe: Type,  equal: s = t,  empty-fset: {},  fset-member: a  s
Definitions :  cand: A c B,  so_lambda: x y.t[x; y],  member: t  T,  uimplies: b supposing a,  so_apply: x[s],  so_apply: x[s1;s2],  and: P  Q,  exists: x:A. B[x],  implies: P  Q,  prop: ,  top: Top,  all: x:A. B[x],  uall: [x:A]. B[x],  false: False,  ge: i  j ,  le: A  B,  nat: ,  not: A,  es-cut: Cut(X;f),  es-cut-add: c+e,  rev_implies: P  Q,  iff: P  Q,  true: True,  squash: T,  or: P  Q,  so_lambda: x.t[x],  es-E-interface: E(X),  sys-antecedent: sys-antecedent(es;Sys),  decidable: Dec(P),  sq_stable: SqStable(P),  uiff: uiff(P;Q),  guard: {T},  sq_type: SQType(T),  l_all: (xL.P[x]),  fset-closed: (s closed under fs),  subtype: S  T,  fset-add: fset-add(eq;x;s)
Lemmas :  eclass_wf,  sys-antecedent_wf,  decidable_wf,  linorder_wf,  empty-fset_wf-cut,  es-cut-add_wf,  eclass-val_wf2,  top_wf,  event-ordering+_wf,  event-ordering+_inc,  es-E_wf,  es-interface-subtype_rel2,  es-prior-interface_wf,  in-eclass_wf,  assert_wf,  fset-member_wf-cut,  not_wf,  es-E-interface_wf,  es-cut_wf,  fset-size_wf,  le_wf,  nat_wf,  ge_wf,  nat_properties,  es-eq_wf-interface,  empty-fset_wf,  decidable__equal_fset,  decidable__equal_es-E-interface,  fset_wf,  es-interface-pred_wf2,  fset-closed_wf,  empty-fset-closed,  es-causl_wf,  fset-add-remove,  decidable__fset-closed,  sq_stable_from_decidable,  es-cut-remove,  fset-size-empty,  int_subtype_base,  subtype_base_sq,  fset-size-remove,  true_wf,  squash_wf,  l_member_wf,  cons_member,  member-fset-remove,  iff_weakening_uiff,  decidable__fset-member,  fset-remove_wf,  fset-member_wf,  fset-to-list,  exists_functionality_wrt_iff,  and_functionality_wrt_iff,  all_functionality_wrt_iff,  implies_functionality_wrt_iff,  Error :Girard-theorem2,  es-causl-maximal-exists

---

\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]))))
            {}\mRightarrow{}  P[\{\}]
            {}\mRightarrow{}  (\mforall{}c:Cut(X;f).  \mforall{}e:E(X).
                        (P[c]
                        {}\mRightarrow{}  (P[c+e])  supposing 
                                    (prior(X)(e)  \mmember{}  c  supposing  \muparrow{}e  \mmember{}\msubb{}  prior(X)  and 
                                    f  e  \mmember{}  c  supposing  \mneg{}((f  e)  =  e))))
            {}\mRightarrow{}  (\mforall{}c:Cut(X;f).  P[c]))


Date html generated: 2011_08_16-PM-05_52_53
Last ObjectModification: 2011_06_20-AM-01_37_29

Home Index