Nuprl Lemma : sc_internal-caused
[Cmd:ValueAllType]. [clients:bag(Id)]. [cmdeq:EqDecider(Cmd)]. [flrs:
]. [locs:bag(Id)]. [es:EO'].
((sc_SimpleConsensus_stdma{mark-simple-consensus.esh:o, i:l}(Cmd; clients; cmdeq; flrs; locs) es)
{sc_Decided{mark-simple-consensus.esh:o}(Cmd) <-- sc_Replica{mark-simple-consensus.esh:o}(Cmd;
clients;
cmdeq;
flrs;
locs)@locs
sc_Retry{mark-simple-consensus.esh:o}(Cmd) <-- sc_Replica{mark-simple-consensus.esh:o}(Cmd;
clients;
cmdeq;
flrs;
locs)@locs
sc_Vote{mark-simple-consensus.esh:o}(Cmd) <-- sc_Replica{mark-simple-consensus.esh:o}(Cmd;
clients;
cmdeq;
flrs;
locs)@locs})
Proof not projected
Definitions occuring in Statement :
class-caused-by: X <-- Z,
Message: Message,
class-at: X@locs,
event-ordering+: EO+(Info),
Id: Id,
uall: [x:A]. B[x],
guard: {T},
implies: P Q,
and: P Q,
apply: f a,
product: x:A 
B[x],
int: ,
deq: EqDecider(T),
bag: bag(T),
vatype: ValueAllType
Lemmas :
cons_member,
l_member_subtype,
es-header_wf,
nat_wf,
decidable__equal_name,
decidable__l_member,
sq_stable_from_decidable,
l_member_wf,
subtype_rel_wf,
name_wf,
base-noloc-classrel,
event-ordering+_inc,
member_wf,
Error :sc_Vote_wf,
vatype_wf,
deq_wf,
bag_wf,
event-ordering+_wf,
Error :sc_SimpleConsensus_stdma_wf,
class-caused-by_wf,
class-at_wf,
es-causl_wf,
squash_wf,
Error :sc_Decided_wf,
classrel_wf,
es-E_wf,
Error :sc_Retry_wf,
Error :sc_Replica_wf,
Id_wf,
Message_wf,
atom_subtype_base,
list_subtype_base,
subtype_base_sq
\mforall{}[Cmd:ValueAllType]. \mforall{}[clients:bag(Id)]. \mforall{}[cmdeq:EqDecider(Cmd)]. \mforall{}[flrs:\mBbbZ{}]. \mforall{}[locs:bag(Id)].
\mforall{}[es:EO'].
((sc\_SimpleConsensus\_stdma\{mark-simple-consensus.esh:o, i:l\}(Cmd; clients; cmdeq; flrs; locs) es)
{}\mRightarrow{} \{sc\_Decided\{mark-simple-consensus.esh:o\}(Cmd) <-- sc\_Replica\{mark-simple-consensus.esh:o\}
(Cmd; clients; cmdeq; flrs; locs)@locs
\mwedge{} sc\_Retry\{mark-simple-consensus.esh:o\}(Cmd) <-- sc\_Replica\{mark-simple-consensus.esh:o\}
(Cmd; clients; cmdeq; flrs; locs)@locs
\mwedge{} sc\_Vote\{mark-simple-consensus.esh:o\}(Cmd) <-- sc\_Replica\{mark-simple-consensus.esh:o\}
(Cmd; clients; cmdeq; flrs; locs)@locs\})
Date html generated:
2012_02_20-PM-03_38_16
Last ObjectModification:
2012_02_02-PM-01_57_46
Home
Index