Nuprl Lemma : last-event-of-set
es:EO. n:
. f:n 
E. 
k:n. i:n. f i 
loc f k supposing i,j:n. (loc(f i) = loc(f j))
Proof not projected
Definitions occuring in Statement :
es-le: e loc e' ,
es-loc: loc(e),
es-E: E,
event_ordering: EO,
Id: Id,
int_seg: {i..j
},
nat_plus: ,
uimplies: b supposing a,
all: x:A. B[x],
exists: x:A. B[x],
apply: f a,
function: x:A B[x],
natural_number: $n,
equal: s = t
Definitions :
so_lambda: 
x.t[x],
implies: P 
Q,
member: t 
T,
uimplies: b supposing a,
all: x:A. B[x],
prop: 
,
false: False,
not: 
A,
le: A B,
and: P 
Q,
lelt: i j < k,
exists: x:A. B[x],
int_seg: {i..j},
guard: {T},
or: P 
Q,
es-le: e loc e' ,
suptype: suptype(S; T),
subtype: S 
T,
rev_implies: P 
Q,
iff: P Q,
sq_type: SQType(T),
decidable: Dec(P),
so_apply: x[s],
uall: [x:A]. B[x],
nat_plus:
Lemmas :
event_ordering_wf,
nat_plus_wf,
int_subtype_base,
subtype_base_sq,
decidable__equal_int,
less_than_wf,
es-E_wf,
es-loc_wf,
Id_wf,
equal_wf,
all_wf,
int_seg_wf,
nat_plus_properties,
es-le_wf,
le_wf,
es-locl_wf,
lelt_wf,
decidable__es-le,
es-le-not-locl,
decidable__es-locl,
es-le_weakening,
es-locl_transitivity1
\mforall{}es:EO. \mforall{}n:\mBbbN{}\msupplus{}. \mforall{}f:\mBbbN{}n {}\mrightarrow{} E. \mexists{}k:\mBbbN{}n. \mforall{}i:\mBbbN{}n. f i \mleq{}loc f k supposing \mforall{}i,j:\mBbbN{}n. (loc(f i) = loc(f j))
Date html generated:
2012_01_23-PM-12_09_36
Last ObjectModification:
2011_12_14-PM-09_20_41
Home
Index