Nuprl Lemma : eo-forward-locl
[Info:Type]. [eo:EO+(Info)]. [e,a,b:Top]. ((a <loc b) ~ (a <loc b))
Proof not projected
Definitions occuring in Statement :
eo-forward: eo.e,
event-ordering+: EO+(Info),
es-locl: (e <loc e'),
uall: [x:A]. B[x],
top: Top,
universe: Type,
sqequal: s ~ t
Definitions :
es-locl: (e <loc e'),
member: t 
T,
uall: [x:A]. B[x],
all: x:A. B[x]
Lemmas :
eo-forward-less,
top_wf,
event-ordering+_wf,
eo-forward-loc
\mforall{}[Info:Type]. \mforall{}[eo:EO+(Info)]. \mforall{}[e,a,b:Top]. ((a <loc b) \msim{} (a <loc b))
Date html generated:
2011_10_20-PM-03_17_46
Last ObjectModification:
2011_08_24-PM-08_57_19
Home
Index