Nuprl Lemma : es-local-pred-cases

[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) ∈ E))
      ∨ ((¬↑(P pred(e))) ∧ (↑can-apply(last(P);pred(e))) ∧ (do-apply(last(P);e) do-apply(last(P);pred(e)) ∈ 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-first: first(e) es-pred: pred(e) es-E: E assert: b bool: 𝔹 uimplies: 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: a function: x:A ─→ B[x] universe: Type equal: t ∈ T do-apply: do-apply(f;x) can-apply: can-apply(f;x)
Lemmas :  es-local-pred-cases-sq assert_witness es-pred_wf event-ordering+_subtype not_wf assert_wf es-pred-locl es-locl_wf can-apply_wf es-E_wf es-local-pred_wf do-apply_wf set_wf bool_wf event-ordering+_wf es-local-pred_wf2 or_wf sq_exists_wf all_wf btrue_wf bfalse_wf equal_wf subtype_rel_dep_function subtype_rel_sets es-locl_transitivity2 es-le_weakening subtype_rel_self true_wf false_wf isl_wf

Latex:
\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)  =  pred(e)))
            \mvee{}  ((\mneg{}\muparrow{}(P  pred(e)))
                \mwedge{}  (\muparrow{}can-apply(last(P);pred(e)))
                \mwedge{}  (do-apply(last(P);e)  =  do-apply(last(P);pred(e))))) 
        supposing  \muparrow{}can-apply(last(P);e)



Date html generated: 2015_07_20-PM-04_06_37
Last ObjectModification: 2015_01_27-PM-09_51_46

Home Index