Nuprl Lemma : causal-order-preserving_wf

[es:EO]. ∀[P:E ─→ ℙ]. ∀[f:{e:E| P[e]}  ─→ E].  (e.f[e] is c< preserving on e.P[e] ∈ ℙ)


Proof




Definitions occuring in Statement :  causal-order-preserving: a.f[a] is c< preserving on e.P[e] es-E: E event_ordering: EO uall: [x:A]. B[x] prop: so_apply: x[s] member: t ∈ T set: {x:A| B[x]}  function: x:A ─→ B[x]
Lemmas :  all_wf es-E_wf es-causl_wf event_ordering_wf
\mforall{}[es:EO].  \mforall{}[P:E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[f:\{e:E|  P[e]\}    {}\mrightarrow{}  E].    (e.f[e]  is  c<  preserving  on  e.P[e]  \mmember{}  \mBbbP{})



Date html generated: 2015_07_17-AM-09_06_09
Last ObjectModification: 2015_01_27-PM-00_48_19

Home Index