Nuprl Lemma : rsc4-votes-consistent
[Cmd:ValueAllType]. [cmdeq:EqDecider(Cmd)]. [locs,clients:bag(Id)]. [coeff,flrs:
]. [es:EO'].
((StandardAssumptions(rsc4_Main) es)
(e1,e2:E. n,i:. x,y,z:Id. c1,c2:Cmd.
(<y, make-Msg(``rsc4 vote``; 
Cmd Id;<<<n, i>, c1>, x>)> 
rsc4_Main(e1)
<z, make-Msg(``rsc4 vote``; Cmd Id;<<<n, i>, c2>, x>)> rsc4_Main(e2)
(c1 = c2))))
Proof
Definitions occuring in Statement :
rsc4_stdma: StandardAssumptions(rsc4_Main),
rsc4_main: rsc4_Main,
make-Msg: make-Msg(hdr;typ;val),
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],
cons: [car / cdr],
nil: [],
int: ,
token: "$token",
equal: s = t,
deq: EqDecider(T),
bag: bag(T),
vatype: ValueAllType
Definitions :
implies: P Q,
uall: [x:A]. B[x],
std-ma: StandardMessageAutomaton(X;hdrs),
so_lambda: 
x.t[x],
prop: 
,
true: True,
member: t T,
squash: 
T,
and: P 
Q,
all: x:A. B[x],
rsc4_stdma: StandardAssumptions(rsc4_Main),
vatype: ValueAllType,
rsc4_Proposal: rsc4_Proposal(Cmd),
sq_or: a 
b,
guard: {T},
or: P Q,
cand: A c B,
rsc4_vote2prop: rsc4_vote2prop(Cmd),
exists: 
x:A. B[x],
pi2: snd(t),
msg-has-type: msg-has-type(m;T),
name: Name,
tl: tl(l),
false: False,
subtype: S 
T,
top: Top,
pi1: fst(t),
rsc4_NewRoundsState: rsc4_NewRoundsState(Cmd),
iff: P 
Q,
rev_implies: P Q,
so_lambda: x y.t[x; y],
rsc4_RoundInfo: rsc4_RoundInfo(Cmd),
uiff: uiff(P;Q),
rsc4_retry'base: rsc4_retry'base(Cmd),
rsc4_vote2retry: rsc4_vote2retry(Cmd),
rsc4_vote'base: rsc4_vote'base(Cmd),
bfalse: ff,
btrue: tt,
eq_atom: x =a y,
atom-deq: AtomDeq,
band: p 
q,
list-deq: list-deq(eq),
name-deq: NameDeq,
ifthenelse: if b then t else f fi ,
name_eq: name_eq(x;y),
assert: 
b,
so_apply: x[s],
sq_stable: SqStable(P),
uimplies: b supposing a,
rev_uimplies: rev_uimplies(P;Q),
so_apply: x[s1;s2],
not: 
A,
le: A 
B,
single-valued-classrel: single-valued-classrel(es;X;T),
sq_type: SQType(T),
rsc4_ReplicaState: rsc4_ReplicaState(Cmd),
rsc4_propose'base: rsc4_propose'base(Cmd)
Lemmas :
deq_wf,
bag_wf,
event-ordering+_wf,
messages-delivered_wf,
message-constraint_wf,
rsc4_headers_no_inputs_wf,
std-ma_wf,
event-ordering+_inc,
es-E_wf,
Id-valueall-type,
int-valueall-type,
product-valueall-type,
make-Msg_wf,
valueall-type_wf,
sq_stable__valueall-type,
rsc4_main_wf,
Id_wf,
Message_wf,
classrel_wf,
rsc4-vote,
true_wf,
squash_wf,
equal_wf,
es-le-loc,
rsc4_vote'base_wf,
rsc4_vote2prop_wf,
concat-lifting-loc-1_wf,
simple-loc-comb-1_wf,
rsc4_propose'base_wf,
parallel-classrel,
rsc4_voter_start_unique,
es-loc_wf,
bag-member_wf,
bag-member-single,
simple-loc-comb-1-concat-classrel,
pi2_wf,
msg-has-type_wf,
assert_wf,
msg-body_wf2,
es-info_wf,
and_wf,
base-noloc-classrel,
tl_wf,
name_wf,
es-header_wf,
pi1_wf_top,
assert_of_le_int,
eo-forward_wf,
rsc4_pos_rounds,
es-locl-trichotomy,
eclass_wf,
es-locl_wf,
es-le_wf,
rsc4_NewRoundsState_wf,
eo-forward-locl,
member-eo-forward-E,
rsc4_rounds_state_mem,
rsc4_vote2retry_wf,
rsc4_retry'base_wf,
eo-forward-base-classrel,
exists_wf,
base-headers-msg-val_wf,
or_wf,
single-valued-classrel-base,
assert-name_eq,
atom_subtype_base,
list_subtype_base,
subtype_base_sq
\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{}e1,e2:E. \mforall{}n,i:\mBbbZ{}. \mforall{}x,y,z:Id. \mforall{}c1,c2:Cmd.
(<y, make-Msg(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<n, i>, c1>, x>)> \mmember{} rsc4\_Main(e1)
{}\mRightarrow{} <z, make-Msg(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<n, i>, c2>, x>)> \mmember{} rsc4\_Main(e2)
{}\mRightarrow{} (c1 = c2))))
Date html generated:
2012_02_20-PM-04_59_38
Last ObjectModification:
2012_02_02-PM-02_16_41
Home
Index