---

{ [Info:Type]
    es:EO+(Info). e:E. P:{e':E| (e' <loc e)}   .
      (first(e))
       ((((P pred(e)))  (do-apply(last(P);e) ~ pred(e)))
         (((P pred(e)))
           (can-apply(last(P);pred(e)))
           (do-apply(last(P);e) ~ do-apply(last(P);pred(e))))) 
      supposing can-apply(last(P);e) }

{ Proof }

---

Definitions occuring in Statement :  es-local-pred: last(P),  event-ordering+: EO+(Info),  es-locl: (e <loc e'),  es-pred: pred(e),  es-first: first(e),  es-E: E,  assert: b,  bool: ,  uimplies: b supposing a,  uall: [x:A]. B[x],  all: x:A. B[x],  not: A,  or: P  Q,  and: P  Q,  set: {x:A| B[x]} ,  apply: f a,  function: x:A  B[x],  universe: Type,  sqequal: s ~ t,  do-apply: do-apply(f;x),  can-apply: can-apply(f;x)
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  uimplies: b supposing a,  assert: b,  can-apply: can-apply(f;x),  es-local-pred: last(P),  and: P  Q,  not: A,  do-apply: do-apply(f;x),  isl: isl(x),  outl: outl(x),  ifthenelse: if b then t else f fi ,  ycomb: Y,  member: t  T,  implies: P  Q,  btrue: tt,  prop: ,  false: False,  bfalse: ff,  true: True,  or: P  Q,  cand: A c B,  sq_exists: x:{A| B[x]},  subtype: S  T,  suptype: suptype(S; T),  sq_type: SQType(T),  top: Top,  so_lambda: x.t[x],  guard: {T},  bool: ,  unit: Unit,  iff: P  Q,  so_apply: x[s],  it:
Lemmas :  es-first_wf,  bool_wf,  iff_weakening_uiff,  assert_wf,  eqtt_to_assert,  false_wf,  not_wf,  uiff_transitivity,  bnot_wf,  eqff_to_assert,  assert_of_bnot,  es-locl_wf,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf,  es-pred_wf,  es-pred-locl,  true_wf,  isl_wf,  es-local-pred_wf,  es-local-pred_wf2,  subtype_rel_function,  subtype_rel_sets,  subtype_rel_self,  es-locl_transitivity2,  es-le_weakening,  subtype_rel_sum,  top_wf

---

\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}e:E.  \mforall{}P:\{e':E|  (e'  <loc  e)\}    {}\mrightarrow{}  \mBbbB{}.
        (\mneg{}\muparrow{}first(e))
        \mwedge{}  (((\muparrow{}(P  pred(e)))  \mwedge{}  (do-apply(last(P);e)  \msim{}  pred(e)))
            \mvee{}  ((\mneg{}\muparrow{}(P  pred(e)))
                \mwedge{}  (\muparrow{}can-apply(last(P);pred(e)))
                \mwedge{}  (do-apply(last(P);e)  \msim{}  do-apply(last(P);pred(e))))) 
        supposing  \muparrow{}can-apply(last(P);e)


Date html generated: 2011_08_16-PM-04_42_31
Last ObjectModification: 2011_06_20-AM-01_02_30

Home Index