Nuprl Lemma : alle-between1-trivial
∀es:EO. ∀e:E. ∀P:Top. ∀e∈[e,e).P[e]
Proof
Definitions occuring in Statement :
alle-between1: ∀e∈[e1,e2).P[e],
es-E: E,
event_ordering: EO,
top: Top,
so_apply: x[s],
all: ∀x:A. B[x]
Lemmas :
es-locl-antireflexive,
es-locl_wf,
es-le_wf,
top_wf,
es-E_wf,
event_ordering_wf,
es-le-trans2
\mforall{}es:EO. \mforall{}e:E. \mforall{}P:Top. \mforall{}e\mmember{}[e,e).P[e]
Date html generated:
2015_07_17-AM-08_46_52
Last ObjectModification:
2015_01_27-PM-02_26_04
Home
Index