Nuprl Lemma : RSC-votes-consistent
[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)
(e1,e2:E. n,i:. x,y,z:Id. c1,c2:Cmd.
(<y, make-Msg(``sc vote``; 
Cmd Id;<<<n, i>, c1>, x>)> 
RSC_SimpleConsensus_main{mark-simple-consensus-V2.esh:o}(Cmd; clients; eq; f; locs)(e1)
<z, make-Msg(``sc vote``; Cmd Id;<<<n, i>, c2>, x>)>
RSC_SimpleConsensus_main{mark-simple-consensus-V2.esh:o}(Cmd; clients; eq; f; locs)(e2)
(c1 = c2))))
Proof not projected
Definitions occuring in Statement :
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 :
uall: [x:A]. B[x],
vatype: ValueAllType,
implies: P Q,
all: x:A. B[x],
member: t T,
so_lambda: 
x.t[x],
squash: 
T,
true: True,
prop: 
,
name: Name,
msg-has-type: msg-has-type(m;T),
pi2: snd(t),
and: P 
Q,
assert: 
b,
uiff: uiff(P;Q),
name_eq: name_eq(x;y),
ifthenelse: if b then t else f fi ,
name-deq: NameDeq,
list-deq: list-deq(eq),
band: p 
q,
atom-deq: AtomDeq,
eq_atom: x =a y,
btrue: tt,
bfalse: ff,
false: False,
exists: 
x:A. B[x],
pi1: fst(t),
top: Top,
so_apply: x[s],
sq_stable: SqStable(P),
sq_or: a 
b,
iff: P 
Q,
uimplies: b supposing a,
or: P Q,
cand: A c B,
sq_type: SQType(T),
guard: {T},
rev_implies: P Q,
subtype: S 
T
Lemmas :
Id_wf,
product-valueall-type,
int-valueall-type,
sq_stable__valueall-type,
Id-valueall-type,
valueall-type_wf,
RSC_vote,
classrel_wf,
Message_wf,
Error :RSC_SimpleConsensus_main_wf,
make-Msg_wf,
es-E_wf,
event-ordering+_inc,
Error :RSC_SimpleConsensus_stdma_wf,
event-ordering+_wf,
bag_wf,
deq_wf,
RSC_voter_start_unique,
es-le-loc,
base-noloc-classrel,
es-info_wf,
msg-body_wf2,
squash_wf,
assert_wf,
msg-has-type_wf,
Error :pi2_wf,
base-headers-msg-val_wf,
subtype_base_sq,
name_wf,
list_subtype_base,
atom_subtype_base,
assert-name_eq,
top_wf,
pi1_wf_top,
true_wf,
RSC_PrVoterState-inv,
eo-forward_wf,
member-eo-forward-E,
es-loc_wf,
RSC_VoterState-trans,
primed-class-opt_wf,
single-bag_wf,
Error :RSC_VoterState_wf,
es-locl_wf,
es-locl-trichotomy,
eo-forward-locl,
es-le_wf,
exists_functionality_wrt_iff,
iff_weakening_uiff,
eo-forward-base-classrel,
primed-class-opt-classrel,
Error :RSC_ReplicaState_wf
\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{}e1,e2:E. \mforall{}n,i:\mBbbZ{}. \mforall{}x,y,z:Id. \mforall{}c1,c2:Cmd.
(<y, make-Msg(``sc vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<n, i>, c1>, x>)> \mmember{}
RSC\_SimpleConsensus\_main\{mark-simple-consensus-V2.esh:o\}(Cmd; clients; eq; f; locs)(e1)
{}\mRightarrow{} <z, make-Msg(``sc vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<n, i>, c2>, x>)> \mmember{}
RSC\_SimpleConsensus\_main\{mark-simple-consensus-V2.esh:o\}(Cmd; clients; eq; f; locs)(e2)
{}\mRightarrow{} (c1 = c2))))
Date html generated:
2012_02_20-PM-04_03_47
Last ObjectModification:
2012_02_02-PM-01_59_48
Home
Index