Nuprl Lemma : eo-forward-first2
[Info:Type]. [eo:EO+(Info)]. [e:E]. [e':{e':E| e' 
loc e } ]. {uiff(
first(e);e = e')}
Proof not projected
Definitions occuring in Statement :
eo-forward: eo.e,
event-ordering+: EO+(Info),
es-le: e loc e' ,
es-first: first(e),
es-E: E,
assert: b,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
guard: {T},
set: {x:A| B[x]} ,
universe: Type,
equal: s = t
Definitions :
prop: 
,
uimplies: b supposing a,
and: P 
Q,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
true: True,
squash: 
T,
implies: P 
Q,
member: t 
T,
guard: {T},
top: Top,
bfalse: ff,
btrue: tt,
all: x:A. B[x],
ifthenelse: if b then t else f fi ,
sq_stable: SqStable(P),
sq_type: SQType(T),
or: P 
Q,
false: False,
not: 
A,
unit: Unit,
bool: 
,
rev_uimplies: rev_uimplies(P;Q),
subtype: S 
T,
it: 
Lemmas :
es-E_wf,
assert_witness,
event-ordering+_wf,
eo-forward_wf,
es-first_wf,
assert_wf,
es-loc_wf,
Id_wf,
equal_wf,
decidable__es-le,
event-ordering+_inc,
es-le_wf,
sq_stable_from_decidable,
member-eo-forward-E,
eo-forward-first,
not_functionality_wrt_uiff,
assert_of_bnot,
eqff_to_assert,
assert-eq-id,
eqtt_to_assert,
uiff_transitivity,
bool_subtype_base,
subtype_base_sq,
bool_cases,
not_wf,
bnot_wf,
bool_wf,
eq_id_wf,
es-eq_wf,
assert-deq,
es-le-loc,
eo-forward-loc,
sq_stable__assert
\mforall{}[Info:Type]. \mforall{}[eo:EO+(Info)]. \mforall{}[e:E]. \mforall{}[e':\{e':E| e' \mleq{}loc e \} ]. \{uiff(\muparrow{}first(e);e = e')\}
Date html generated:
2012_02_20-PM-02_44_09
Last ObjectModification:
2012_01_11-AM-07_09_59
Home
Index