Nuprl Lemma : RSC_ReplicaState-prop1
[Cmd:ValueAllType]. [eq:EqDecider(Cmd)]. [locs,clients:bag(Id)]. [f:
]. [es:EO'].
e:E. max:. missing: List.
(<max, missing> 
RSC_ReplicaState(Cmd)(e) 
((max 
0 ) 
(xmissing.(0 < x) (x < max))))
Proof not projected
Definitions occuring in Statement :
RSC_ReplicaState: RSC_ReplicaState(Cmd),
Message: Message,
classrel: v X(e),
event-ordering+: EO+(Info),
es-E: E,
Id: Id,
uall: [x:A]. B[x],
ge: i j ,
all: x:A. B[x],
implies: P Q,
and: P Q,
less_than: a < b,
pair: <a, b>,
product: x:A 
B[x],
list: type List,
natural_number: $n,
int: ,
l_all: (xL.P[x]),
deq: EqDecider(T),
bag: bag(T),
vatype: ValueAllType
Definitions :
false: False,
not: 
A,
le: A 
B,
l_all: (xL.P[x]),
uall: [x:A]. B[x],
ycomb: Y,
so_lambda: 
x y.t[x; y],
subtype: S 
T,
top: Top,
cand: A c B,
so_lambda: x.t[x],
prop: 
,
true: True,
member: t T,
list_accum: list_accum(x,a.f[x; a];y;l),
squash: 
T,
ge: i j ,
and: P Q,
implies: P Q,
all: x:A. B[x],
vatype: ValueAllType,
guard: {T},
RSC_onpropose: Error :RSC_onpropose,
bfalse: ff,
btrue: tt,
ifthenelse: if b then t else f fi ,
so_apply: x[s1;s2],
so_apply: x[s],
sq_stable: SqStable(P),
sq_or: a 
b,
exists: 
x:A. B[x],
iff: P 
Q,
uimplies: b supposing a,
sq_type: SQType(T),
pi2: snd(t),
pi1: fst(t),
uiff: uiff(P;Q),
unit: Unit,
bool: 
,
rev_implies: P Q,
it: 
Lemmas :
deq_wf,
Id_wf,
bag_wf,
event-ordering+_wf,
event-ordering+_inc,
es-E_wf,
Error :RSC_ReplicaState_wf,
Message_wf,
classrel_wf,
append_wf,
pi1_wf_top,
top_wf,
map_wf,
list_accum_append,
decidable__lt,
decidable__cand,
decidable__l_all-better-extract,
decidable__le,
le_wf,
sq_stable_from_decidable,
l_member_wf,
l_all_wf2,
ge_wf,
sq_stable__and,
valueall-type_wf,
sq_stable__valueall-type,
RSC-ilf,
guard_wf,
int-deq_wf,
list-diff_wf,
from-upto_wf,
lt_int_wf,
ifthenelse_wf,
list_accum_invariant,
l_all_nil,
int_subtype_base,
list_subtype_base,
subtype_base_sq,
Error :pi2_wf,
assert_of_le_int,
bnot_of_lt_int,
assert_functionality_wrt_uiff,
eqff_to_assert,
bnot_wf,
le_int_wf,
assert_of_lt_int,
eqtt_to_assert,
assert_wf,
uiff_transitivity,
bool_wf,
l_all_append,
from-upto-member,
member-list-diff
\mforall{}[Cmd:ValueAllType]. \mforall{}[eq:EqDecider(Cmd)]. \mforall{}[locs,clients:bag(Id)]. \mforall{}[f:\mBbbZ{}]. \mforall{}[es:EO'].
\mforall{}e:E. \mforall{}max:\mBbbZ{}. \mforall{}missing:\mBbbZ{} List.
(<max, missing> \mmember{} RSC\_ReplicaState(Cmd)(e) {}\mRightarrow{} ((max \mgeq{} 0 ) \mwedge{} (\mforall{}x\mmember{}missing.(0 < x) \mwedge{} (x < max))))
Date html generated:
2012_02_20-PM-04_02_25
Last ObjectModification:
2012_02_02-PM-01_59_36
Home
Index