Nuprl Lemma : RSC_validity_property
[Cmd:ValueAllType]. [eq:EqDecider(Cmd)]. [locs,clients:bag(Id)]. [f:
]. [es:EO'].
((RSC_stdma{i:l}(Cmd;clients;eq;f;locs) es) 
RSC_validity(Cmd;es))
Proof not projected
Definitions occuring in Statement :
RSC_validity: RSC_validity(Cmd;es),
RSC_stdma: RSC_stdma{i:l}(Cmd;clients;cmdeq;flrs;locs),
Message: Message,
event-ordering+: EO+(Info),
Id: Id,
uall: [x:A]. B[x],
implies: P Q,
apply: f a,
int: ,
deq: EqDecider(T),
bag: bag(T),
vatype: ValueAllType
Definitions :
uall: [x:A]. B[x],
vatype: ValueAllType,
implies: P Q,
RSC_validity: RSC_validity(Cmd;es),
member: t 
T,
all: x:A. B[x],
and: P 
Q,
squash: 
T,
exists: 
x:A. B[x],
nat: 
,
ge: i 
j ,
le: A 
B,
not: 
A,
false: False,
prop: 
,
true: True,
RSC_headers_no_inputs: Error :RSC_headers_no_inputs,
es-header: es-header(es;e),
name: Name,
so_lambda: 
x.t[x],
select: l[i],
int_seg: {i..j
},
length: ||as||,
ycomb: Y,
lelt: i j < k,
ifthenelse: if b then t else f fi ,
le_int: i z j,
bnot: 
b,
lt_int: i <z j,
btrue: tt,
bfalse: ff,
RSC_Vote: Error :RSC_Vote,
pi1: fst(t),
top: Top,
subtype: S 
T,
cand: A c B,
pi2: snd(t),
RSC_Propose: Error :RSC_Propose,
label: ...$L... t,
or: P 
Q,
es-causle: e c e',
uiff: uiff(P;Q),
RSC_stdma: Error :RSC_stdma,
RSC_Decided: Error :RSC_Decided,
RSC_Retry: Error :RSC_Retry,
strongwellfounded: SWellFounded(R[x; y]),
message-constraint: message-constraint{i:l}(es;X;hdrs),
std-ma: StandardMessageAutomaton(X;hdrs),
uimplies: b supposing a,
so_apply: x[s],
sq_stable: SqStable(P),
sq_or: a b,
iff: P 
Q,
sq_type: SQType(T),
guard: {T},
l_member: (x l),
es-p-local-pred: es-p-local-pred(es;P),
classrel: v X(e),
bag-member: x bs,
msg-header: msg-header(m),
!hyp_hide: x
Lemmas :
es-causl-swellfnd,
event-ordering+_inc,
nat_properties,
ge_wf,
nat_wf,
le_wf,
es-causl_wf,
base-noloc-classrel-make-Msg,
product-valueall-type,
int-valueall-type,
sq_stable__valueall-type,
valueall-type_wf,
select_member,
name_wf,
l_member_wf,
msg-header_wf,
Error :RSC_headers_no_inputs_wf,
squash_wf,
classrel_wf,
Id_wf,
Error :RSC_main_wf,
es-loc_wf,
Error :RSC_Decided_wf,
Id-valueall-type,
Error :RSC_Vote_wf,
Error :RSC_Retry_wf,
es-E_wf,
Error :RSC_stdma_wf,
Message_wf,
event-ordering+_wf,
bag_wf,
deq_wf,
RSC_decided,
poss-maj-unanimous,
pair-eta,
poss-maj_wf,
subtype_base_sq,
int_subtype_base,
l_all_cons,
es-causl_transitivity2,
es-causle_weakening,
Error :RSC_Propose_wf,
non_neg_length,
length_wf_nat,
top_wf,
length_wf,
RSC_vote,
product-wf,
base-headers-msg-val_wf,
RSC_retry,
poss-maj-member,
cons_member,
true_wf,
primed-class-opt-classrel,
Error :RSC_VotesInRound_wf,
single-bag_wf,
eo-forward_wf,
member-eo-forward-E,
sq_stable_from_decidable,
es-le_wf,
decidable__es-le,
RSC_VotesInRound-inv,
eo-forward-E-subtype,
select_wf,
eo-forward-base-classrel,
eo-forward-le,
eo-forward-locl,
es-causle_weakening_locl,
es-causl_weakening,
es-causl_transitivity1,
decidable__es-causl,
sq_stable__equal,
bag-member-single,
pi1_wf_top,
Error :pi2_wf,
member_wf,
nil_member
\mforall{}[Cmd:ValueAllType]. \mforall{}[eq:EqDecider(Cmd)]. \mforall{}[locs,clients:bag(Id)]. \mforall{}[f:\mBbbZ{}]. \mforall{}[es:EO'].
((RSC\_stdma\{i:l\}(Cmd;clients;eq;f;locs) es) {}\mRightarrow{} RSC\_validity(Cmd;es))
Date html generated:
2012_02_20-PM-04_04_49
Last ObjectModification:
2012_02_02-PM-01_59_54
Home
Index