Nuprl Lemma : sc-retry-round1
[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)
``sc retry``.sc_Retry{mark-simple-consensus.esh:o}(Cmd) <-- ni.sc_roundout{mark-simple-consensus.esh:o}
(Cmd; eq; f)
ni@Loc|Loc,sc_Vote{mark-simple-consensus.esh:o}
(Cmd),
Prior(sc_VotesInRound{mark-simple-consensus.esh:o}
(Cmd)
ni)|)
Proof not projected
Definitions occuring in Statement :
concat-lifting-loc-2: f@Loc,
base-class-caused-by: hdr.X <-- p.Z[p],
Message: Message,
simple-loc-comb-2: F|Loc,X, Y|,
primed-class: Prior(X),
event-ordering+: EO+(Info),
Id: Id,
uall: [x:A]. B[x],
implies: P Q,
apply: f a,
product: x:A 
B[x],
cons: [car / cdr],
nil: [],
int: ,
token: "$token",
deq: EqDecider(T),
bag: bag(T),
vatype: ValueAllType
Lemmas :
eo-forward-E-subtype,
iff_wf,
rev_implies_wf,
eo-forward-forward2,
es-le-loc,
permutation_wf,
es-loc-pred,
ifthenelse_wf,
event_ordering_wf,
Error :dep-isect_wf,
es-locl_wf,
eo-forward-le,
Error :sc_Decided_wf,
Error :sc_Decision_wf,
concat-lifting-1_wf,
simple-comb-1_wf,
simple-comb-1-concat-classrel,
bool_cases,
bool_wf,
bool_subtype_base,
uiff_transitivity,
eqtt_to_assert,
assert-deq,
not_wf,
eqff_to_assert,
assert_of_bnot,
not_functionality_wrt_uiff,
int-deq_wf,
bnot_wf,
bag-member-empty-iff,
es-info-make-Msg,
sq_stable__and,
sq_stable_from_decidable,
decidable__es-le,
decidable__es-causl,
sq_stable__classrel,
true_wf,
intensional-universe_wf,
l_member_wf,
bag_qinc,
false_wf,
bag-member-map,
make-Msg_wf,
sq_stable__valueall-type,
product-valueall-type,
int-valueall-type,
pi1_wf_top,
Error :pi2_wf,
base-noloc-classrel,
subtype_base_sq,
mData_wf,
name_wf,
product_subtype_base,
list_subtype_base,
atom_subtype_base,
set_subtype_base,
assert_wf,
uiff_wf,
assert-name_eq,
Error :sc_voteMSGSto_wf,
once-class_wf,
send-once-class_wf,
once-classrel,
concat-lifting-loc-2_wf,
Id_wf,
Message_wf,
Error :sc_roundout_wf,
Error :sc_Vote_wf,
primed-class_wf,
Error :sc_VotesInRound_wf,
Error :sc_Retry_wf,
es-E_wf,
classrel_wf,
squash_wf,
es-le_wf,
es-causl_wf,
simple-loc-comb-2_wf,
eo-forward_wf,
base-class-caused-by_wf,
Error :sc_SimpleConsensus_stdma_wf,
event-ordering+_wf,
bag_wf,
deq_wf,
vatype_wf,
member_wf,
uall_wf,
sc_internal-caused,
event-ordering+_inc,
valueall-type_wf,
Error :sc_Replica_wf,
classrel-at,
es-loc_wf,
es-info_wf,
Error :sc_NewVoters_wf,
Error :sc_Voter_wf,
bind-class-rel,
Error :sc_Notify_wf,
Error :sc_NewRounds_wf,
Error :sc_Round_wf,
parallel-class_wf,
parallel-classrel,
until-class_wf,
bind-class_wf,
Error :eclass_wf,
subtype_rel_wf,
es-interface-top,
es-interface-subtype_rel2,
es-base-E_wf,
subtype_rel_self,
top_wf,
member-eo-forward-E,
until-classrel
\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{} ``sc retry``.sc\_Retry\{mark-simple-consensus.esh:o\}
(Cmd) <-- ni.sc\_roundout\{mark-simple-consensus.esh:o\}(Cmd; eq; f) ni@Loc|Loc,
sc\_Vote\{mark-simple-consensus.esh:o\}(Cmd),
Prior(sc\_VotesInRound\{mark-simple-consensus.esh:o\}(Cmd) ni)|)
Date html generated:
2012_02_20-PM-03_38_24
Last ObjectModification:
2012_02_02-PM-01_57_48
Home
Index