Nuprl Lemma : rsc5-ilf
(
[Cmd:ValueAllType]. [es:EO']. [e:E].
v:
Cmd Id. {v 
rsc5_vote'base(Cmd)(e) 
v Base(``rsc5 vote``; Cmd Id)(e)})
([a:]. [es:EO']. [e:E]. {
rsc5_Halt() a(e) a Base(``rsc5 decided``;)(e)})
([b,a:]. [locs:bag(Id)]. [flrs,coeff:]. [clients:bag(Id)]. [Cmd:ValueAllType]. [cmdeq:EqDecider(Cmd)].
[es:EO']. [e:E]. [i:Id]. [m:Message].
{<i, m> rsc5_Quorum(Cmd;clients;cmdeq;coeff;flrs;locs) <a, b>(e)
a1,b1:
b2:Cmd
b3:Id
(<<<a1, b1>, b2>, b3> Base(``rsc5 vote``; Cmd Id)(e)
((a2:
b4:Cmd
(((((fst((rsc5_possmajstep(Cmd;cmdeq) (inl <a2, b4> ) b2))) = ((coeff * flrs) + 1))
(((m = make-Msg(``rsc5 decided``;;a1)) i locs)
((m = make-Msg([notify]; Cmd;<a1, snd((rsc5_possmajstep(Cmd;cmdeq) (inl <a2, b4> ) b2))>))
i clients)))
((
((fst((rsc5_possmajstep(Cmd;cmdeq) (inl <a2, b4> ) b2))) = ((coeff * flrs) + 1)))
(i = loc(e))
(m
= make-Msg(``rsc5 retry``; Cmd;<<a1, b1 + 1>
, snd((rsc5_possmajstep(Cmd;cmdeq) (inl <a2, b4> ) b2))
>))))
(b5:Id List
((<inl <a2, b4> , b5> Memory-class(rsc5_add_to_quorum(Cmd;cmdeq)
<a, b>;rsc5_init() <inr , []>;rsc5_vote'base(Cmd))(e)
(||b5|| = (coeff * flrs)))
(
(rsc5_newvote(Cmd) <a, b> <<<a1, b1>, b2>, b3> <inl <a2, b4> , b5>))))))
(((((fst((rsc5_possmajstep(Cmd;cmdeq) (inr ) b2))) = ((coeff * flrs) + 1))
(((m = make-Msg(``rsc5 decided``;;a1)) i locs)
((m = make-Msg([notify]; Cmd;<a1, snd((rsc5_possmajstep(Cmd;cmdeq) (inr ) b2))>))
i clients)))
((((fst((rsc5_possmajstep(Cmd;cmdeq) (inr ) b2))) = ((coeff * flrs) + 1)))
(i = loc(e))
(m
= make-Msg(``rsc5 retry``; Cmd;<<a1, b1 + 1>
, snd((rsc5_possmajstep(Cmd;cmdeq) (inr ) b2))
>))))
(b4:Id List
((<inr , b4> Memory-class(rsc5_add_to_quorum(Cmd;cmdeq)
<a, b>;rsc5_init() <inr , []>;rsc5_vote'base(Cmd))(e)
(||b4|| = (coeff * flrs)))
((rsc5_newvote(Cmd) <a, b> <<<a1, b1>, b2>, b3> <inr , b4>)))))))})
([Cmd:ValueAllType]. [es:EO']. [e:E].
v: Cmd
{v rsc5_RoundInfo(Cmd)(e)
v Base(``rsc5 retry``; Cmd)(e)
(a,b:
b1:Cmd
((v = <<a, b>, b1>) (b2:Id. <<<a, b>, b1>, b2> Base(``rsc5 vote``; Cmd Id)(e))))})
([Cmd:ValueAllType]. [es:EO']. [e:E].
v: Cmd
{v rsc5_Proposal(Cmd)(e)
v Base([propose]; Cmd)(e)
(a,b:
b1:Cmd. ((v = <a, b1>) (b2:Id. <<<a, b>, b1>, b2> Base(``rsc5 vote``; Cmd Id)(e))))})
([Cmd:ValueAllType]. [clients:bag(Id)]. [cmdeq:EqDecider(Cmd)]. [coeff,flrs:]. [locs:bag(Id)]. [es:EO'].
[e:E]. [i:Id]. [m:Message].
{<i, m> rsc5_main(Cmd;clients;cmdeq;coeff;flrs;locs)(e)
loc(e) locs
(e':{e':E| e' 
loc e }
a:
((b:Cmd
((<a, b> Base([propose]; Cmd)(e')
(b1:. b3:Id. <<<a, b1>, b>, b3> Base(``rsc5 vote``; Cmd Id)(e')))
((((i locs (m = make-Msg(``rsc5 vote``; Cmd Id;<<<a, 0>, b>, loc(e)>))) (e = e'))
((no rsc5_Quorum(Cmd;clients;cmdeq;coeff;flrs;locs) <a, 0> between e' and e)
<i, m> {rsc5_Quorum(Cmd;clients;cmdeq;coeff;flrs;locs) <a, 0>}(e)))
((no rsc5_Halt() a between e' and e) (e1:{e1:E| e1 loc ... } . ...)))))
...))})
Proof not projected
Definitions occuring in Statement :
rsc5_update_replica: rsc5_update_replica(Cmd),
rsc5_Proposal: rsc5_Proposal(Cmd),
rsc5_Halt: rsc5_Halt(),
rsc5_update_round: rsc5_update_round(Cmd),
rsc5_RoundInfo: rsc5_RoundInfo(Cmd),
rsc5_Quorum: rsc5_Quorum(Cmd;clients;cmdeq;coeff;flrs;locs),
rsc5_add_to_quorum: rsc5_add_to_quorum(Cmd;cmdeq),
rsc5_possmajstep: rsc5_possmajstep(Cmd;cmdeq),
rsc5_newvote: rsc5_newvote(Cmd),
rsc5_vote'base: rsc5_vote'base(Cmd),
Memory-class: Memory-class(f;init;X),
make-Msg: make-Msg(hdr;typ;val),
base-headers-msg-val: Base(hdr;typ),
Message: Message,
no-classrel-in-interval: (no X between start and e),
classrel: v X(e),
eo-forward: eo.e,
event-ordering+: EO+(Info),
es-le: e loc e' ,
es-loc: loc(e),
es-E: E,
Id: Id,
length: ||as||,
assert: b,
sq_or: a b,
it: ,
uall: [x:A]. B[x],
guard: {T},
pi1: fst(t),
pi2: snd(t),
all: x:A. B[x],
exists: x:A. B[x],
iff: P Q,
not: A,
squash: T,
or: P Q,
and: P Q,
unit: Unit,
less_than: a < b,
set: {x:A| B[x]} ,
apply: f a,
pair: <a, b>,
product: x:A B[x],
inr: inr x ,
inl: inl x ,
union: left + right,
cons: [car / cdr],
nil: [],
list: type List,
multiply: n * m,
add: n + m,
natural_number: $n,
int: ,
token: "$token",
equal: s = t,
l_member: (x l),
deq: EqDecider(T),
bag-member: x bs,
bag: bag(T),
vatype: ValueAllType
Definitions :
rsc5_main: rsc5_main(Cmd;clients;cmdeq;coeff;flrs;locs),
rsc5_Replica: rsc5_Replica(Cmd;clients;cmdeq;coeff;flrs;locs),
rsc5_Voter: rsc5_Voter(Cmd;clients;cmdeq;coeff;flrs;locs),
rsc5_NewVoters: rsc5_NewVoters(Cmd),
rsc5_NewRounds: rsc5_NewRounds(Cmd),
rsc5_Round: rsc5_Round(Cmd;clients;cmdeq;coeff;flrs;locs),
rsc5_NewRoundsState: rsc5_NewRoundsState(Cmd),
rsc5_when_new_round: rsc5_when_new_round(Cmd),
rsc5_vote'broadcast: rsc5_vote'broadcast(Cmd),
uiff: uiff(P;Q),
rsc5_ReplicaState: rsc5_ReplicaState(Cmd),
rsc5_when_new_proposal: rsc5_when_new_proposal(Cmd),
rsc5_Proposal: rsc5_Proposal(Cmd),
rsc5_vote2prop: rsc5_vote2prop(Cmd),
rsc5_propose'base: rsc5_propose'base(Cmd),
rsc5_RoundInfo: rsc5_RoundInfo(Cmd),
rsc5_vote2retry: rsc5_vote2retry(Cmd),
rsc5_retry'base: rsc5_retry'base(Cmd),
rsc5_Quorum: rsc5_Quorum(Cmd;clients;cmdeq;coeff;flrs;locs),
rsc5_QuorumState: rsc5_QuorumState(Cmd;cmdeq),
rsc5_when_quorum: rsc5_when_quorum(Cmd;clients;cmdeq;coeff;flrs;locs),
rsc5_roundout: rsc5_roundout(Cmd;clients;cmdeq;coeff;flrs;locs),
so_lambda: 
x y.t[x; y],
exposed-bfalse: exposed-bfalse,
rsc5_notify'broadcast: rsc5_notify'broadcast(Cmd),
rsc5_decided'broadcast: rsc5_decided'broadcast(),
subtype: S 
T,
rsc5_retry'send: rsc5_retry'send(Cmd),
sq_or: a b,
outl: outl(x),
isl: isl(x),
top: Top,
rsc5_newvote: rsc5_newvote(Cmd),
rsc5_possmajstep: rsc5_possmajstep(Cmd;cmdeq),
rsc5_Halt: rsc5_Halt(),
rsc5_decided'base: rsc5_decided'base(),
bfalse: ff,
btrue: tt,
ifthenelse: if b then t else f fi ,
or: P Q,
so_lambda: x.t[x],
exists: x:A. B[x],
cand: A c B,
rsc5_vote'base: rsc5_vote'base(Cmd),
true: True,
squash: T,
bag-member: x bs,
rev_implies: P Q,
implies: P Q,
name: Name,
prop: 
,
member: t T,
classrel: v X(e),
iff: P Q,
guard: {T},
all: x:A. B[x],
vatype: ValueAllType,
uall: [x:A]. B[x],
and: P Q,
so_apply: x[s1;s2],
pi2: snd(t),
pi1: fst(t),
sq_stable: SqStable(P),
bool: 
,
unit: Unit,
uimplies: b supposing a,
rev_uimplies: rev_uimplies(P;Q),
so_apply: x[s],
it:
Lemmas :
classrel-at,
eo-forward-forward2,
eclass_wf,
eo-forward-le,
subtype_rel_self,
subtype_rel_sets,
bind-class-rel-weak,
until-classrel,
es-le-loc,
eo-forward-no-prior-classrel,
once-classrel-weak,
eo-forward-first2,
eo-forward-loc,
send-once-loc-classrel,
sq_or_sq_or,
and_functionality_wrt_uiff,
eo-forward-base-classrel,
squash-bag-member,
assert_of_le_int,
assert_of_band,
bnot_of_lt_int,
bnot_thru_bor,
assert_functionality_wrt_uiff,
le_wf,
and_wf,
le_int_wf,
not_functionality_wrt_iff,
assert-deq-member,
assert_of_lt_int,
assert_of_bor,
iff_weakening_uiff,
and_functionality_wrt_iff,
squash_sq_or,
rsc5_main_wf,
rsc5_Replica_wf,
class-at_wf,
rsc5_Voter_wf,
rsc5_NewVoters_wf,
es-interface-subtype_rel2,
rsc5_NewRounds_wf,
bind-class_wf,
until-class_wf,
rsc5_Round_wf,
rsc5_NewRoundsState_wf,
rsc5_when_new_round_wf,
once-class_wf,
send-once-loc-class_wf,
rsc5_vote'broadcast_wf,
subtype_rel_set,
rsc5_ReplicaState_wf,
rsc5_when_new_proposal_wf,
lt_int_wf,
bor_wf,
l_member_wf,
less_than_wf,
rsc5_update_replica_wf,
rsc5_update_round_wf,
decidable__es-le,
es-le_wf,
sq_stable_from_decidable,
member-eo-forward-E,
no-classrel-in-interval_wf,
eo-forward_wf,
eo-forward-E-subtype,
Id-valueall-type,
rsc5_Proposal_wf,
rsc5_vote2prop_wf,
rsc5_propose'base_wf,
parallel-classrel-weak,
sq_or_squash3,
rsc5_RoundInfo_wf,
rsc5_vote2retry_wf,
rsc5_retry'base_wf,
parallel-class_wf,
simple-loc-comb-2-concat-classrel-weak,
exists-unit,
exists-union,
assert_of_bnot,
eqff_to_assert,
eqtt_to_assert,
uiff_transitivity,
spread_wf,
exists-product1,
pair-eta,
bag-member-append,
bag-member-map,
sq_or_squash,
squash_true,
and_true_l,
deq_wf,
rsc5_Quorum_wf,
rsc5_QuorumState_wf,
rsc5_when_quorum_wf,
concat-lifting-loc-2_wf,
simple-loc-comb-2_wf,
rsc5_notify'broadcast_wf,
rsc5_decided'broadcast_wf,
bag-append_wf,
rsc5_retry'send_wf,
bag-map_wf,
id-deq_wf,
deq-member_wf,
bnot_wf,
product-deq_wf,
band_wf,
length_wf,
rsc5_init_wf,
rsc5_add_to_quorum_wf,
Memory-class_wf,
es-loc_wf,
sq_or_wf,
pi2_wf,
make-Msg_wf,
sq_stable__valueall-type,
product-valueall-type,
int-valueall-type,
top_wf,
pi1_wf_top,
simple-loc-comb-1-concat-classrel-weak,
bag-member-empty-weak,
bag-member-single-weak,
bool_wf,
bag-member-ifthenelse,
and_false_r,
trivial-eq,
not_functionality_wrt_uiff,
safe-assert-deq,
and_functionality_wrt_uiff2,
or_functionality_wrt_iff,
ifthenelse-prop,
not_wf,
assert_wf,
iff_transitivity,
or_false_r,
equal_wf,
exists-elim,
squash_equal,
squash-classrel,
squash_and,
and_true_r,
rsc5_Halt_wf,
rsc5_decided'base_wf,
concat-lifting-loc-1_wf,
simple-loc-comb-1_wf,
empty-bag_wf,
single-bag_wf,
bag_wf,
bag-member_wf,
it_wf,
unit_wf2,
int-deq_wf,
eqof_wf,
ifthenelse_wf,
or_wf,
exists_wf,
squash_wf,
true_wf,
valueall-type_wf,
event-ordering+_wf,
event-ordering+_inc,
es-E_wf,
false_wf,
rsc5_vote'base_wf,
base-headers-msg-val_wf,
Id_wf,
Message_wf,
classrel_wf
(\mforall{}[Cmd:ValueAllType]. \mforall{}[es:EO']. \mforall{}[e:E].
\mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id
\{v \mmember{} rsc5\_vote'base(Cmd)(e) \mLeftarrow{}{}\mRightarrow{} v \mmember{} Base(``rsc5 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e)\})
\mwedge{} (\mforall{}[a:\mBbbZ{}]. \mforall{}[es:EO']. \mforall{}[e:E]. \{\mcdot{} \mmember{} rsc5\_Halt() a(e) \mLeftarrow{}{}\mRightarrow{} a \mmember{} Base(``rsc5 decided``;\mBbbZ{})(e)\})
\mwedge{} (\mforall{}[b,a:\mBbbZ{}]. \mforall{}[locs:bag(Id)]. \mforall{}[flrs,coeff:\mBbbZ{}]. \mforall{}[clients:bag(Id)]. \mforall{}[Cmd:ValueAllType].
\mforall{}[cmdeq:EqDecider(Cmd)]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}[i:Id]. \mforall{}[m:Message].
\{<i, m> \mmember{} rsc5\_Quorum(Cmd;clients;cmdeq;coeff;flrs;locs) <a, b>(e)
\mLeftarrow{}{}\mRightarrow{} \mdownarrow{}\mexists{}a1,b1:\mBbbZ{}
\mexists{}b2:Cmd
\mexists{}b3:Id
(<<<a1, b1>, b2>, b3> \mmember{} Base(``rsc5 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e)
\mwedge{} ((\mexists{}a2:\mBbbZ{}
\mexists{}b4:Cmd
(((((fst((rsc5\_possmajstep(Cmd;cmdeq) (inl <a2, b4> ) b2)))
= ((coeff * flrs) + 1))
\mwedge{} (\mdownarrow{}((m = make-Msg(``rsc5 decided``;\mBbbZ{};a1)) \mwedge{} i \mdownarrow{}\mmember{} locs)
\mvee{} ((m
= make-Msg([notify];\mBbbZ{} \mtimes{} Cmd;<a1
, snd((rsc5\_possmajstep(Cmd;cmdeq) (inl <a2, b4> ) b2))
>))
\mwedge{} i \mdownarrow{}\mmember{} clients)))
\mvee{} ((\mneg{}((fst((rsc5\_possmajstep(Cmd;cmdeq) (inl <a2, b4> ) b2)))
= ((coeff * flrs) + 1)))
\mwedge{} (i = loc(e))
\mwedge{} (m
= make-Msg(``rsc5 retry``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd;<<a1, b1 + 1>
, snd((rsc5\_possmajstep(Cmd;cmdeq) (inl <a2, b4> ) b2))
>))))
\mwedge{} (\mexists{}b5:Id List
((<inl <a2, b4> , b5> \mmember{}
Memory-class(rsc5\_add\_to\_quorum(Cmd;cmdeq)
<a, b>rsc5\_init() <inr \mcdot{} , []>rsc5\_vote'base(Cmd))(e)
\mwedge{} (||b5|| = (coeff * flrs)))
\mwedge{} (\muparrow{}(rsc5\_newvote(Cmd) <a, b> <<<a1, b1>, b2>, b3> <inl <a2, b4> , b5>))))))
\mvee{} (((((fst((rsc5\_possmajstep(Cmd;cmdeq) (inr \mcdot{} ) b2))) = ((coeff * flrs) + 1))
\mwedge{} (\mdownarrow{}((m = make-Msg(``rsc5 decided``;\mBbbZ{};a1)) \mwedge{} i \mdownarrow{}\mmember{} locs)
\mvee{} ((m
= make-Msg([notify];\mBbbZ{} \mtimes{} Cmd;<a1
, snd((rsc5\_possmajstep(Cmd;cmdeq) (inr \mcdot{} ) b2))
>))
\mwedge{} i \mdownarrow{}\mmember{} clients)))
\mvee{} ((\mneg{}((fst((rsc5\_possmajstep(Cmd;cmdeq) (inr \mcdot{} ) b2))) = ((coeff * flrs) + 1)))
\mwedge{} (i = loc(e))
\mwedge{} (m
= make-Msg(``rsc5 retry``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd;<<a1, b1 + 1>
, snd((rsc5\_possmajstep(Cmd;cmdeq) (inr \mcdot{} ) b2))
>))))
\mwedge{} (\mexists{}b4:Id List
((<inr \mcdot{} , b4> \mmember{} Memory-class(rsc5\_add\_to\_quorum(Cmd;cmdeq)
<a, b>rsc5\_init()
<inr \mcdot{} , []>rsc5\_vote'base(Cmd))(e)
\mwedge{} (||b4|| = (coeff * flrs)))
\mwedge{} (\muparrow{}(rsc5\_newvote(Cmd) <a, b> <<<a1, b1>, b2>, b3> <inr \mcdot{} , b4>)))))))\})
\mwedge{} (\mforall{}[Cmd:ValueAllType]. \mforall{}[es:EO']. \mforall{}[e:E].
\mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd
\{v \mmember{} rsc5\_RoundInfo(Cmd)(e)
\mLeftarrow{}{}\mRightarrow{} v \mmember{} Base(``rsc5 retry``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)(e)
\mdownarrow{}\mvee{} (\mexists{}a,b:\mBbbZ{}
\mexists{}b1:Cmd
((v = <<a, b>, b1>)
\mwedge{} (\mexists{}b2:Id. <<<a, b>, b1>, b2> \mmember{} Base(``rsc5 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e))))\})
\mwedge{} (\mforall{}[Cmd:ValueAllType]. \mforall{}[es:EO']. \mforall{}[e:E].
\mforall{}v:\mBbbZ{} \mtimes{} Cmd
\{v \mmember{} rsc5\_Proposal(Cmd)(e)
\mLeftarrow{}{}\mRightarrow{} v \mmember{} Base([propose];\mBbbZ{} \mtimes{} Cmd)(e)
\mdownarrow{}\mvee{} (\mexists{}a,b:\mBbbZ{}
\mexists{}b1:Cmd
((v = <a, b1>)
\mwedge{} (\mexists{}b2:Id. <<<a, b>, b1>, b2> \mmember{} Base(``rsc5 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e))))\})
\mwedge{} (\mforall{}[Cmd:ValueAllType]. \mforall{}[clients:bag(Id)]. \mforall{}[cmdeq:EqDecider(Cmd)]. \mforall{}[coeff,flrs:\mBbbZ{}].
\mforall{}[locs:bag(Id)]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}[i:Id]. \mforall{}[m:Message].
\{<i, m> \mmember{} rsc5\_main(Cmd;clients;cmdeq;coeff;flrs;locs)(e)
\mLeftarrow{}{}\mRightarrow{} loc(e) \mdownarrow{}\mmember{} locs
\mwedge{} (\mdownarrow{}\mexists{}e':\{e':E| e' \mleq{}loc e \}
\mexists{}a:\mBbbZ{}
((\mexists{}b:Cmd
((<a, b> \mmember{} Base([propose];\mBbbZ{} \mtimes{} Cmd)(e')
\mdownarrow{}\mvee{} (\mexists{}b1:\mBbbZ{}. \mexists{}b3:Id. <<<a, b1>, b>, b3> \mmember{} Base(``rsc5 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e')))
\mwedge{} ((((i \mdownarrow{}\mmember{} locs
\mwedge{} (m = make-Msg(``rsc5 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<a, 0>, b>, loc(e)>)))
\mwedge{} (e = e'))
\mvee{} ((no rsc5\_Quorum(Cmd;clients;cmdeq;coeff;flrs;locs) <a, 0> between e' and e)
\mwedge{} <i, m> \mmember{} \{rsc5\_Quorum(Cmd;clients;cmdeq;coeff;flrs;locs) <a, 0>\}(e)))
\mdownarrow{}\mvee{} ((no rsc5\_Halt() a between e' and e) \mwedge{} (\mdownarrow{}\mexists{}e1:\{e1:E| e1 \mleq{}loc ... \} . ...)))))
\mwedge{} ...))\})
Date html generated:
2012_02_20-PM-05_11_18
Last ObjectModification:
2012_02_02-PM-02_20_35
Home
Index