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)
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
uimplies: b supposing a,
member: t ∈ T,
same-thread: same-thread(es;p;e;e'),
and: P ∧ Q,
prop: ℙ,
uall: ∀[x:A]. B[x],
exists: ∃x:A. B[x],
or: P ∨ Q,
nat: ℕ,
decidable: Dec(P),
sq_type: SQType(T),
guard: {T},
p-fun-exp: f^n,
p-graph: p-graph(A;f),
top: Top,
p-id: p-id(),
do-apply: do-apply(f;x),
can-apply: can-apply(f;x),
isl: isl(x),
outl: outl(x),
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
es-p-le: e p≤ e',
cand: A c∧ B,
es-p-locl: e p< e',
nat_plus: ℕ+,
le: A ≤ B,
iff: P ⇐⇒ Q,
not: ¬A,
rev_implies: P ⇐ Q,
false: False,
uiff: uiff(P;Q),
subtype_rel: A ⊆r B,
less_than': less_than'(a;b),
true: True,
subtract: n - m,
es-causle: e c≤ e'
Latex:
\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:
2016_05_16-AM-10_33_34
Last ObjectModification:
2015_12_28-PM-09_20_04
Theory : new!event-ordering
Home
Index