Nuprl Lemma : archive-condition-one-one
[V:Type]. [A:Id List]. [t:
]. [f:V List 
V]. [L:consensus-rcv(V;A) List]. [n1,n2:
]. [v1,v2:V].
({(n1 = n2) 
(v1 = v2)}) supposing (archive-condition(V;A;t;f;n2;v2;L) and archive-condition(V;A;t;f;n1;v1;L))
Proof not projected
Definitions occuring in Statement :
archive-condition: archive-condition(V;A;t;f;n;v;L),
consensus-rcv: consensus-rcv(V;A),
Id: Id,
nat_plus: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
guard: {T},
and: P Q,
function: x:A B[x],
list: type List,
int: ,
universe: Type,
equal: s = t
Definitions :
cand: A c B,
false: False,
implies: P 
Q,
not: 
A,
ycomb: Y,
label: ...$L... t,
ge: i 
j ,
nat: ,
length: ||as||,
le: A 
B,
or: P 
Q,
exists: 
x:A. B[x],
so_lambda: 
x.t[x],
prop: 
,
member: t 
T,
and: P Q,
guard: {T},
uimplies: b supposing a,
uall: [x:A]. B[x],
squash: 
T,
subtype: S 
T,
all: x:A. B[x],
top: Top,
bnot: 
b,
outr: outr(x),
isl: isl(x),
outl: outl(x),
true: True,
bfalse: ff,
btrue: tt,
ifthenelse: if b then t else f fi ,
assert: 
b,
reduce: reduce(f;k;as),
filter: filter(P;l),
mapfilter: mapfilter(f;P;L),
map: map(f;as),
votes-from-inning: votes-from-inning(i;L),
values-for-distinct: values-for-distinct(eq;L),
tl: tl(l),
hd: hd(l),
so_apply: x[s],
archive-condition: archive-condition(V;A;t;f;n;v;L),
nat_plus: ,
pi2: snd(t),
pi1: fst(t),
null: null(as),
cs-rcv-vote: Vote[a;i;v],
cs-initial-rcv: Init[v],
append: as @ bs,
consensus-rcv: consensus-rcv(V;A),
rcv-vote?: rcv-vote?(x),
band: p q,
rcvd-inning-eq: inning(r) =
i,
iff: P 
Q,
sq_type: SQType(T)
Lemmas :
nat_plus_wf,
nat_plus_inc,
rcvd-inning-gt_wf,
filter_wf_top,
null_wf3,
assert_wf,
cs-rcv-vote_wf,
Id_wf,
exists_wf,
le_wf,
cs-initial-rcv_wf,
or_wf,
tl_wf,
ge_wf,
hd_wf,
equal_wf,
and_wf,
votes-from-inning_wf,
values-for-distinct_wf,
non_neg_length,
length_cons,
length_wf_nil,
length_nil,
length_wf,
consensus-rcv_wf,
general-append-cancellation,
member_wf,
archive-condition_wf,
nat_wf,
length_wf_nat,
strong-subtype-self,
strong-subtype-set3,
l_member_wf,
strong-subtype-deq-subtype,
id-deq_wf,
pi2_wf,
pi1_wf_top,
false_wf,
outr_wf,
isl_wf,
outl_wf,
true_wf,
remove-repeats_wf,
length-map,
assert_of_bnot,
eqff_to_assert,
uiff_transitivity,
eqtt_to_assert,
iff_weakening_uiff,
bool_subtype_base,
subtype_base_sq,
bool_cases,
bnot_wf,
not_wf,
bool_wf,
rcvd-inning-eq_wf,
map_wf,
append_wf,
nat_plus_properties,
Error :pi2_wf,
vote-crosses-threshold,
top_wf,
consensus-rcv-crosses-threshold,
int_subtype_base,
set_subtype_base,
squash_wf
\mforall{}[V:Type]. \mforall{}[A:Id List]. \mforall{}[t:\mBbbN{}\msupplus{}]. \mforall{}[f:V List {}\mrightarrow{} V]. \mforall{}[L:consensus-rcv(V;A) List]. \mforall{}[n1,n2:\mBbbZ{}].
\mforall{}[v1,v2:V].
(\{(n1 = n2) \mwedge{} (v1 = v2)\}) supposing
(archive-condition(V;A;t;f;n2;v2;L) and
archive-condition(V;A;t;f;n1;v1;L))
Date html generated:
2012_01_23-PM-12_07_24
Last ObjectModification:
2011_12_14-PM-09_43_11
Home
Index