Nuprl Lemma : sc-retry-round
[Cmd:ValueAllType]. [eq:EqDecider(Cmd)]. [locs,clients:bag(Id)]. [f:
]. [es:EO'].
((sc_SimpleConsensus_stdma{mark-simple-consensus.esh:o, i:l}(Cmd; clients; eq; f; locs) es)
(e':E. v: 
Cmd.
(v 
sc_Retry{mark-simple-consensus.esh:o}(Cmd)(e')
(
e,start:E
(start 
loc e
(n,i:
c:Cmd
cmds:Cmd List
((e <loc e')
(<<n, i>, c> sc_Vote{mark-simple-consensus.esh:o}(Cmd)(e)
cmds Prior(sc_VotesInRound{mark-simple-consensus.esh:o}(Cmd) <n, i>)(e)
(||cmds|| = (2 * f))
(
((fst(poss-maj(eq;[c / cmds];c))) = ((2 * f) + 1))))
(v = <<n, i + 1>, snd(poss-maj(eq;[c / cmds];c))>))))))))
Proof not projected
Definitions occuring in Statement :
Message: Message,
primed-class: Prior(X),
classrel: v X(e),
eo-forward: eo.e,
event-ordering+: EO+(Info),
es-le: e loc e' ,
es-locl: (e <loc e'),
es-E: E,
Id: Id,
length: ||as||,
uall: [x:A]. B[x],
pi1: fst(t),
pi2: snd(t),
all: x:A. B[x],
exists: x:A. B[x],
not: A,
squash: T,
implies: P Q,
and: P Q,
apply: f a,
pair: <a, b>,
product: x:A B[x],
cons: [car / cdr],
list: type List,
multiply: n * m,
add: n + m,
natural_number: $n,
int: ,
equal: s = t,
poss-maj: poss-maj(eq;L;x),
deq: EqDecider(T),
bag: bag(T),
vatype: ValueAllType
Lemmas :
int_subtype_base,
es-base-E_wf,
subtype_rel_self,
intensional-universe_wf,
l_member_wf,
true_wf,
bag_qinc,
Error :eclass_wf,
es-interface-top,
eo-forward-loc,
false_wf,
es-causl_wf,
sq_stable__and,
sq_stable_from_decidable,
decidable__es-locl,
sq_stable__classrel,
sq_stable__equal,
sq_stable__not,
Message_wf,
Error :sc_SimpleConsensus_stdma_wf,
es-E_wf,
classrel_wf,
Error :sc_Retry_wf,
squash_wf,
es-le_wf,
es-locl_wf,
Error :sc_Vote_wf,
eo-forward_wf,
primed-class_wf,
Error :sc_VotesInRound_wf,
not_wf,
vatype_wf,
uall_wf,
deq_wf,
bag_wf,
Id_wf,
event-ordering+_wf,
sc-retry-round1,
member_wf,
event-ordering+_inc,
simple-loc-comb-2-concat-classrel,
Error :sc_roundout_wf,
subtype_rel_wf,
member-eo-forward-E,
es-loc_wf,
make-Msg_wf,
valueall-type_wf,
product-valueall-type,
int-valueall-type,
sq_stable__valueall-type,
bool_cases,
bool_wf,
subtype_base_sq,
bool_subtype_base,
uiff_transitivity,
eqtt_to_assert,
assert_wf,
assert_of_band,
and_functionality_wrt_uiff,
assert-deq,
eqff_to_assert,
assert_functionality_wrt_uiff,
bnot_thru_band,
assert_of_bor,
or_functionality_wrt_uiff,
assert_of_bnot,
not_functionality_wrt_uiff,
band_wf,
product-deq_wf,
int-deq_wf,
length_wf,
bor_wf,
bnot_wf,
decidable_wf,
decidable__assert,
pair-eta,
poss-maj_wf,
nat_wf,
top_wf,
pi1_wf_top,
length_wf_nat,
bag-member-single,
Error :pi1_wf,
Error :sc_dcdMSGto_wf,
Error :pi2_wf,
Error :sc_retryMSGto_wf,
bag-member-empty-iff,
mData_wf,
name_wf,
uiff_wf,
assert-name_eq
\mforall{}[Cmd:ValueAllType]. \mforall{}[eq:EqDecider(Cmd)]. \mforall{}[locs,clients:bag(Id)]. \mforall{}[f:\mBbbZ{}]. \mforall{}[es:EO'].
((sc\_SimpleConsensus\_stdma\{mark-simple-consensus.esh:o, i:l\}(Cmd; clients; eq; f; locs) es)
{}\mRightarrow{} (\mforall{}e':E. \mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd.
(v \mmember{} sc\_Retry\{mark-simple-consensus.esh:o\}(Cmd)(e')
{}\mRightarrow{} (\mdownarrow{}\mexists{}e,start:E
(start \mleq{}loc e
\mwedge{} (\mexists{}n,i:\mBbbZ{}
\mexists{}c:Cmd
\mexists{}cmds:Cmd List
((e <loc e')
\mwedge{} (<<n, i>, c> \mmember{} sc\_Vote\{mark-simple-consensus.esh:o\}(Cmd)(e)
\mwedge{} cmds \mmember{} Prior(sc\_VotesInRound\{mark-simple-consensus.esh:o\}(Cmd) <n, i>)(e)
\mwedge{} (||cmds|| = (2 * f))
\mwedge{} (\mneg{}((fst(poss-maj(eq;[c / cmds];c))) = ((2 * f) + 1))))
\mwedge{} (v = <<n, i + 1>, snd(poss-maj(eq;[c / cmds];c))>))))))))
Date html generated:
2012_02_20-PM-03_38_34
Last ObjectModification:
2012_02_02-PM-01_57_50
Home
Index