Nuprl Definition : at-majority-locs
at-majority-locs(es;elist;locs;e.P[e]) ==
(||elist|| > (||locs|| 
2)) 
no_repeats(Id;map(
e.loc(e);elist)) (
e
elist.P[e]) (eelist.(loc(e) locs))
Proof not projected
Definitions occuring in Statement :
es-loc: loc(e),
es-E: E,
Id: Id,
map: map(f;as),
length: ||as||,
gt: i > j,
and: P Q,
lambda: x.A[x],
divide: n m,
natural_number: $n,
l_all: (xL.P[x]),
no_repeats: no_repeats(T;l),
l_member: (x l)
Definitions :
gt: i > j,
divide: n m,
length: ||as||,
natural_number: $n,
no_repeats: no_repeats(T;l),
map: map(f;as),
lambda: x.A[x],
and: P Q,
l_all: (xL.P[x]),
es-E: E,
l_member: (x l),
es-loc: loc(e),
Id: Id
FDL editor aliases :
at-majority-locs
at-majority-locs(es;elist;locs;e.P[e]) ==
(||elist|| > (||locs|| \mdiv{} 2))
\mwedge{} no\_repeats(Id;map(\mlambda{}e.loc(e);elist))
\mwedge{} (\mforall{}e\mmember{}elist.P[e])
\mwedge{} (\mforall{}e\mmember{}elist.(loc(e) \mmember{} locs))
Date html generated:
2011_10_20-PM-04_57_40
Last ObjectModification:
2011_05_10-PM-04_29_09
Home
Index