Nuprl Lemma : es-local-pred-property

[Info:Type]
  ∀es:EO+(Info). ∀e:E. ∀P:{e':E| (e' <loc e)}  ─→ 𝔹.
    ((↑can-apply(last(P);e) ⇐⇒ ∃a:E. ((a <loc e) ∧ (↑(P a))))
    ∧ (do-apply(last(P);e) <loc e)
      ∧ (↑(P do-apply(last(P);e)))
      ∧ (∀e'':E. ((e'' <loc e)  (do-apply(last(P);e) <loc e'')  (¬↑(P 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-E: E assert: b bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] iff: ⇐⇒ Q not: ¬A implies:  Q and: P ∧ Q set: {x:A| B[x]}  apply: a function: x:A ─→ B[x] universe: Type do-apply: do-apply(f;x) can-apply: can-apply(f;x)
Lemmas :  es-local-pred-property2

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}e:E.  \mforall{}P:\{e':E|  (e'  <loc  e)\}    {}\mrightarrow{}  \mBbbB{}.
        ((\muparrow{}can-apply(last(P);e)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:E.  ((a  <loc  e)  \mwedge{}  (\muparrow{}(P  a))))
        \mwedge{}  (do-apply(last(P);e)  <loc  e)
            \mwedge{}  (\muparrow{}(P  do-apply(last(P);e)))
            \mwedge{}  (\mforall{}e'':E.  ((e''  <loc  e)  {}\mRightarrow{}  (do-apply(last(P);e)  <loc  e'')  {}\mRightarrow{}  (\mneg{}\muparrow{}(P  e'')))) 
            supposing  \muparrow{}can-apply(last(P);e))



Date html generated: 2015_07_20-PM-04_06_53
Last ObjectModification: 2015_01_27-PM-09_49_11

Home Index