Nuprl Lemma : at-majority-locs_wf
[Info:Type]. [es:EO+(Info)]. [elist:E List]. [locs:Id List]. [P:E 
].
(at-majority-locs(es;elist;locs;e.P[e]) 
)
Proof not projected
Definitions occuring in Statement :
at-majority-locs: at-majority-locs(es;elist;locs;e.P[e]),
event-ordering+: EO+(Info),
es-E: E,
Id: Id,
uall: [x:A]. B[x],
prop: ,
so_apply: x[s],
member: t T,
function: x:A B[x],
list: type List,
universe: Type
Definitions :
int: 
,
void: Void,
implies: P 
Q,
false: False,
not: 
A,
nequal: a 
b T ,
l_member: (x l),
set: {x:A| B[x]} ,
so_lambda: 
x.t[x],
l_all: (xL.P[x]),
es-loc: loc(e),
lambda: x.A[x],
listp: A List
,
combination: Combination(n;T),
uimplies: b supposing a,
bag: bag(T),
map: map(f;as),
no_repeats: no_repeats(T;l),
natural_number: $n,
length: ||as||,
divide: n 
m,
less_than: a < b,
gt: i > j,
product: x:A 
B[x],
and: P 
Q,
subtype: S 
T,
all: x:A. B[x],
axiom: Ax,
apply: f a,
so_apply: x[s],
at-majority-locs: at-majority-locs(es;elist;locs;e.P[e]),
equal: s = t,
Id: Id,
list: type List,
uall: [x:A]. B[x],
isect: 
x:A. B[x],
member: t T,
function: x:A B[x],
prop: ,
universe: Type,
es-E: E,
event_ordering: EO,
event-ordering+: EO+(Info),
tactic: Error :tactic
Lemmas :
event-ordering+_inc,
event-ordering+_wf,
gt_wf,
length_wf1,
no_repeats_wf,
map_wf,
l_all_wf2,
es-E_wf,
Id_wf,
l_member_wf,
es-loc_wf
\mforall{}[Info:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[elist:E List]. \mforall{}[locs:Id List]. \mforall{}[P:E {}\mrightarrow{} \mBbbP{}].
(at-majority-locs(es;elist;locs;e.P[e]) \mmember{} \mBbbP{})
Date html generated:
2011_10_20-PM-04_57_55
Last ObjectModification:
2011_05_10-PM-04_30_50
Home
Index