Nuprl Lemma : ohc_v1_quorum2_inv
es:EO'. e1:E. Cmd:ValueAllType. ni:
. z:(Cmd?) List (Id List).
(z 
ohc_v1_Quorum2State(Cmd) ni(e1) 
let cmds,z = z in no_repeats(Id;z) 
(||z|| = ||cmds||))
Proof not projected
Definitions occuring in Statement :
ohc_v1_Quorum2State: ohc_v1_Quorum2State(Cmd),
Message: Message,
classrel: v X(e),
event-ordering+: EO+(Info),
es-E: E,
Id: Id,
length: ||as||,
all: x:A. B[x],
implies: P Q,
and: P Q,
unit: Unit,
apply: f a,
spread: spread def,
product: x:A B[x],
union: left + right,
list: type List,
int: ,
equal: s = t,
no_repeats: no_repeats(T;l),
vatype: ValueAllType
Definitions :
all: x:A. B[x],
vatype: ValueAllType,
implies: P Q,
and: P Q,
length: ||as||,
ohc_v1_add_to_quorum: ohc_v1_add_to_quorum(),
ohc_v1_init: ohc_v1_init(),
prop: 
,
member: t T,
so_lambda: 
x.t[x],
cand: A c B,
squash: 
T,
true: True,
ifthenelse: if b then t else f fi ,
ohc_v1_newvote: ohc_v1_newvote(),
ohc_v1_addvote: ohc_v1_addvote(),
btrue: tt,
ycomb: Y,
not: 
A,
bfalse: ff,
unit: Unit,
ohc_v1_Quorum2State: ohc_v1_Quorum2State(Cmd),
uall: [x:A]. B[x],
sq_stable: SqStable(P),
so_apply: x[s],
bool: 
,
uimplies: b supposing a,
uiff: uiff(P;Q),
false: False,
iff: P 
Q,
guard: {T},
it: 
,
subtype: S 
T
Lemmas :
Memory-class-invariant,
Message_wf,
unit_wf2,
Id_wf,
no_repeats_wf,
length_wf,
ohc_v1_add_to_quorum_wf,
ohc_v1_init_wf,
bag_wf,
ohc_v1_vote'base_wf,
sq_stable__valueall-type,
valueall-type_wf,
sq_stable__and,
equal_wf,
sq_stable__no_repeats,
sq_stable__equal,
band_wf,
eqof_wf,
product-deq_wf,
int-deq_wf,
bnot_wf,
deq-member_wf,
id-deq_wf,
bool_wf,
eqtt_to_assert,
no_repeats_cons,
iff_transitivity,
assert_wf,
not_wf,
l_member_wf,
iff_weakening_uiff,
assert_of_band,
and_functionality_wrt_iff,
safe-assert-deq,
assert_of_bnot,
not_functionality_wrt_iff,
assert-deq-member,
uiff_transitivity,
eqff_to_assert,
es-locl_wf,
event-ordering+_inc,
bag-member-single,
no_repeats_nil,
bag-member_wf,
single-bag_wf,
classrel_wf,
ohc_v1_Quorum2State_wf,
es-E_wf,
event-ordering+_wf
\mforall{}es:EO'. \mforall{}e1:E. \mforall{}Cmd:ValueAllType. \mforall{}ni:\mBbbZ{} \mtimes{} \mBbbZ{}. \mforall{}z:(Cmd?) List \mtimes{} (Id List).
(z \mmember{} ohc\_v1\_Quorum2State(Cmd) ni(e1) {}\mRightarrow{} let cmds,z = z in no\_repeats(Id;z) \mwedge{} (||z|| = ||cmds||))
Date html generated:
2012_02_20-PM-05_23_19
Last ObjectModification:
2012_02_13-PM-01_05_00
Home
Index