Nuprl Lemma : eo-forward-not-first2
[Info:Type]. eo:EO+(Info). e:E. e':{e':E| e' 
loc e } . uiff(
first(e);(e' <loc e))
Proof not projected
Definitions occuring in Statement :
eo-forward: eo.e,
event-ordering+: EO+(Info),
es-le: e loc e' ,
es-locl: (e <loc e'),
es-first: first(e),
es-E: E,
assert: b,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
all: x:A. B[x],
not: A,
set: {x:A| B[x]} ,
universe: Type
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
uiff: uiff(P;Q),
not: A,
member: t 
T,
prop: 
,
uimplies: b supposing a,
implies: P 
Q,
squash: 
T,
true: True,
and: P 
Q,
false: False,
rev_implies: P 
Q,
iff: P Q,
guard: {T},
es-le: e loc e' ,
sq_stable: SqStable(P),
or: P 
Q,
subtype: S 
T
Lemmas :
es-E_wf,
event-ordering+_inc,
es-le_wf,
event-ordering+_wf,
not_wf,
assert_wf,
es-first_wf,
eo-forward_wf,
member-eo-forward-E,
sq_stable_from_decidable,
decidable__es-le,
equal_wf,
Id_wf,
es-loc_wf,
es-locl_wf,
decidable__es-locl,
es-locl_transitivity2,
es-le_weakening_eq,
es-locl_irreflexivity,
uiff_functionality_wrt_uiff2,
iff_weakening_uiff,
not_functionality_wrt_uiff,
eo-forward-first2
\mforall{}[Info:Type]. \mforall{}eo:EO+(Info). \mforall{}e:E. \mforall{}e':\{e':E| e' \mleq{}loc e \} . uiff(\mneg{}\muparrow{}first(e);(e' <loc e))
Date html generated:
2012_01_23-PM-12_15_55
Last ObjectModification:
2012_01_10-PM-03_54_42
Home
Index