Nuprl Lemma : at-majority-locs_wf2
[es:EO']. [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]),
Message: Message,
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
Definitions :
int: 
,
void: Void,
implies: P 
Q,
false: False,
not: 
A,
nequal: a 
b T ,
set: {x:A| B[x]} ,
listp: A List
,
combination: Combination(n;T),
uimplies: b supposing a,
bag: bag(T),
es-loc: loc(e),
lambda: 
x.A[x],
map: map(f;as),
natural_number: $n,
length: ||as||,
divide: n 
m,
less_than: a < b,
gt: i > j,
no_repeats: no_repeats(T;l),
l_member: (x l),
so_lambda: 
x.t[x],
l_all: (xL.P[x]),
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]),
Message: Message,
equal: s = t,
Id: Id,
list: type List,
uall: [x:A]. B[x],
prop: ,
universe: Type,
es-E: E,
event-ordering+: EO+(Info),
event_ordering: EO,
function: x:A B[x],
member: t T,
isect: 
x:A. B[x],
tactic: Error :tactic
Lemmas :
l_member_wf,
es-E_wf,
l_all_wf2,
l_all_wf,
Id_wf,
es-loc_wf,
map_wf,
no_repeats_wf,
length_wf1,
gt_wf,
Message_wf,
event-ordering+_wf,
event-ordering+_inc
\mforall{}[es:EO']. \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_58_10
Last ObjectModification:
2011_05_10-PM-04_40_10
Home
Index