Nuprl Lemma : es-pred?_property
∀es:EO. ∀e:E.
case es-pred?(es;e)
of inl(p) =>
(loc(p) = loc(e) ∈ Id) ∧ (p < e) ∧ (∀e':E. (e' < e) ⇒ ((e' = p ∈ E) ∨ (e' < p)) supposing loc(e') = loc(e) ∈ Id)
| inr(z) =>
∀e':E. ¬(e' < e) supposing loc(e') = loc(e) ∈ Id
Proof
Definitions occuring in Statement :
es-pred?: es-pred?(es;e),
es-causl: (e < e'),
es-loc: loc(e),
es-E: E,
event_ordering: EO,
Id: Id,
uimplies: b supposing a,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
es-pred?: es-pred?(es;e),
member: t ∈ T,
uall: ∀[x:A]. B[x],
es-E: E,
es-base-E: es-base-E(es),
implies: P ⇒ Q,
exposed-bfalse: exposed-bfalse,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
ifthenelse: if b then t else f fi ,
bfalse: ff,
exists: ∃x:A. B[x],
prop: ℙ,
or: P ∨ Q,
sq_type: SQType(T),
guard: {T},
bnot: ¬bb,
assert: ↑b,
false: False,
not: ¬A
Latex:
\mforall{}es:EO. \mforall{}e:E.
case es-pred?(es;e)
of inl(p) =>
(loc(p) = loc(e))
\mwedge{} (p < e)
\mwedge{} (\mforall{}e':E. (e' < e) {}\mRightarrow{} ((e' = p) \mvee{} (e' < p)) supposing loc(e') = loc(e))
| inr(z) =>
\mforall{}e':E. \mneg{}(e' < e) supposing loc(e') = loc(e)
Date html generated:
2016_05_16-AM-09_17_17
Last ObjectModification:
2015_12_28-PM-09_56_49
Theory : new!event-ordering
Home
Index