---

{ [es:EO]. [p:E  (E + Top)].
    [A:E  ]
      ([e,e':E].  (same-thread(es;p;e;e')) supposing (A[e'] and A[e])) supposin\000Cg 
         ((x:{e:E| A[e]} 
            y:{e:E| A[e]} 
              ((y = x)  ((can-apply(p;y))  A[do-apply(p;y)]))) and 
         p-inject({e:E| A[e]} ;E;p)) 
    supposing causal-predecessor(es;p) }

{ Proof }

---

Definitions occuring in Statement :  same-thread: same-thread(es;p;e;e'),  causal-predecessor: causal-predecessor(es;p),  es-E: E,  event_ordering: EO,  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  top: Top,  prop: ,  so_apply: x[s],  all: x:A. B[x],  exists: x:A. B[x],  or: P  Q,  and: P  Q,  set: {x:A| B[x]} ,  function: x:A  B[x],  union: left + right,  equal: s = t,  p-inject: p-inject(A;B;f),  do-apply: do-apply(f;x),  can-apply: can-apply(f;x)
Definitions :  strong-subtype: strong-subtype(A;B),  le: A  B,  ge: i  j ,  not: A,  less_than: a < b,  uiff: uiff(P;Q),  subtype_rel: A r B,  axiom: Ax,  final-iterate: final-iterate(f;x),  same-thread: same-thread(es;p;e;e'),  ifthenelse: if b then t else f fi ,  bool: ,  do-apply: do-apply(f;x),  void: Void,  can-apply: can-apply(f;x),  cand: A c B,  limited-type: LimitedType,  pair: <a, b>,  and: P  Q,  or: P  Q,  product: x:A  B[x],  exists: x:A. B[x],  subtype: S  T,  suptype: suptype(S; T),  so_apply: x[s],  set: {x:A| B[x]} ,  p-inject: p-inject(A;B;f),  apply: f a,  es-causl: (e < e'),  implies: P  Q,  assert: b,  universe: Type,  prop: ,  causal-predecessor: causal-predecessor(es;p),  uimplies: b supposing a,  isect: x:A. B[x],  dep-isect: Error :dep-isect,  eq_atom: x =a y,  eq_atom: eq_atom$n(x;y),  all: x:A. B[x],  uall: [x:A]. B[x],  function: x:A  B[x],  union: left + right,  top: Top,  es-E: E,  record+: record+,  member: t  T,  equal: s = t,  event_ordering: EO,  record-select: r.x,  infix_ap: x f y,  tactic: Error :tactic,  record: record(x.T[x]),  l_member: (x  l),  lambda: x.A[x],  so_lambda: x.t[x],  guard: {T},  wellfounded: WellFnd{i}(A;x,y.R[x; y]),  sq_type: SQType(T),  decide: case b of inl(x) => s[x] | inr(y) => t[y]
Lemmas :  same-thread_transitivity,  same-thread_inversion,  same-thread-do-apply,  same-thread_weakening,  subtype_base_sq,  es-causl-wellfnd,  es-causl_wf,  uiff_inversion,  top_wf,  es-E_wf,  member_wf,  can-apply_wf,  assert_wf,  p-inject_wf,  causal-predecessor_wf,  event_ordering_wf,  do-apply_wf,  same-thread_wf

---

\mforall{}[es:EO].  \mforall{}[p:E  {}\mrightarrow{}  (E  +  Top)].
    \mforall{}[A:E  {}\mrightarrow{}  \mBbbP{}]
        (\mforall{}[e,e':E].    (same-thread(es;p;e;e'))  supposing  (A[e']  and  A[e]))  supposing 
              ((\mexists{}x:\{e:E|  A[e]\}  .  \mforall{}y:\{e:E|  A[e]\}  .  ((y  =  x)  \mvee{}  ((\muparrow{}can-apply(p;y))  \mwedge{}  A[do-apply(p;y)])))  and 
              p-inject(\{e:E|  A[e]\}  ;E;p)) 
    supposing  causal-predecessor(es;p)


Date html generated: 2011_08_16-AM-11_19_22
Last ObjectModification: 2011_06_20-AM-00_24_38

Home Index