Nuprl Lemma : tl-es-le-before
es:EO. e,e':E. ((e' 
tl(
loc(e))) 
e' loc e 
(
first(e')))
Proof not projected
Definitions occuring in Statement :
es-le-before: loc(e),
es-le: e loc e' ,
es-first: first(e),
es-E: E,
event_ordering: EO,
tl: tl(l),
assert: b,
all: x:A. B[x],
iff: P Q,
not: A,
and: P Q,
l_member: (x l)
Definitions :
all: x:A. B[x],
tl: tl(l),
es-le-before: loc(e),
not: A,
member: t T,
nat: 
,
implies: P Q,
ge: i 
j ,
le: A B,
false: False,
squash: 
T,
true: True,
append: as @ bs,
es-before: before(e),
ycomb: Y,
ifthenelse: if b then t else f fi ,
btrue: tt,
bfalse: ff,
prop: 
,
guard: {T},
iff: P Q,
and: P Q,
subtype: S 
T,
cand: A c B,
rev_implies: P Q,
or: P 
Q,
es-le: e loc e' ,
strongwellfounded: SWellFounded(R[x; y]),
exists: 
x:A. B[x],
uall: [x:A]. B[x],
bool: 
,
unit: Unit,
uimplies: b supposing a,
uiff: uiff(P;Q),
decidable: Dec(P),
it: 
Lemmas :
es-causl-swellfnd,
nat_properties,
ge_wf,
less_than_wf,
nat_wf,
le_wf,
es-causl_wf,
es-first_wf,
bool_wf,
eqtt_to_assert,
uiff_transitivity,
equal_wf,
assert_wf,
bnot_wf,
not_wf,
eqff_to_assert,
assert_of_bnot,
es-E_wf,
event_ordering_wf,
es-pred_wf,
es-pred-causl,
es-le-before_wf,
Id_wf,
es-loc_wf,
member_singleton,
or_functionality_wrt_iff,
member_append,
iff_transitivity,
iff_functionality_wrt_iff,
implies_functionality_wrt_iff,
iff_wf,
l_member_wf,
es-le_wf,
append_wf,
or_wf,
and_wf,
decidable__cand,
decidable__es-le,
decidable__not,
decidable__assert,
es-pred-locl,
es-locl_transitivity1,
es-le_weakening,
es-locl_wf,
es-le-pred
\mforall{}es:EO. \mforall{}e,e':E. ((e' \mmember{} tl(\mleq{}loc(e))) \mLeftarrow{}{}\mRightarrow{} e' \mleq{}loc e \mwedge{} (\mneg{}\muparrow{}first(e')))
Date html generated:
2012_01_23-PM-12_11_06
Last ObjectModification:
2011_12_13-AM-10_31_34
Home
Index