---

{ [Info:Type]. [es:EO+(Info)]. [T:Type]. [X:EClass(T)]. [e:E]. [e':E(X)].
    ({(e  (X)')  ((X)'(e) = X(e'))}) supposing 
       ((e'':E. ((e' <loc e'')  (e'' <loc e)  (e''  X))) and 
       (e' <loc 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),  es-locl: (e <loc e'),  es-E: E,  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  guard: {T},  all: x:A. B[x],  not: A,  implies: P  Q,  and: P  Q,  universe: Type,  equal: s = t
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  all: x:A. B[x],  implies: P  Q,  assert: b,  guard: {T},  and: P  Q,  exists: x:A. B[x],  member: t  T,  cand: A c B,  btrue: tt,  ifthenelse: if b then t else f fi ,  true: True,  prop: ,  so_lambda: x y.t[x; y],  squash: T,  es-E-interface: E(X),  iff: P  Q,  rev_implies: P  Q,  sq_type: SQType(T),  so_apply: x[s1;s2],  es-locl: (e <loc e'),  not: A,  or: P  Q,  false: False,  subtype: S  T
Lemmas :  prior-val-val,  is-prior-val,  subtype_base_sq,  bool_wf,  bool_subtype_base,  es-locl_wf,  assert_wf,  in-eclass_wf,  assert_witness,  es-prior-val_wf,  top_wf,  es-interface-top,  es-E_wf,  event-ordering+_inc,  not_wf,  es-E-interface_wf,  eclass_wf,  event-ordering+_wf,  assert_elim,  eclass-val_wf,  squash_wf,  true_wf,  es-locl-total,  btrue_neq_bfalse,  not_assert_elim

---

\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[e:E].  \mforall{}[e':E(X)].
    (\{(\muparrow{}e  \mmember{}\msubb{}  (X)')  \mwedge{}  ((X)'(e)  =  X(e'))\})  supposing 
          ((\mforall{}e'':E.  ((e'  <loc  e'')  {}\mRightarrow{}  (e''  <loc  e)  {}\mRightarrow{}  (\mneg{}\muparrow{}e''  \mmember{}\msubb{}  X)))  and 
          (e'  <loc  e))


Date html generated: 2011_08_16-PM-05_06_50
Last ObjectModification: 2011_06_20-AM-01_10_55

Home Index