Nuprl Lemma : p-compose-causal-predecessor1
∀es:EO. ∀p,w:E ─→ (E + Top).
(causal-predecessor(es;p) ⇒ causal-weak-predecessor(es;w) ⇒ causal-predecessor(es;p o w))
Proof
Definitions occuring in Statement :
causal-weak-predecessor: causal-weak-predecessor(es;p),
causal-predecessor: causal-predecessor(es;p),
es-E: E,
event_ordering: EO,
top: Top,
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ─→ B[x],
union: left + right,
p-compose: f o g
Lemmas :
assert_wf,
can-apply_wf,
es-E_wf,
p-compose_wf,
top_wf,
subtype_rel_dep_function,
subtype_rel_sum,
all_wf,
es-causle_wf,
do-apply_wf,
es-causl_wf,
event_ordering_wf,
isl_wf,
false_wf,
es-causl_transitivity2,
bfalse_wf,
and_wf,
equal_wf,
assert_elim,
btrue_neq_bfalse,
true_wf
\mforall{}es:EO. \mforall{}p,w:E {}\mrightarrow{} (E + Top).
(causal-predecessor(es;p) {}\mRightarrow{} causal-weak-predecessor(es;w) {}\mRightarrow{} causal-predecessor(es;p o w))
Date html generated:
2015_07_17-AM-09_07_06
Last ObjectModification:
2015_01_27-PM-00_48_48
Home
Index