Nuprl Lemma : RSC_votes-from-locs
[Cmd:ValueAllType]. [eq:EqDecider(Cmd)]. [locs,clients:bag(Id)]. [f:
]. [es:EO'].
((RSC_SimpleConsensus_stdma{mark-simple-consensus-V2.esh:o, i:l}(Cmd; clients; eq; f; locs) es)
(n,i:. c:Cmd. l:Id. e:E. (<<<n, i>, c>, l> 
RSC_Vote(Cmd)(e) l 
locs)))
Proof not projected
Definitions occuring in Statement :
RSC_Vote: RSC_Vote(Cmd),
Message: Message,
classrel: v X(e),
event-ordering+: EO+(Info),
es-E: E,
Id: Id,
uall: [x:A]. B[x],
all: x:A. B[x],
implies: P Q,
apply: f a,
pair: <a, b>,
product: x:A 
B[x],
int: ,
deq: EqDecider(T),
bag-member: x bs,
bag: bag(T),
vatype: ValueAllType
Definitions :
uall: [x:A]. B[x],
vatype: ValueAllType,
implies: P Q,
all: x:A. B[x],
bag-member: x bs,
squash: T,
RSC_SimpleConsensus_headers_no_inputs: Error :RSC_SimpleConsensus_headers_no_inputs,
and: P 
Q,
es-header: es-header(es;e),
name: Name,
exists: 
x:A. B[x],
member: t T,
so_lambda: 
x.t[x],
true: True,
select: l[i],
int_seg: {i..j
},
length: ||as||,
ycomb: Y,
lelt: i 
j < k,
le: A B,
not: 
A,
false: False,
prop: 
,
ifthenelse: if b then t else f fi ,
le_int: i z j,
bnot: 
b,
lt_int: i <z j,
btrue: tt,
bfalse: ff,
Id: Id,
RSC_SimpleConsensus_stdma: Error :RSC_SimpleConsensus_stdma,
RSC_Vote: Error :RSC_Vote,
message-constraint: message-constraint{i:l}(es;X;hdrs),
std-ma: StandardMessageAutomaton(X;hdrs),
uimplies: b supposing a,
uiff: uiff(P;Q),
so_apply: x[s],
sq_stable: SqStable(P),
iff: P 
Q,
cand: A c B,
sq_type: SQType(T),
guard: {T},
msg-header: msg-header(m),
subtype: S 
T
Lemmas :
base-noloc-classrel-make-Msg,
Id_wf,
product-valueall-type,
int-valueall-type,
sq_stable__valueall-type,
Id-valueall-type,
valueall-type_wf,
select_member,
name_wf,
le_wf,
l_member_wf,
msg-header_wf,
Error :RSC_SimpleConsensus_headers_no_inputs_wf,
squash_wf,
es-causl_wf,
classrel_wf,
Error :RSC_SimpleConsensus_main_wf,
es-loc_wf,
RSC_vote,
event-ordering+_inc,
Message_wf,
Error :RSC_Vote_wf,
es-E_wf,
Error :RSC_SimpleConsensus_stdma_wf,
event-ordering+_wf,
bag_wf,
deq_wf,
subtype_base_sq,
atom2_subtype_base
\mforall{}[Cmd:ValueAllType]. \mforall{}[eq:EqDecider(Cmd)]. \mforall{}[locs,clients:bag(Id)]. \mforall{}[f:\mBbbZ{}]. \mforall{}[es:EO'].
((RSC\_SimpleConsensus\_stdma\{mark-simple-consensus-V2.esh:o, i:l\}(Cmd; clients; eq; f; locs) es)
{}\mRightarrow{} (\mforall{}n,i:\mBbbZ{}. \mforall{}c:Cmd. \mforall{}l:Id. \mforall{}e:E. (<<<n, i>, c>, l> \mmember{} RSC\_Vote(Cmd)(e) {}\mRightarrow{} l \mdownarrow{}\mmember{} locs)))
Date html generated:
2012_02_20-PM-04_03_26
Last ObjectModification:
2012_02_02-PM-01_59_46
Home
Index