Nuprl Lemma : three-cs-archive-condition
V:Type. A:Id List. t:
. f:V List 
V. s:ts-type(three-consensus-ts(V;A;t;f)).
((ts-init(three-consensus-ts(V;A;t;f)) (ts-rel(three-consensus-ts(V;A;t;f))^*) s)
(v:V. a:{a:Id| (a 
A)} . n:. L:consensus-rcv(V;A) List.
(L 
s a
archive-condition(V;A;t;f;n;v;L)
(
as:{a:Id| (a A)} List
(no_repeats({a:Id| (a A)} ;as)
(||as|| = ((2 * t) + 1))
(vs:V List
((||vs|| = ||as||)
(v = (f vs))
(i:||as||
L:consensus-rcv(V;A) List. (L s as[i] archive-condition(V;A;t;f;n - 1;vs[i];L))))))))))
Proof not projected
Definitions occuring in Statement :
three-consensus-ts: three-consensus-ts(V;A;t;f),
archive-condition: archive-condition(V;A;t;f;n;v;L),
consensus-rcv: consensus-rcv(V;A),
Id: Id,
select: l[i],
length: ||as||,
int_seg: {i..j
},
nat_plus: ,
infix_ap: x f y,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
and: P Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x],
list: type List,
multiply: n * m,
subtract: n - m,
add: n + m,
natural_number: $n,
int: 
,
universe: Type,
equal: s = t,
no_repeats: no_repeats(T;l),
iseg: l1 l2,
l_member: (x l),
rel_star: R^*,
ts-rel: ts-rel(ts),
ts-init: ts-init(ts),
ts-type: ts-type(ts)
Definitions :
pi2: snd(t),
false: False,
le: A B,
cand: A c B,
not: 
A,
pi1: fst(t),
so_lambda: 
x.t[x],
member: t T,
prop: 
,
and: P Q,
exists: x:A. B[x],
ts-init: ts-init(ts),
ts-rel: ts-rel(ts),
infix_ap: x f y,
implies: P Q,
three-consensus-ts: three-consensus-ts(V;A;t;f),
all: x:A. B[x],
Id: Id,
no_repeats: no_repeats(T;l),
nat_plus: ,
subtype: S 
T,
top: Top,
true: True,
squash: 
T,
values-for-distinct: values-for-distinct(eq;L),
nat: ,
guard: {T},
sq_type: SQType(T),
rev_implies: P 
Q,
iff: P Q,
or: P 
Q,
ts-type: ts-type(ts),
ifthenelse: if b then t else f fi ,
bfalse: ff,
btrue: tt,
null: null(as),
assert: 
b,
lelt: i j < k,
uimplies: b supposing a,
so_apply: x[s],
ts-reachable: ts-reachable(ts),
uall: [x:A]. B[x],
int_seg: {i..j},
decidable: Dec(P),
consensus-rcv: consensus-rcv(V;A),
sq_stable: SqStable(P),
cs-initial-rcv: Init[v],
cs-rcv-vote: Vote[a;i;v]
Lemmas :
ts-init_wf,
ts-rel_wf,
rel_star_wf,
append_wf,
not_wf,
cs-rcv-vote_wf,
equal_wf,
nat_wf,
archive-condition-nil,
iseg_nil,
ts-type_wf,
ts-reachable_wf,
select_wf,
int_seg_wf,
length_wf,
no_repeats_wf,
exists_wf,
archive-condition_wf,
iseg_wf,
consensus-rcv_wf,
nat_plus_wf,
l_member_wf,
Id_wf,
all_wf,
nat_plus_inc,
three-consensus-ts_wf,
ts-reachable-induction3,
iseg_append,
iseg_weakening,
Id_sq,
decidable__equal_Id,
iseg-append-one,
atom2_subtype_base,
subtype_base_sq,
member_wf,
length_wf_nat,
archive-condition-append-vote,
archive-condition-append-init,
int_sq,
remove-repeats_property,
votes-from-inning_wf,
pi1_wf_top,
map_wf,
strong-subtype-self,
strong-subtype-set3,
strong-subtype-deq-subtype,
id-deq_wf,
remove-repeats_wf,
consensus-rcv-crosses-size,
decidable__l_member,
sq_stable_from_decidable,
values-for-distinct_wf,
length-map,
vote-crosses-threshold,
int_subtype_base,
le_wf,
values-for-distinct-property,
member-remove-repeats,
property-from-l_member,
member_singleton,
or_functionality_wrt_iff,
member_append,
iff_transitivity,
three-cs-vote-invariant
\mforall{}V:Type. \mforall{}A:Id List. \mforall{}t:\mBbbN{}\msupplus{}. \mforall{}f:V List {}\mrightarrow{} V. \mforall{}s:ts-type(three-consensus-ts(V;A;t;f)).
((ts-init(three-consensus-ts(V;A;t;f)) (ts-rel(three-consensus-ts(V;A;t;f))\^{}*) s)
{}\mRightarrow{} (\mforall{}v:V. \mforall{}a:\{a:Id| (a \mmember{} A)\} . \mforall{}n:\mBbbN{}\msupplus{}. \mforall{}L:consensus-rcv(V;A) List.
(L \mleq{} s a
{}\mRightarrow{} archive-condition(V;A;t;f;n;v;L)
{}\mRightarrow{} (\mexists{}as:\{a:Id| (a \mmember{} A)\} List
(no\_repeats(\{a:Id| (a \mmember{} A)\} ;as)
\mwedge{} (||as|| = ((2 * t) + 1))
\mwedge{} (\mexists{}vs:V List
((||vs|| = ||as||)
\mwedge{} (v = (f vs))
\mwedge{} (\mforall{}i:\mBbbN{}||as||
\mexists{}L:consensus-rcv(V;A) List
(L \mleq{} s as[i] \mwedge{} archive-condition(V;A;t;f;n - 1;vs[i];L))))))))))
Date html generated:
2012_01_23-PM-12_07_43
Last ObjectModification:
2011_12_14-PM-09_20_33
Home
Index