Nuprl Lemma : RSC_Voter_nlp
Cmd:ValueAllType. clients:bag(Id). cmdeq:EqDecider(Cmd). flrs:
. locs:bag(Id). x0: 
Cmd.
NormalLProgrammable'(Id Message;RSC_Voter(Cmd;clients;cmdeq;flrs;locs) x0)
Proof not projected
Definitions occuring in Statement :
RSC_Voter: RSC_Voter(Cmd;clients;cmdeq;flrs;locs),
Message: Message,
normal-locally-programmable: NormalLProgrammable(A;X),
Id: Id,
all: x:A. B[x],
apply: f a,
product: x:A B[x],
int: ,
deq: EqDecider(T),
bag: bag(T),
vatype: ValueAllType
Definitions :
all: x:A. B[x],
vatype: ValueAllType,
RSC_Voter: RSC_Voter(Cmd;clients;cmdeq;flrs;locs),
member: t 
T,
so_lambda: 
x.t[x],
top: Top,
label: ...$L... t,
subtype: S 
T,
suptype: suptype(S; T),
squash: 
T,
true: True,
uall: [x:A]. B[x],
implies: P 
Q,
so_apply: x[s],
uimplies: b supposing a,
sq_stable: SqStable(P)
Lemmas :
parallel-class-nlp,
Id_wf,
Message_wf,
product-valueall-type,
Id-valueall-type,
Message-valueall-type,
valueall-type_wf,
parallel-class_wf,
RSC_Round_wf,
RSC_Notify_wf,
until-class_wf,
bind-class_wf,
RSC_NewRounds_wf,
Error :apply_wf,
eclass_wf2,
top_wf,
es-interface-subtype_rel,
RSC_Round_nlp,
RSC_Notify_nlp,
until-class-nlp,
bind-class-nlp,
int-valueall-type,
sq_stable__valueall-type,
RSC_NewRounds_nlp,
bag_wf,
deq_wf,
vatype_wf
\mforall{}Cmd:ValueAllType. \mforall{}clients:bag(Id). \mforall{}cmdeq:EqDecider(Cmd). \mforall{}flrs:\mBbbZ{}. \mforall{}locs:bag(Id). \mforall{}x0:\mBbbZ{} \mtimes{} Cmd.
NormalLProgrammable'(Id \mtimes{} Message;RSC\_Voter(Cmd;clients;cmdeq;flrs;locs) x0)
Date html generated:
2012_02_20-PM-03_59_59
Last ObjectModification:
2012_02_02-PM-01_58_43
Home
Index