---

{ [Info:Type]. [es:EO+(Info)]. [X,Y:EClass(Top)]. [e:E].
    (prior(X)(e) = prior(Y)(e)) supposing 
       ((e':E
           (((prior(X)(e) <loc e')  (prior(Y)(e) <loc e'))
            (e' <loc e)
            (e'  X  e'  Y))) and 
       (e  prior(X)) and 
       (e  prior(Y))) }

{ Proof }

---

Definitions occuring in Statement :  es-prior-interface: prior(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],  top: Top,  all: x:A. B[x],  iff: P  Q,  implies: P  Q,  or: P  Q,  universe: Type,  equal: s = t
Definitions :  void: Void,  infix_ap: x f y,  es-causl: (e < e'),  es-loc: loc(e),  Id: Id,  intensional-universe: IType,  rev_implies: P  Q,  record: record(x.T[x]),  atom: Atom,  apply: f a,  es-base-E: es-base-E(es),  token: "$token",  pair: <a, b>,  bool: ,  axiom: Ax,  eclass-val: X(e),  union: left + right,  or: P  Q,  es-locl: (e <loc e'),  iff: P  Q,  implies: P  Q,  fpf: a:A fp-> B[a],  strong-subtype: strong-subtype(A;B),  record-select: r.x,  eq_atom: x =a y,  eq_atom: eq_atom$n(x;y),  decide: case b of inl(x) => s[x] | inr(y) => t[y],  ifthenelse: if b then t else f fi ,  dep-isect: Error :dep-isect,  record+: record+,  le: A  B,  ge: i  j ,  not: A,  less_than: a < b,  product: x:A  B[x],  and: P  Q,  uiff: uiff(P;Q),  set: {x:A| B[x]} ,  subtype_rel: A r B,  es-E-interface: E(X),  es-prior-interface: prior(X),  in-eclass: e  X,  prop: ,  assert: b,  uimplies: b supposing a,  subtype: S  T,  top: Top,  event_ordering: EO,  es-E: E,  lambda: x.A[x],  event-ordering+: EO+(Info),  universe: Type,  eclass: EClass(A[eo; e]),  all: x:A. B[x],  function: x:A  B[x],  member: t  T,  equal: s = t,  so_lambda: x y.t[x; y],  uall: [x:A]. B[x],  isect: x:A. B[x],  MaAuto: Error :MaAuto,  D: Error :D,  CollapseTHENA: Error :CollapseTHENA,  RepeatFor: Error :RepeatFor,  tactic: Error :tactic,  CollapseTHEN: Error :CollapseTHEN,  false: False,  cand: A c B,  inr: inr x ,  inl: inl x ,  bfalse: ff,  unit: Unit,  true: True,  btrue: tt,  guard: {T}
Lemmas :  rev_implies_wf,  not_functionality_wrt_iff,  btrue_wf,  true_wf,  bool_wf,  bfalse_wf,  false_wf,  unit_wf,  es-locl-total,  es-prior-interface-val,  es-E-interface_wf,  eclass-val_wf2,  es-prior-interface_wf,  assert_wf,  eclass-val_wf,  subtype_rel_self,  es-base-E_wf,  es-locl_wf,  es-E_wf,  iff_wf,  subtype_rel_wf,  eclass_wf,  member_wf,  es-prior-interface_wf1,  top_wf,  es-prior-interface_wf0,  in-eclass_wf,  event-ordering+_inc,  event-ordering+_wf,  intensional-universe_wf,  Id_wf,  es-loc_wf,  es-causl_wf,  es-E-interface-subtype_rel,  es-interface-subtype_rel2

---

\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X,Y:EClass(Top)].  \mforall{}[e:E].
    (prior(X)(e)  =  prior(Y)(e))  supposing 
          ((\mforall{}e':E
                  (((prior(X)(e)  <loc  e')  \mvee{}  (prior(Y)(e)  <loc  e'))
                  {}\mRightarrow{}  (e'  <loc  e)
                  {}\mRightarrow{}  (\muparrow{}e'  \mmember{}\msubb{}  X  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}e'  \mmember{}\msubb{}  Y)))  and 
          (\muparrow{}e  \mmember{}\msubb{}  prior(X))  and 
          (\muparrow{}e  \mmember{}\msubb{}  prior(Y)))


Date html generated: 2011_08_16-PM-04_47_17
Last ObjectModification: 2011_06_20-AM-01_05_11

Home Index