Nuprl Lemma : rsc4_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> 
rsc4_ReplicaState(Cmd)(e1)
((max1 < n) 
(n missing1))
<n, c1> rsc4_Proposal(Cmd)(e1)
<max2, missing2> rsc4_ReplicaState(Cmd)(e2)
((max2 < n) (n missing2))
<n, c2> rsc4_Proposal(Cmd)(e2)
(loc(e1) = loc(e2))
(e1 = e2))
Proof
Definitions occuring in Statement :
rsc4_ReplicaState: rsc4_ReplicaState(Cmd),
rsc4_Proposal: rsc4_Proposal(Cmd),
Message: Message,
classrel: v X(e),
event-ordering+: EO+(Info),
es-loc: loc(e),
es-E: E,
Id: Id,
all: x:A. B[x],
implies: P Q,
or: P Q,
less_than: a < b,
pair: <a, b>,
product: x:A 
B[x],
list: type List,
int: ,
equal: s = t,
l_member: (x l),
deq: EqDecider(T),
bag: bag(T),
vatype: ValueAllType
Definitions :
guard: {T},
so_lambda: 
x.t[x],
prop: 
,
false: False,
and: P 
Q,
member: t T,
iff: P 
Q,
rev_implies: P Q,
implies: P Q,
vatype: ValueAllType,
all: x:A. B[x],
uimplies: b supposing a,
so_apply: x[s],
not: 
A,
le: A 
B,
uall: [x:A]. B[x],
or: P Q,
subtype: S 
T
Lemmas :
valueall-type_wf,
deq_wf,
bag_wf,
event-ordering+_wf,
es-E_wf,
rsc4_ReplicaState_wf,
rsc4_Proposal_wf,
classrel_wf,
Message_wf,
es-loc_wf,
Id_wf,
equal_wf,
assert_of_lt_int,
or_functionality_wrt_iff,
implies_functionality_wrt_iff,
all_functionality_wrt_iff,
assert_of_le_int,
iff_weakening_uiff,
assert-int-list-member,
not_functionality_wrt_iff,
less_than_wf,
l_member_wf,
lt_int_wf,
or_wf,
all_wf,
le_int_wf,
int-list-member_wf,
assert_wf,
not_wf,
and_wf,
le_wf,
and_functionality_wrt_iff,
rsc4_replica_state_mem,
event-ordering+_inc,
es-locl-trichotomy
\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{} rsc4\_ReplicaState(Cmd)(e1)
{}\mRightarrow{} ((max1 < n) \mvee{} (n \mmember{} missing1))
{}\mRightarrow{} <n, c1> \mmember{} rsc4\_Proposal(Cmd)(e1)
{}\mRightarrow{} <max2, missing2> \mmember{} rsc4\_ReplicaState(Cmd)(e2)
{}\mRightarrow{} ((max2 < n) \mvee{} (n \mmember{} missing2))
{}\mRightarrow{} <n, c2> \mmember{} rsc4\_Proposal(Cmd)(e2)
{}\mRightarrow{} (loc(e1) = loc(e2))
{}\mRightarrow{} (e1 = e2))
Date html generated:
2012_02_20-PM-04_58_57
Last ObjectModification:
2012_02_02-PM-03_39_09
Home
Index