Nuprl Lemma : ohc_v1-ilf-quorum2
HIDDEN
Proof not projected
Definitions occuring in Statement :
ohc_v1_Quorum2: ohc_v1_Quorum2(Cmd;cmdeq;flrs;learners;locs),
ohc_v1_prune_off_units: ohc_v1_prune_off_units(Cmd),
ohc_v1_add_to_quorum: ohc_v1_add_to_quorum(),
ohc_v1_newvote: ohc_v1_newvote(),
ohc_v1_init: ohc_v1_init(),
ohc_v1_vote'base: ohc_v1_vote'base(Cmd),
Memory-class: Memory-class(f;init;X),
make-Msg: make-Msg(hdr;typ;val),
base-headers-msg-val: Base(hdr;typ),
Message: Message,
classrel: v 
X(e),
event-ordering+: EO+(Info),
es-loc: loc(e),
es-E: E,
Id: Id,
length: ||as||,
assert: 
b,
it: 
,
uall: 
[x:A]. B[x],
guard: {T},
pi1: fst(t),
pi2: snd(t),
exists: 
x:A. B[x],
iff: P 
Q,
not: 
A,
squash: 
T,
or: P 
Q,
and: P 
Q,
unit: Unit,
set: {x:A| B[x]} ,
apply: f a,
pair: <a, b>,
product: x:A 
B[x],
inr: inr x ,
inl: inl x ,
union: left + right,
cons: [car / cdr],
nil: [],
list: type List,
add: n + m,
natural_number: $n,
int: 
,
token: "$token",
universe: Type,
equal: s = t,
hide: HIDDEN,
poss-maj: poss-maj(eq;L;x),
deq: EqDecider(T),
bag-member: x bs,
bag: bag(T),
valueall-type: valueall-type(T)
Definitions :
hide: HIDDEN,
uall: [x:A]. B[x],
guard: {T},
iff: P Q,
classrel: v X(e),
squash: T,
exists: x:A. B[x],
or: P Q,
and: P Q,
bag-member: x bs,
ohc_v1_newvote: ohc_v1_newvote(),
member: t T,
let: let,
all: x:A. B[x],
prop: 
,
name: Name,
cand: A c B,
implies: P Q,
rev_implies: P Q,
top: Top,
vatype: ValueAllType,
subtype: S 
T,
true: True,
so_lambda: 
x.t[x],
sq_or: a b,
ohc_v1_retry'send: ohc_v1_retry'send(Cmd),
nequal: a 
b T ,
ifthenelse: if b then t else f fi ,
ohc_v1_notify'broadcast: ohc_v1_notify'broadcast(Cmd),
ohc_v1_decided'broadcast: ohc_v1_decided'broadcast(),
btrue: tt,
bfalse: ff,
exposed-bfalse: exposed-bfalse,
ohc_v1_roundout2: ohc_v1_roundout2(Cmd;cmdeq;flrs;learners;locs),
ohc_v1_vote'base: ohc_v1_vote'base(Cmd),
ohc_v1_when_quorum2: ohc_v1_when_quorum2(Cmd;cmdeq;flrs;learners;locs),
ohc_v1_Quorum2State: ohc_v1_Quorum2State(Cmd),
ohc_v1_Quorum2: ohc_v1_Quorum2(Cmd;cmdeq;flrs;learners;locs),
nat: 
,
so_apply: x[s],
sq_stable: SqStable(P),
rev_uimplies: rev_uimplies(P;Q),
uiff: uiff(P;Q),
uimplies: b supposing a,
not: A,
false: False,
pi1: fst(t),
pi2: snd(t),
unit: Unit,
bool: 
,
it:
Lemmas :
false_wf,
classrel_wf,
Message_wf,
unit_wf2,
Id_wf,
base-headers-msg-val_wf,
length_wf,
pi1_wf_top,
poss-maj_wf,
ohc_v1_prune_off_units_wf,
nat_wf,
product-valueall-type,
int-valueall-type,
valueall-type_wf,
sq_stable__valueall-type,
squash_wf,
or_wf,
make-Msg_wf,
pi2_wf,
bag-member_wf,
true_wf,
sq_or_wf,
exists_wf,
not_wf,
equal_wf,
es-loc_wf,
event-ordering+_inc,
ifthenelse_wf,
eq_int_wf,
bag-map_wf,
null_wf3,
top_wf,
ohc_v1_retry'send_wf,
bag_wf,
bag-append_wf,
ohc_v1_notify'broadcast_wf,
ohc_v1_decided'broadcast_wf,
single-bag_wf,
Memory-class_wf,
ohc_v1_add_to_quorum_wf,
ohc_v1_init_wf,
ohc_v1_vote'base_wf,
assert_wf,
band_wf,
eqof_wf,
product-deq_wf,
int-deq_wf,
bnot_wf,
deq-member_wf,
id-deq_wf,
let_wf,
empty-bag_wf,
it_wf,
ohc_v1_roundout2_wf,
simple-loc-comb-2_wf,
concat-lifting-loc-2_wf,
ohc_v1_when_quorum2_wf,
ohc_v1_Quorum2State_wf,
ohc_v1_Quorum2_wf,
es-E_wf,
event-ordering+_wf,
deq_wf,
and_true_l,
squash_and,
squash_true,
sq_or_squash,
exists-elim,
trivial-eq,
iff_transitivity,
ifthenelse-prop,
or_functionality_wrt_iff,
nequal_wf,
and_functionality_wrt_uiff2,
assert_of_eq_int,
neg_assert_of_eq_int,
bag-member-map,
assert_of_null,
not_functionality_wrt_uiff,
or_false_r,
bag-member-ifthenelse,
bool_wf,
uiff_transitivity,
eqtt_to_assert,
bag-member-append,
eqff_to_assert,
assert_of_bnot,
bag-member-single-weak,
pair-eta,
and_false_r,
bag-member-empty-weak,
exists-product1,
exists-union,
exists-unit,
simple-loc-comb-2-concat-classrel-weak
HIDDEN
Date html generated:
2012_02_20-PM-05_29_47
Last ObjectModification:
2012_02_16-PM-05_53_16
Home
Index