Nuprl Lemma : rsc4-decided-property
[Cmd:ValueAllType]. [cmdeq:EqDecider(Cmd)]. [locs,clients:bag(Id)]. [coeff,flrs:
]. [es:EO'].
((StandardAssumptions(rsc4_Main) es)
(e:E. c:Cmd. n:.
(<n, c> 
rsc4_decided'base(Cmd)(e)
(
x:Id
rnd:
L:Id List
((no_repeats(Id;L) 
(||L|| = ((coeff * flrs) + 1)))
(vtrL.(e':E. <x, make-Msg(``rsc4 vote``; 
Cmd Id;<<<n, rnd>, c>, vtr>)> rsc4_Main(e'))
vtr locs))))))
Proof
Definitions occuring in Statement :
rsc4_stdma: StandardAssumptions(rsc4_Main),
rsc4_main: rsc4_Main,
rsc4_decided'base: rsc4_decided'base(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 :
top: Top,
cand: A c B,
subtype: S 
T,
bfalse: ff,
btrue: tt,
lt_int: i <z j,
bnot: 
b,
le_int: i 
z j,
ifthenelse: if b then t else f fi ,
prop: 
,
false: False,
not: A,
le: A B,
lelt: i j < k,
ycomb: Y,
int_seg: {i..j
},
select: l[i],
so_lambda: 
x.t[x],
name: Name,
es-header: es-header(es;e),
rsc4_headers_no_inputs: rsc4_headers_no_inputs(),
true: True,
member: t T,
length: ||as||,
and: P Q,
nat: ,
squash: T,
all: x:A. B[x],
implies: P Q,
vatype: ValueAllType,
uall: [x:A]. B[x],
rsc4_QuorumState: rsc4_QuorumState(Cmd),
guard: {T},
exists: x:A. B[x],
l_all: (xL.P[x]),
Id: Id,
msg-header: msg-header(m),
pi1: fst(t),
or: P 
Q,
rsc4_NewRoundsState: rsc4_NewRoundsState(Cmd),
iff: P 
Q,
sq_or: a b,
so_apply: x[s],
uiff: uiff(P;Q),
uimplies: b supposing a,
std-ma: StandardMessageAutomaton(X;hdrs),
message-constraint: message-constraint{i:l}(es;X;hdrs),
sq_stable: SqStable(P),
rsc4_decided'base: rsc4_decided'base(Cmd),
rsc4_stdma: StandardAssumptions(rsc4_Main),
rsc4_newvote: rsc4_newvote(Cmd),
sq_type: SQType(T),
l_member: (x l),
pMsg: pMsg(P.M[P]),
rev_implies: P Q,
rsc4_vote'base: rsc4_vote'base(Cmd),
Message: Message
Lemmas :
deq_wf,
bag_wf,
event-ordering+_wf,
rsc4_stdma_wf,
rsc4_decided'base_wf,
le_wf,
pi1_wf_top,
top_wf,
nat_wf,
subtype_rel_simple_product,
poss-maj_wf,
pair-eta,
poss-maj-unanimous,
rsc4-decided,
es-loc_wf,
rsc4_main_wf,
Id_wf,
classrel_wf,
es-causl_wf,
Message_wf,
event-ordering+_inc,
es-E_wf,
exists_wf,
squash_wf,
rsc4_headers_no_inputs_wf,
msg-header_wf,
l_member_wf,
lelt_wf,
name_wf,
select_member,
int-valueall-type,
product-valueall-type,
base-noloc-classrel-make-Msg,
valueall-type_wf,
sq_stable__valueall-type,
equal_wf,
decidable__es-le,
es-le_wf,
sq_stable_from_decidable,
member-eo-forward-E,
eo-forward_wf,
rsc4_quorum_invariant,
assert-deq-member,
not_functionality_wrt_iff,
assert_of_bnot,
assert_of_eq_int,
and_functionality_wrt_uiff,
uiff_transitivity,
and_functionality_wrt_iff,
assert_of_band,
iff_weakening_uiff,
iff_transitivity,
not_wf,
id-deq_wf,
deq-member_wf,
bnot_wf,
eq_int_wf,
band_wf,
assert_wf,
bag-member_wf,
Id-valueall-type,
make-Msg_wf,
l_all_wf2,
length_wf,
no_repeats_wf,
and_wf,
no_repeats_cons,
cons_member,
sq_stable__bag-member,
sq_stable__squash,
sq_stable__and,
l_all_cons,
int_subtype_base,
atom2_subtype_base,
subtype_base_sq,
rsc4-vote,
es-info_wf,
eo-forward-E-subtype,
rsc4_vote'base_wf,
select_wf,
eo-forward-info,
base-noloc-classrel,
eo-forward-loc,
es-le-loc,
es-info-make-Msg,
subtype_rel_set,
assert_of_le_int,
rsc4_pos_rounds
\mforall{}[Cmd:ValueAllType]. \mforall{}[cmdeq:EqDecider(Cmd)]. \mforall{}[locs,clients:bag(Id)]. \mforall{}[coeff,flrs:\mBbbZ{}]. \mforall{}[es:EO'].
((StandardAssumptions(rsc4\_Main) es)
{}\mRightarrow{} (\mforall{}e:E. \mforall{}c:Cmd. \mforall{}n:\mBbbZ{}.
(<n, c> \mmember{} rsc4\_decided'base(Cmd)(e)
{}\mRightarrow{} (\mdownarrow{}\mexists{}x:Id
\mexists{}rnd:\mBbbN{}
\mexists{}L:Id List
((no\_repeats(Id;L) \mwedge{} (||L|| = ((coeff * flrs) + 1)))
\mwedge{} (\mforall{}vtr\mmember{}L.(\mdownarrow{}\mexists{}e':E
<x, make-Msg(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<n, rnd>, c>, vtr>)> \mmember{}
rsc4\_Main(e'))
\mwedge{} vtr \mdownarrow{}\mmember{} locs))))))
Date html generated:
2012_02_20-PM-05_00_23
Last ObjectModification:
2012_02_02-PM-02_16_43
Home
Index