Nuprl Lemma : ohc_v1-ilf-quorum1
HIDDEN
Proof not projected
Definitions occuring in Statement :
ohc_v1_Quorum1: ohc_v1_Quorum1(Cmd;cmdeq;flrs),
ohc_v1_add_to_quorum: ohc_v1_add_to_quorum(),
ohc_v1_newvote: ohc_v1_newvote(),
ohc_v1_init: ohc_v1_init(),
ohc_v1_proposal'base: ohc_v1_proposal'base(Cmd),
Memory-class: Memory-class(f;init;X),
base-headers-msg-val: Base(hdr;typ),
Message: Message,
classrel: v 
X(e),
event-ordering+: EO+(Info),
es-E: E,
Id: Id,
length: ||as||,
assert: 
b,
it: 
,
uall: 
[x:A]. B[x],
guard: {T},
pi1: fst(t),
pi2: snd(t),
all: x:A. B[x],
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),
valueall-type: valueall-type(T)
Definitions :
hide: HIDDEN,
uall: [x:A]. B[x],
all: x:A. B[x],
guard: {T},
iff: P Q,
classrel: v X(e),
squash: T,
exists: x:A. B[x],
and: P Q,
or: P Q,
ohc_v1_newvote: ohc_v1_newvote(),
member: t T,
bag-member: x bs,
ohc_v1_roundout1: ohc_v1_roundout1(Cmd;cmdeq;flrs),
prop: 
,
name: Name,
cand: A c B,
implies: P Q,
rev_implies: P Q,
top: Top,
subtype: S 
T,
so_lambda: 
x.t[x],
vatype: ValueAllType,
true: True,
nequal: a 
b T ,
ifthenelse: if b then t else f fi ,
exposed-bfalse: exposed-bfalse,
btrue: tt,
bfalse: ff,
ohc_v1_proposal'base: ohc_v1_proposal'base(Cmd),
ohc_v1_when_quorum1: ohc_v1_when_quorum1(Cmd;cmdeq;flrs),
ohc_v1_Quorum1State: ohc_v1_Quorum1State(Cmd),
ohc_v1_Quorum1: ohc_v1_Quorum1(Cmd;cmdeq;flrs),
nat: 
,
so_apply: x[s],
unit: Unit,
bool: 
,
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q),
uimplies: b supposing a,
it:
Lemmas :
false_wf,
classrel_wf,
Message_wf,
Id_wf,
base-headers-msg-val_wf,
length_wf,
or_wf,
pi1_wf_top,
poss-maj_wf,
nat_wf,
unit_wf2,
pi2_wf,
not_wf,
equal_wf,
it_wf,
ifthenelse_wf,
eq_int_wf,
exists_wf,
Memory-class_wf,
ohc_v1_add_to_quorum_wf,
ohc_v1_init_wf,
bag_wf,
ohc_v1_proposal'base_wf,
assert_wf,
band_wf,
eqof_wf,
product-deq_wf,
int-deq_wf,
bnot_wf,
deq-member_wf,
id-deq_wf,
bag-member_wf,
single-bag_wf,
empty-bag_wf,
squash_wf,
simple-loc-comb-2_wf,
concat-lifting-loc-2_wf,
ohc_v1_when_quorum1_wf,
ohc_v1_Quorum1State_wf,
ohc_v1_Quorum1_wf,
es-E_wf,
event-ordering+_inc,
event-ordering+_wf,
deq_wf,
valueall-type_wf,
or_false_r,
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-ifthenelse,
bool_wf,
uiff_transitivity,
eqtt_to_assert,
bag-member-single-weak,
eqff_to_assert,
assert_of_bnot,
not_functionality_wrt_uiff,
and_false_r,
pair-eta,
bag-member-empty-weak,
exists-product1,
simple-loc-comb-2-concat-classrel-weak,
es-loc_wf
HIDDEN
Date html generated:
2012_02_20-PM-05_29_34
Last ObjectModification:
2012_02_16-PM-05_53_08
Home
Index