Nuprl Lemma : eo-forward-alle-lt

Info:Type. ∀es:EO+(Info). ∀b:E. ∀e:{e:E| b ≤loc .
  ∀[P:{e':E| b ≤loc e'  ∧ (e' <loc e)}  ⟶ ℙ]. (∀e'<e.P[e'] ⇐⇒ ∀e':E. (b ≤loc e'   (e' <loc e)  P[e']))


Proof




Definitions occuring in Statement :  eo-forward: eo.e event-ordering+: EO+(Info) alle-lt: e<e'.P[e] es-le: e ≤loc e'  es-locl: (e <loc e') es-E: E uall: [x:A]. B[x] prop: so_apply: x[s] all: x:A. B[x] iff: ⇐⇒ Q implies:  Q and: P ∧ Q set: {x:A| B[x]}  function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  alle-lt: e<e'.P[e] all: x:A. B[x] uall: [x:A]. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T uimplies: supposing a prop: subtype_rel: A ⊆B top: Top so_lambda: λ2x.t[x] decidable: Dec(P) or: P ∨ Q false: False not: ¬A so_apply: x[s] cand: c∧ B es-locl: (e <loc e') rev_implies:  Q

Latex:
\mforall{}Info:Type.  \mforall{}es:EO+(Info).  \mforall{}b:E.  \mforall{}e:\{e:E|  b  \mleq{}loc  e  \}  .
    \mforall{}[P:\{e':E|  b  \mleq{}loc  e'    \mwedge{}  (e'  <loc  e)\}    {}\mrightarrow{}  \mBbbP{}]
        (\mforall{}e'<e.P[e']  \mLeftarrow{}{}\mRightarrow{}  \mforall{}e':E.  (b  \mleq{}loc  e'    {}\mRightarrow{}  (e'  <loc  e)  {}\mRightarrow{}  P[e']))



Date html generated: 2016_05_16-PM-01_11_44
Last ObjectModification: 2015_12_29-PM-01_53_32

Theory : event-ordering


Home Index