Nuprl Lemma : es-direct-prior-exists
es:EO. e,e':E. ((e' < e) 
(
e'':E. (e'' 
es-direct-prior(es;e) 
e' 
loc e'' )))
Proof not projected
Definitions occuring in Statement :
es-direct-prior: es-direct-prior(es;e),
es-le: e loc e' ,
es-causl: (e < e'),
es-E: E,
event_ordering: EO,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
and: P Q,
bag-member: x bs
Definitions :
cand: A c B,
prop: 
,
so_lambda: 
x y.t[x; y],
member: t T,
and: P Q,
exists: x:A. B[x],
implies: P Q,
all: x:A. B[x],
bfalse: ff,
btrue: tt,
ifthenelse: if b then t else f fi ,
so_apply: x[s1;s2],
so_apply: x[s],
top: Top,
not: 
A,
subtype: S 
T,
iseg: l1 l2,
rev_implies: P 
Q,
iff: P Q,
trans: Trans(T;x,y.E[x; y]),
guard: {T},
or: P 
Q,
refl: Refl(T;x,y.E[x; y]),
es-le: e loc e' ,
uall: [x:A]. B[x],
uiff: uiff(P;Q),
uimplies: b supposing a,
unit: Unit,
bool: 
,
ycomb: Y,
rev_uimplies: rev_uimplies(P;Q),
list_accum: list_accum(x,a.f[x; a];y;l),
sq_type: SQType(T),
false: False,
it: 
Lemmas :
event_ordering_wf,
es-causl_wf,
es-le_wf,
es-direct-prior_wf,
bag-member_wf,
es-blocl_wf,
ifthenelse_wf,
es-pred-list_wf,
es-E_wf,
list_accum_wf,
es-loc_wf,
Id_wf,
equal_wf,
es-direct-prior-member-iff,
assert_of_bnot,
eqff_to_assert,
uiff_transitivity,
eqtt_to_assert,
list_accum_invariant2,
bnot_wf,
bool_wf,
member-es-pred-list,
l_member_wf,
not_wf,
assert_wf,
ifthenelse-wf,
append_wf,
top_wf,
list_accum_append,
member_wf,
es-locl_wf,
nat_wf,
length_wf_nat,
l_member_decomp,
decidable__es-E-equal,
bag-member-list,
es-blocl-iff,
bag_qinc,
bag-maximal?-iff,
list_accum_iseg_inv,
assert_elim,
bool_subtype_base,
subtype_base_sq,
es-locl_transitivity1,
iseg_wf,
es-le_transitivity,
es-locl_irreflexivity,
es-locl_transitivity2,
and_wf,
es-locl-trichotomy,
not_functionality_wrt_iff,
list_accum_invariant
\mforall{}es:EO. \mforall{}e,e':E. ((e' < e) {}\mRightarrow{} (\mexists{}e'':E. (e'' \mdownarrow{}\mmember{} es-direct-prior(es;e) \mwedge{} e' \mleq{}loc e'' )))
Date html generated:
2012_01_23-PM-12_09_04
Last ObjectModification:
2011_12_14-PM-09_43_17
Home
Index