Nuprl Lemma : RSC_ReplicaState-prop2
[Cmd:ValueAllType]. [eq:EqDecider(Cmd)]. [locs,clients:bag(Id)]. [f:
]. [es:EO'].
e1,e2:E. max1,max2:. missing1,missing2: List.
(<max1, missing1> 
RSC_ReplicaState(Cmd)(e1)
<max2, missing2> RSC_ReplicaState(Cmd)(e2)
(e1 <loc e2)
((max2 
max1 ) 
(xmissing2.(x missing1) 
(x > max1))))
Proof not projected
Definitions occuring in Statement :
RSC_ReplicaState: RSC_ReplicaState(Cmd),
Message: Message,
classrel: v X(e),
event-ordering+: EO+(Info),
es-locl: (e <loc e'),
es-E: E,
Id: Id,
uall: [x:A]. B[x],
gt: i > j,
ge: i j ,
all: x:A. B[x],
implies: P Q,
or: P Q,
and: P Q,
pair: <a, b>,
product: x:A 
B[x],
list: type List,
int: ,
l_all: (xL.P[x]),
l_member: (x l),
deq: EqDecider(T),
bag: bag(T),
vatype: ValueAllType
Definitions :
uall: [x:A]. B[x],
vatype: ValueAllType,
all: x:A. B[x],
implies: P Q,
ge: i j ,
or: P Q,
gt: i > j,
squash: 
T,
list_accum: list_accum(x,a.f[x; a];y;l),
member: t T,
true: True,
prop: 
,
so_lambda: 
x.t[x],
top: Top,
so_lambda: x y.t[x; y],
ycomb: Y,
map: map(f;as),
pi1: fst(t),
subtype: S 
T,
exists: 
x:A. B[x],
and: P Q,
name: Name,
cand: A c B,
sq_or: a b,
guard: {T},
iff: P 
Q,
rev_implies: P Q,
l_all: (xL.P[x]),
pi2: snd(t),
le: A 
B,
not: 
A,
false: False,
RSC_onpropose: Error :RSC_onpropose,
ifthenelse: if b then t else f fi ,
btrue: tt,
bfalse: ff,
sq_stable: SqStable(P),
so_apply: x[s],
so_apply: x[s1;s2],
iseg: l1 l2,
sq_type: SQType(T),
uimplies: b supposing a,
bool: 
,
unit: Unit,
uiff: uiff(P;Q),
it: 
Lemmas :
RSC-ilf,
sq_stable__valueall-type,
valueall-type_wf,
sq_stable__and,
ge_wf,
l_all_wf2,
l_member_wf,
gt_wf,
sq_stable_from_decidable,
le_wf,
decidable__le,
decidable__l_all-better-extract,
decidable__or,
decidable__l_member,
decidable__equal_int,
decidable__lt,
list_accum_append,
map_wf,
es-E_wf,
event-ordering+_inc,
Message_wf,
top_wf,
es-locl_wf,
classrel_wf,
Error :RSC_ReplicaState_wf,
event-ordering+_wf,
bag_wf,
Id_wf,
deq_wf,
map_append_sq,
iseg_map,
pi1_wf_top,
append_wf,
prior-classrel-list-append,
Error :RSC_Proposal_wf,
RSC_Proposal-single-val,
sq_stable__sq_or,
base-headers-msg-val_wf,
iseg_wf,
list_accum_wf,
Error :RSC_onpropose_wf,
length_wf_nat,
nat_wf,
squash_wf,
true_wf,
subtype_base_sq,
product_subtype_base,
int_subtype_base,
list_subtype_base,
member_wf,
append_assoc,
list_accum_invariant,
guard_wf,
Error :pi2_wf,
lt_int_wf,
bool_wf,
uiff_transitivity,
assert_wf,
eqtt_to_assert,
assert_of_lt_int,
le_int_wf,
bnot_wf,
eqff_to_assert,
assert_functionality_wrt_uiff,
bnot_of_lt_int,
assert_of_le_int,
l_all_append,
from-upto_wf,
from-upto-member,
member-list-diff,
int-deq_wf,
list-diff_wf
\mforall{}[Cmd:ValueAllType]. \mforall{}[eq:EqDecider(Cmd)]. \mforall{}[locs,clients:bag(Id)]. \mforall{}[f:\mBbbZ{}]. \mforall{}[es:EO'].
\mforall{}e1,e2:E. \mforall{}max1,max2:\mBbbZ{}. \mforall{}missing1,missing2:\mBbbZ{} List.
(<max1, missing1> \mmember{} RSC\_ReplicaState(Cmd)(e1)
{}\mRightarrow{} <max2, missing2> \mmember{} RSC\_ReplicaState(Cmd)(e2)
{}\mRightarrow{} (e1 <loc e2)
{}\mRightarrow{} ((max2 \mgeq{} max1 ) \mwedge{} (\mforall{}x\mmember{}missing2.(x \mmember{} missing1) \mvee{} (x > max1))))
Date html generated:
2012_02_20-PM-04_02_35
Last ObjectModification:
2012_02_02-PM-01_59_37
Home
Index