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
Lemmas :
es-first_wf,
bool_wf,
eqtt_to_assert,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
es-E_wf,
event_ordering_wf,
assert-es-first,
es-causl_wf,
Id_wf,
es-loc_wf,
es-pred_property
\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:
2015_07_17-AM-08_35_53
Last ObjectModification:
2015_01_27-PM-02_58_37
Home
Index