Nuprl Lemma : causal-weak-predecessor_wf

[es:EO]. ∀[p:E ─→ (E Top)].  (causal-weak-predecessor(es;p) ∈ ℙ)


Proof




Definitions occuring in Statement :  causal-weak-predecessor: causal-weak-predecessor(es;p) es-E: E event_ordering: EO uall: [x:A]. B[x] top: Top prop: member: t ∈ T function: x:A ─→ B[x] union: left right
Lemmas :  all_wf assert_wf can-apply_wf subtype_rel_dep_function top_wf subtype_rel_sum es-causle_wf do-apply_wf es-E_wf event_ordering_wf
\mforall{}[es:EO].  \mforall{}[p:E  {}\mrightarrow{}  (E  +  Top)].    (causal-weak-predecessor(es;p)  \mmember{}  \mBbbP{})



Date html generated: 2015_07_17-AM-09_07_00
Last ObjectModification: 2015_01_27-PM-00_47_51

Home Index