Nuprl Lemma : decidable__es-locl
∀the_es:EO. ∀e',e:E. Dec((e <loc e'))
Proof
Definitions occuring in Statement :
es-locl: (e <loc e'),
es-E: E,
event_ordering: EO,
decidable: Dec(P),
all: ∀x:A. B[x]
Lemmas :
decidable_functionality,
es-locl_wf,
assert_wf,
es-bless_wf,
assert-es-bless,
decidable__assert,
es-E_wf,
event_ordering_wf
\mforall{}the$_{es}$:EO. \mforall{}e',e:E. Dec((e <loc e'))
Date html generated:
2015_07_17-AM-08_39_43
Last ObjectModification:
2015_01_27-PM-02_41_08
Home
Index