Nuprl Lemma : thread-p-ordered
∀es:EO. ∀p:E ─→ (E + Top).
((causal-predecessor(es;p) ∧ p-inject(E;E;p))
⇒ (∀e,e':E. (e p< e' ∨ (e = e' ∈ E)) ∨ e' p< e supposing same-thread(es;p;e;e')))
Proof
Definitions occuring in Statement :
same-thread: same-thread(es;p;e;e'),
es-p-locl: e p< e',
causal-predecessor: causal-predecessor(es;p),
es-E: E,
event_ordering: EO,
uimplies: b supposing a,
top: Top,
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
function: x:A ─→ B[x],
union: left + right,
equal: s = t ∈ T,
p-inject: p-inject(A;B;f)
Lemmas :
same-thread_wf,
es-E_wf,
causal-predecessor_wf,
p-inject_wf,
top_wf,
event_ordering_wf,
same-final-iterate-one-one,
causal-pred-wellfounded,
decidable__equal_int,
subtype_base_sq,
int_subtype_base,
primrec0_lemma,
es-p-locl_wf,
equal_wf,
decidable__lt,
false_wf,
not-equal-2,
add_functionality_wrt_le,
add-associates,
add-zero,
zero-add,
le-add-cancel,
condition-implies-le,
add-commutes,
minus-add,
minus-zero,
less_than_wf,
p-graph_wf2,
p-fun-exp_wf,
nat_plus_subtype_nat,
es-causle_weakening_p-le,
or_wf
\mforall{}es:EO. \mforall{}p:E {}\mrightarrow{} (E + Top).
((causal-predecessor(es;p) \mwedge{} p-inject(E;E;p))
{}\mRightarrow{} (\mforall{}e,e':E. (e p< e' \mvee{} (e = e')) \mvee{} e' p< e supposing same-thread(es;p;e;e')))
Date html generated:
2015_07_17-AM-09_09_07
Last ObjectModification:
2015_01_27-PM-00_46_54
Home
Index