Nuprl Lemma : RSC-decided-property
[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)
(e:E. c:Cmd. n:.
(<n, c> 
RSC_Decided(Cmd)(e)
(
x:Id
rnd:
L:Id List
((no_repeats(Id;L) 
(||L|| = ((2 * f) + 1)))
(vtrL.(e':E
<x, make-Msg(``sc vote``; 
Cmd Id;<<<n, rnd>, c>, vtr>)>
RSC_SimpleConsensus_main{mark-simple-consensus-V2.esh:o}(Cmd; clients; eq; f; locs)(e'))
vtr locs))))))
Proof not projected
Definitions occuring in Statement :
RSC_Decided: RSC_Decided(Cmd),
make-Msg: make-Msg(hdr;typ;val),
Message: Message,
classrel: v X(e),
event-ordering+: EO+(Info),
es-E: E,
Id: Id,
length: ||as||,
nat: ,
uall: [x:A]. B[x],
all: x:A. B[x],
exists: x:A. B[x],
squash: T,
implies: P Q,
and: P Q,
apply: f a,
pair: <a, b>,
product: x:A B[x],
cons: [car / cdr],
nil: [],
list: type List,
multiply: n * m,
add: n + m,
natural_number: $n,
int: ,
token: "$token",
equal: s = t,
l_all: (xL.P[x]),
no_repeats: no_repeats(T;l),
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],
squash: T,
exists: x:A. B[x],
and: P Q,
length: ||as||,
member: t T,
true: True,
not: 
A,
RSC_SimpleConsensus_headers_no_inputs: Error :RSC_SimpleConsensus_headers_no_inputs,
es-header: es-header(es;e),
name: Name,
so_lambda: 
x.t[x],
select: l[i],
int_seg: {i..j
},
ycomb: Y,
lelt: i 
j < k,
le: A B,
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,
cand: A c B,
nat: ,
top: Top,
RSC_VotesInRound: Error :RSC_VotesInRound,
Accum-class: Accum-class(f;init;X),
RSC_collect: Error :RSC_collect,
RSC_Vote: Error :RSC_Vote,
uiff: uiff(P;Q),
band: p q,
guard: {T},
l_all: (xL.P[x]),
bag-member: x bs,
Id: Id,
RSC_SimpleConsensus_stdma: Error :RSC_SimpleConsensus_stdma,
RSC_Decided: Error :RSC_Decided,
sq_stable: SqStable(P),
message-constraint: message-constraint{i:l}(es;X;hdrs),
std-ma: StandardMessageAutomaton(X;hdrs),
uimplies: b supposing a,
so_apply: x[s],
or: P 
Q,
sq_or: a b,
iff: P 
Q,
rev_uimplies: rev_uimplies(P;Q),
bool: 
,
unit: Unit,
l_member: (x l),
sq_type: SQType(T),
msg-header: msg-header(m),
subtype: S 
T,
it: 
Lemmas :
sq_stable__valueall-type,
valueall-type_wf,
base-noloc-classrel-make-Msg,
product-valueall-type,
int-valueall-type,
select_member,
name_wf,
le_wf,
l_member_wf,
msg-header_wf,
Error :RSC_SimpleConsensus_headers_no_inputs_wf,
squash_wf,
es-E_wf,
event-ordering+_inc,
Message_wf,
es-causl_wf,
classrel_wf,
Id_wf,
Error :RSC_SimpleConsensus_main_wf,
es-loc_wf,
RSC_decided,
Error :RSC_Decided_wf,
Error :RSC_SimpleConsensus_stdma_wf,
event-ordering+_wf,
bag_wf,
deq_wf,
member-eo-forward-E,
sq_stable_from_decidable,
es-le_wf,
decidable__es-le,
primed-class-opt_wf,
single-bag_wf,
Error :RSC_VotesInRound_wf,
eo-forward_wf,
not_wf,
length_wf,
pi1_wf_top,
poss-maj_wf,
subtype_rel_simple_product,
top_wf,
Error :pi2_wf,
nat_wf,
base-headers-msg-val_wf,
eo-forward-E-subtype,
RSC_PrVoterState-inv,
rec-combined-class-opt-1-classrel,
Error :RSC_collect_wf,
simple-comb-2-classrel,
Error :RSC_Vote_wf,
rec-combined-class-opt-1_wf,
lifting-2_wf,
eq_int_wf,
bool_wf,
uiff_transitivity,
assert_wf,
eqtt_to_assert,
assert_of_eq_int,
deq-member_wf,
id-deq_wf,
iff_transitivity,
iff_weakening_uiff,
assert-deq-member,
bnot_wf,
eqff_to_assert,
assert_of_bnot,
not_functionality_wrt_iff,
not_functionality_wrt_uiff,
eo-forward-base-classrel,
nat_properties,
RSC_VotesInRound-inv,
no_repeats_wf,
l_all_wf2,
make-Msg_wf,
Id-valueall-type,
bag-member_wf,
subtype_base_sq,
atom2_subtype_base,
poss-maj-unanimous,
pair-eta,
select_wf,
es-le-loc,
eo-forward-loc,
RSC_vote
\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{}e:E. \mforall{}c:Cmd. \mforall{}n:\mBbbZ{}.
(<n, c> \mmember{} RSC\_Decided(Cmd)(e)
{}\mRightarrow{} (\mdownarrow{}\mexists{}x:Id
\mexists{}rnd:\mBbbN{}
\mexists{}L:Id List
((no\_repeats(Id;L) \mwedge{} (||L|| = ((2 * f) + 1)))
\mwedge{} (\mforall{}vtr\mmember{}L.(\mdownarrow{}\mexists{}e':E
<x, make-Msg(``sc vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<n, rnd>, c>, vtr>)> \mmember{}
RSC\_SimpleConsensus\_main\{mark-simple-consensus-V2.esh:o\}(Cmd;
clients;
eq;
f;
locs)(e'))
\mwedge{} vtr \mdownarrow{}\mmember{} locs))))))
Date html generated:
2012_02_20-PM-04_03_58
Last ObjectModification:
2012_02_02-PM-01_59_49
Home
Index