Nuprl Lemma : es-local-pred_wf2
[Info:Type]. [es:EO+(Info)]. [e:E]. [P:{e':E| (e' <loc e)} 
].
(last(P) e 
(
e':{E| ((e' <loc e) 
(
(P e')) (e'':E. ((e' <loc e'') 
(e'' <loc e) (
(P e'')))))})
((e':{E| ((e' <loc e) ((P e')))})))
Proof not projected
Definitions occuring in Statement :
es-local-pred: last(P),
event-ordering+: EO+(Info),
es-locl: (e <loc e'),
es-E: E,
assert: b,
bool: ,
uall: [x:A]. B[x],
all: x:A. B[x],
sq_exists: x:{A| B[x]},
not: A,
implies: P Q,
or: P Q,
and: P Q,
member: t T,
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x],
universe: Type
Definitions :
member: t T,
uall: [x:A]. B[x],
true: True,
squash: 
T,
false: False,
le: A 
B,
ge: i 
j ,
nat: 
,
not: A,
implies: P Q,
or: P Q,
all: x:A. B[x],
bfalse: ff,
cand: A c B,
so_lambda: 
x.t[x],
prop: 
,
btrue: tt,
ifthenelse: if b then t else f fi ,
ycomb: Y,
es-local-pred: last(P),
and: P Q,
sq_exists: x:{A| B[x]},
exists: x:A. B[x],
strongwellfounded: SWellFounded(R[x; y]),
uiff: uiff(P;Q),
unit: Unit,
uimplies: b supposing a,
so_apply: x[s],
bool: ,
iff: P 
Q,
subtype: S 
T,
it: 
,
guard: {T}
Lemmas :
event-ordering+_wf,
event-ordering+_inc,
es-E_wf,
bool_wf,
es-locl_wf,
equal_wf,
es-causl_wf,
le_wf,
nat_wf,
less_than_wf,
ge_wf,
nat_properties,
es-causl-swellfnd,
assert_of_bnot,
eqff_to_assert,
uiff_transitivity,
inl_wf,
eqtt_to_assert,
es-pred-locl,
es-pred_wf,
bnot_wf,
not_wf,
all_wf,
assert_wf,
sq_exists_wf,
inr_wf,
es-first_wf,
es-le_weakening,
es-locl_transitivity2,
subtype_rel_self,
subtype_rel_sets,
subtype_rel_dep_function,
es-pred-causl,
not_subtype_rel,
subtype_rel_sum,
es-locl-iff,
true_wf,
squash_wf
\mforall{}[Info:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[e:E]. \mforall{}[P:\{e':E| (e' <loc e)\} {}\mrightarrow{} \mBbbB{}].
(last(P) e \mmember{} (\mexists{}e':\{E| ((e' <loc e)
\mwedge{} (\muparrow{}(P e'))
\mwedge{} (\mforall{}e'':E. ((e' <loc e'') {}\mRightarrow{} (e'' <loc e) {}\mRightarrow{} (\mneg{}\muparrow{}(P e'')))))\})
\mvee{} (\mneg{}(\mexists{}e':\{E| ((e' <loc e) \mwedge{} (\muparrow{}(P e')))\})))
Date html generated:
2012_01_23-PM-12_26_23
Last ObjectModification:
2011_12_13-PM-02_56_43
Home
Index