Nuprl Lemma : es-closed-open-interval-nil
∀es:EO. ∀e:E. ([e;e) = [] ∈ (E List))
Proof
Definitions occuring in Statement :
es-closed-open-interval: [e;e'),
es-E: E,
event_ordering: EO,
nil: [],
list: T List,
all: ∀x:A. B[x],
equal: s = t ∈ T
Lemmas :
assert_of_null,
es-closed-open-interval_wf,
null_filter,
es-ble_wf,
es-before_wf,
l_all_iff,
l_member_wf,
not_wf,
assert_wf,
member-es-before,
es-le_wf,
assert-es-ble,
all_wf,
es-E_wf,
event_ordering_wf,
es-locl_irreflexivity,
es-locl_transitivity2
\mforall{}es:EO. \mforall{}e:E. ([e;e) = [])
Date html generated:
2015_07_17-AM-08_41_37
Last ObjectModification:
2015_01_27-PM-02_39_04
Home
Index