Nuprl Lemma : sc-vote+1-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. n:. i:{i:| i > 0} . c:Cmd.
(<<n, i>, c> 
sc_Vote{mark-simple-consensus.esh:o}(Cmd)(e')
(
e:E. ((e < e') 
<<n, i>, c> sc_Retry{mark-simple-consensus.esh:o}(Cmd)(e))))))
Proof not projected
Definitions occuring in Statement :
Message: Message,
classrel: v X(e),
event-ordering+: EO+(Info),
es-causl: (e < e'),
es-E: E,
Id: Id,
uall: [x:A]. B[x],
gt: i > j,
all: x:A. B[x],
exists: x:A. B[x],
squash: T,
implies: P Q,
and: P Q,
set: {x:A| B[x]} ,
apply: f a,
pair: <a, b>,
product: x:A 
B[x],
natural_number: $n,
int: ,
deq: EqDecider(T),
bag: bag(T),
vatype: ValueAllType
Lemmas :
int_subtype_base,
Error :sc_Retry_wf,
Error :sc_NewRound_wf,
eo-forward-E-member,
es-causl_wf,
eo-forward-le,
es-causle_weakening_locl,
es-causl_transitivity1,
sq_stable__classrel,
eo-forward-base-classrel,
base-headers-msg-val_wf,
simple-loc-comb-2-concat-classrel,
bool_cases,
bool_subtype_base,
uiff_transitivity,
eqtt_to_assert,
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,
length_wf_nat,
bag-member-single,
Error :sc_dcdMSGto_wf,
Error :pi1_wf,
Error :sc_retryMSGto_wf,
bag-member-empty-iff,
send-once-classrel,
bag-member-map,
make-Msg_wf,
sq_stable__valueall-type,
product-valueall-type,
int-valueall-type,
pi1_wf_top,
Error :pi2_wf,
mData_wf,
product_subtype_base,
set_subtype_base,
assert_wf,
uiff_wf,
assert-name_eq,
iff_wf,
rev_implies_wf,
squash_wf,
msg-body_wf2,
msg-has-type_wf,
ifthenelse_wf,
true_wf,
rational-has-value,
int_nzero_wf,
b-union_wf,
bool_wf,
rationals_wf,
int-rational,
btrue_wf,
bfalse_wf,
tunion_wf,
Id-has-valueall,
type-valueall-type,
eq_term_wf,
unit_wf,
subtype_rel_wf,
name_wf,
member_wf,
base-noloc-classrel,
nat_wf,
l_member_wf,
valueall-type_wf,
deq_wf,
Id_wf,
bag_wf,
Message_wf,
event-ordering+_wf,
vatype_wf,
Error :sc_SimpleConsensus_stdma_wf,
event-ordering+_inc,
es-E_wf,
gt_wf,
Error :sc_Vote_wf,
classrel_wf,
subtype_base_sq,
list_subtype_base,
atom_subtype_base,
select_member,
le_wf,
not_wf,
false_wf,
Error :sc_Replica_wf,
classrel-at,
es-loc_wf,
es-info_wf,
Error :sc_NewVoters_wf,
Error :sc_Voter_wf,
bind-class-rel,
eo-forward_wf,
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,
es-interface-top,
es-interface-subtype_rel2,
es-base-E_wf,
subtype_rel_self,
top_wf,
member-eo-forward-E,
Error :sc_VotesInRound_wf,
primed-class_wf,
Error :sc_roundout_wf,
concat-lifting-loc-2_wf,
simple-loc-comb-2_wf,
once-class_wf,
Error :sc_voteMSGSto_wf,
send-once-class_wf,
once-classrel,
Error :sc_Decided_wf,
Error :sc_Decision_wf,
concat-lifting-1_wf,
simple-comb-1_wf,
simple-comb-1-concat-classrel,
until-classrel,
es-le_wf,
intensional-universe_wf
\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{}n:\mBbbZ{}. \mforall{}i:\{i:\mBbbZ{}| i > 0\} . \mforall{}c:Cmd.
(<<n, i>, c> \mmember{} sc\_Vote\{mark-simple-consensus.esh:o\}(Cmd)(e')
{}\mRightarrow{} (\mdownarrow{}\mexists{}e:E. ((e < e') \mwedge{} <<n, i>, c> \mmember{} sc\_Retry\{mark-simple-consensus.esh:o\}(Cmd)(e))))))
Date html generated:
2012_02_20-PM-03_38_39
Last ObjectModification:
2012_02_02-PM-01_57_50
Home
Index