---

{ [Info,T:Type].
    es:EO+(Info). X:EClass(T).
      [P:T  ]
        ((e:E(X)
            (P[X(e)] supposing e  (X)'
             P[(X)'(e)]  P[X(e)] supposing e  (X)'))
         (e:E(X). P[X(e)])) }

{ Proof }

---

Definitions occuring in Statement :  es-prior-val: (X)',  es-E-interface: E(X),  eclass-val: X(e),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  prop: ,  so_apply: x[s],  all: x:A. B[x],  not: A,  implies: P  Q,  and: P  Q,  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  prop: ,  implies: P  Q,  and: P  Q,  uimplies: b supposing a,  assert: b,  so_apply: x[s],  member: t  T,  cand: A c B,  so_lambda: x y.t[x; y],  btrue: tt,  ifthenelse: if b then t else f fi ,  true: True,  not: A,  nat: ,  ge: i  j ,  le: A  B,  false: False,  squash: T,  es-E-interface: E(X),  so_apply: x[s1;s2],  sq_type: SQType(T),  guard: {T},  decidable: Dec(P),  or: P  Q,  strongwellfounded: SWellFounded(R[x; y]),  exists: x:A. B[x],  es-locl: (e <loc e'),  subtype: S  T
Lemmas :  es-E-interface_wf,  not_wf,  assert_wf,  in-eclass_wf,  es-prior-val_wf,  top_wf,  eclass-val_wf,  es-E_wf,  event-ordering+_wf,  subtype_base_sq,  bool_subtype_base,  event-ordering+_inc,  bool_wf,  eclass_wf,  assert_elim,  decidable__assert,  es-interface-top,  es-causl-swellfnd,  nat_properties,  ge_wf,  nat_wf,  le_wf,  es-causl_wf,  assert_witness,  prior-val-val

---

\mforall{}[Info,T:Type].
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(T).
        \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}]
            ((\mforall{}e:E(X).  (P[X(e)]  supposing  \mneg{}\muparrow{}e  \mmember{}\msubb{}  (X)'  \mwedge{}  P[(X)'(e)]  {}\mRightarrow{}  P[X(e)]  supposing  \muparrow{}e  \mmember{}\msubb{}  (X)'))
            {}\mRightarrow{}  (\mforall{}e:E(X).  P[X(e)]))


Date html generated: 2011_08_16-PM-05_09_05
Last ObjectModification: 2011_06_20-AM-01_12_03

Home Index