Nuprl Lemma : RSC_ReplicaState_wf
[Cmd:ValueAllType]. (RSC_ReplicaState(Cmd) 
EClass'(
( List)))
Proof not projected
Definitions occuring in Statement :
RSC_ReplicaState: RSC_ReplicaState(Cmd),
Message: Message,
eclass: EClass(A[eo; e]),
uall: [x:A]. B[x],
member: t T,
product: x:A B[x],
list: type List,
int: ,
vatype: ValueAllType
Definitions :
uall: [x:A]. B[x],
member: t T,
RSC_ReplicaState: RSC_ReplicaState(Cmd),
vatype: ValueAllType,
uimplies: b supposing a
Lemmas :
vatype_wf,
bool_wf,
Id_wf,
bag_wf,
subtype_rel_function,
subtype_rel_self,
subtype_rel_bag,
subtype_rel_simple_product,
Accum-class_wf,
ifthenelse_wf,
Error :apply_wf,
RSC_new_proposal_wf,
RSC_onnewpropose_wf,
RSC_init_wf,
pair_wf,
nil_wf,
RSC_Proposal_wf
\mforall{}[Cmd:ValueAllType]. (RSC\_ReplicaState(Cmd) \mmember{} EClass'(\mBbbZ{} \mtimes{} (\mBbbZ{} List)))
Date html generated:
2012_02_20-PM-04_01_37
Last ObjectModification:
2012_02_02-PM-01_59_23
Home
Index