Nuprl Lemma : RSC_voter_start_unique
Cmd:ValueAllType. eq:EqDecider(Cmd). locs,clients:bag(Id). es:EO'. n,max1,max2:
. missing1,missing2: List.
e1,e2:E. c1,c2:Cmd.
(<max1, missing1> 
Prior(RSC_ReplicaState(Cmd))?
z.{<0, []>}(e1)
((max1 < n) 
(n missing1))
(<n, c1> Base(``sc propose``; 
Cmd)(e1)
(
j:. x:Id. <<<n, j>, c1>, x> Base(``sc vote``; Cmd Id)(e1)))
<max2, missing2> Prior(RSC_ReplicaState(Cmd))?z.{<0, []>}(e2)
((max2 < n) (n missing2))
(<n, c2> Base(``sc propose``; Cmd)(e2)
(j:. x:Id. <<<n, j>, c2>, x> Base(``sc vote``; Cmd Id)(e2)))
(loc(e1) = loc(e2))
(e1 = e2))
Proof not projected
Definitions occuring in Statement :
RSC_ReplicaState: RSC_ReplicaState(Cmd),
base-headers-msg-val: Base(hdr;typ),
Message: Message,
primed-class-opt: Prior(X)?b,
classrel: v X(e),
event-ordering+: EO+(Info),
es-loc: loc(e),
es-E: E,
Id: Id,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
or: P Q,
less_than: a < b,
lambda: x.A[x],
pair: <a, b>,
product: x:A B[x],
cons: [car / cdr],
nil: [],
list: type List,
natural_number: $n,
int: ,
token: "$token",
equal: s = t,
l_member: (x l),
deq: EqDecider(T),
single-bag: {x},
bag: bag(T),
vatype: ValueAllType
Definitions :
all: x:A. B[x],
vatype: ValueAllType,
implies: P Q,
classrel: v X(e),
RSC_ReplicaState: Error :RSC_ReplicaState,
or: P Q,
exists: x:A. B[x],
member: t T,
and: P 
Q,
RSC_Proposal: Error :RSC_Proposal,
RSC_Propose: Error :RSC_Propose,
RSC_vote2prop: Error :RSC_vote2prop,
RSC_Vote: Error :RSC_Vote,
sq_or: a 
b,
squash: T,
true: True,
prop: 
,
guard: {T},
cand: A c B,
Accum-class: Accum-class(f;init;X),
rec-combined-class-opt-1: F|X,Prior(self)?init|,
rec-comb: rec-comb(X;f;init),
select: l[i],
ycomb: Y,
ifthenelse: if b then t else f fi ,
le_int: i 
z j,
bnot: 
b,
lt_int: i <z j,
bfalse: ff,
btrue: tt,
name: Name,
le: A B,
not: A,
subtype: S 
T,
false: False,
iff: P 
Q,
rev_implies: P Q,
top: Top,
so_lambda: 
x.t[x],
uall: [x:A]. B[x],
rev_uimplies: rev_uimplies(P;Q),
uiff: uiff(P;Q),
uimplies: b supposing a,
sq_stable: SqStable(P),
es-locl: (e <loc e'),
es-p-local-pred: es-p-local-pred(es;P),
decidable: Dec(P),
es-le: e loc e' ,
RSC_onpropose: Error :RSC_onpropose,
ge: i 
j ,
l_all: (xL.P[x]),
gt: i > j,
sq_type: SQType(T),
single-valued-classrel: single-valued-classrel(es;X;T),
pi1: fst(t),
pi2: snd(t),
so_apply: x[s],
eclass: EClass(A[eo; e])
Lemmas :
es-locl-trichotomy,
event-ordering+_inc,
Message_wf,
parallel-classrel,
Error :RSC_Propose_wf,
simple-loc-comb-1_wf,
concat-lifting-loc-1_wf,
Error :RSC_vote2prop_wf,
Error :RSC_Vote_wf,
classrel_wf,
simple-loc-comb-1-concat-classrel,
bag-member-single,
bag-member_wf,
Id_wf,
bag_wf,
bag-member-lifting-2,
Error :RSC_onpropose_wf,
Error :RSC_Proposal_wf,
sq_stable__valueall-type,
valueall-type_wf,
primed-class-opt_wf,
Error :RSC_ReplicaState_wf,
es-loc_wf,
base-headers-msg-val_wf,
l_member_wf,
es-E_wf,
event-ordering+_wf,
deq_wf,
primed-class-opt-classrel,
single-bag_wf,
decidable__es-le,
decidable__es-locl,
es-le-not-locl,
es-le_wf,
le_wf,
not_wf,
sq_stable__and,
sq_stable_from_decidable,
decidable__le,
sq_stable__not,
lt_int_wf,
bool_wf,
assert_wf,
RSC_ReplicaState-prop2,
append_wf,
from-upto_wf,
le_int_wf,
bnot_wf,
list-diff_wf,
int-deq_wf,
bool_cases,
subtype_base_sq,
bool_subtype_base,
uiff_transitivity,
eqtt_to_assert,
assert_of_lt_int,
eqff_to_assert,
assert_functionality_wrt_uiff,
bnot_of_lt_int,
assert_of_le_int,
iff_transitivity,
member_append,
or_functionality_wrt_uiff3,
from-upto-member,
member-list-diff,
and_functionality_wrt_iff,
not_functionality_wrt_iff,
member_singleton,
RSC_ReplicaState-prop1,
RSC_ReplicaState-single-val,
pi1_wf_top,
Error :pi2_wf,
list_subtype_base,
int_subtype_base
\mforall{}Cmd:ValueAllType. \mforall{}eq:EqDecider(Cmd). \mforall{}locs,clients:bag(Id). \mforall{}es:EO'. \mforall{}n,max1,max2:\mBbbZ{}.
\mforall{}missing1,missing2:\mBbbZ{} List. \mforall{}e1,e2:E. \mforall{}c1,c2:Cmd.
(<max1, missing1> \mmember{} Prior(RSC\_ReplicaState(Cmd))?\mlambda{}z.\{ɘ, []>\}(e1)
{}\mRightarrow{} ((max1 < n) \mvee{} (n \mmember{} missing1))
{}\mRightarrow{} (<n, c1> \mmember{} Base(``sc propose``;\mBbbZ{} \mtimes{} Cmd)(e1)
\mvee{} (\mexists{}j:\mBbbZ{}. \mexists{}x:Id. <<<n, j>, c1>, x> \mmember{} Base(``sc vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e1)))
{}\mRightarrow{} <max2, missing2> \mmember{} Prior(RSC\_ReplicaState(Cmd))?\mlambda{}z.\{ɘ, []>\}(e2)
{}\mRightarrow{} ((max2 < n) \mvee{} (n \mmember{} missing2))
{}\mRightarrow{} (<n, c2> \mmember{} Base(``sc propose``;\mBbbZ{} \mtimes{} Cmd)(e2)
\mvee{} (\mexists{}j:\mBbbZ{}. \mexists{}x:Id. <<<n, j>, c2>, x> \mmember{} Base(``sc vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e2)))
{}\mRightarrow{} (loc(e1) = loc(e2))
{}\mRightarrow{} (e1 = e2))
Date html generated:
2012_02_20-PM-04_03_36
Last ObjectModification:
2012_02_02-PM-01_59_47
Home
Index