---

{ es:EO
    [R:{R:E  E  | e,e':E.  (R[e;e']  (e' < e))} ]
      d:e,e':E.  Dec(R e e')
        (causal-predecessor(es;es-r-pred{i:l}(es;d))
         (e:E
             ((can-apply(es-r-pred{i:l}(es;d);e)  e':E. R[e;e'])
              R[e;do-apply(es-r-pred{i:l}(es;d);e)] 
               supposing can-apply(es-r-pred{i:l}(es;d);e)))) }

{ Proof }

---

Definitions occuring in Statement :  es-r-pred: es-r-pred{i:l}(es;d),  causal-predecessor: causal-predecessor(es;p),  es-causl: (e < e'),  es-E: E,  event_ordering: EO,  assert: b,  decidable: Dec(P),  uimplies: b supposing a,  uall: [x:A]. B[x],  prop: ,  so_apply: x[s1;s2],  all: x:A. B[x],  exists: x:A. B[x],  iff: P  Q,  implies: P  Q,  and: P  Q,  set: {x:A| B[x]} ,  apply: f a,  function: x:A  B[x],  do-apply: do-apply(f;x),  can-apply: can-apply(f;x)
Definitions :  fpf: a:A fp-> B[a],  strong-subtype: strong-subtype(A;B),  list: type List,  eq_atom: x =a y,  eq_atom: eq_atom$n(x;y),  record-select: r.x,  dep-isect: Error :dep-isect,  record+: record+,  le: A  B,  ge: i  j ,  not: A,  less_than: a < b,  uiff: uiff(P;Q),  subtype_rel: A r B,  void: Void,  subtype: S  T,  suptype: suptype(S; T),  lambda: x.A[x],  do-apply: do-apply(f;x),  rev_implies: P  Q,  can-apply: can-apply(f;x),  limited-type: LimitedType,  top: Top,  iff: P  Q,  assert: b,  uimplies: b supposing a,  exists: x:A. B[x],  so_lambda: x.t[x],  causal-pred-from-relation,  es-r-pred: es-r-pred{i:l}(es;d),  equal: s = t,  member: t  T,  union: left + right,  or: P  Q,  event_ordering: EO,  uall: [x:A]. B[x],  isect: x:A. B[x],  so_apply: x[s1;s2],  universe: Type,  es-causl: (e < e'),  infix_ap: x f y,  set: {x:A| B[x]} ,  decidable: Dec(P),  apply: f a,  es-E: E,  prop: ,  and: P  Q,  product: x:A  B[x],  causal-predecessor: causal-predecessor(es;p),  all: x:A. B[x],  function: x:A  B[x],  implies: P  Q,  CollapseTHEN: Error :CollapseTHEN,  D: Error :D,  Auto: Error :Auto,  CollapseTHENA: Error :CollapseTHENA,  Unfold: Error :Unfold,  tactic: Error :tactic
Lemmas :  es-E_wf,  top_wf,  causal-predecessor_wf,  iff_wf,  assert_wf,  event_ordering_wf,  uall_wf,  es-causl_wf,  decidable_wf,  causal-pred-from-relation,  can-apply_wf,  member_wf,  do-apply_wf,  subtype_rel_wf

---

\mforall{}es:EO
    \mforall{}[R:\{R:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}|  \mforall{}e,e':E.    (R[e;e']  {}\mRightarrow{}  (e'  <  e))\}  ]
        \mforall{}d:\mforall{}e,e':E.    Dec(R  e  e')
            (causal-predecessor(es;es-r-pred\{i:l\}(es;d))
            \mwedge{}  (\mforall{}e:E
                      ((\muparrow{}can-apply(es-r-pred\{i:l\}(es;d);e)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}e':E.  R[e;e'])
                      \mwedge{}  R[e;do-apply(es-r-pred\{i:l\}(es;d);e)]  supposing  \muparrow{}can-apply(es-r-pred\{i:l\}(es;d);e))))


Date html generated: 2011_08_16-AM-11_13_24
Last ObjectModification: 2011_06_20-AM-00_20_48

Home Index