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) ∈ V)
∧ (∀i:ℕ||as||
∃L:consensus-rcv(V;A) List. (L ≤ s as[i] ∧ archive-condition(V;A;t;f;n - 1;vs[i];L))))))))))
Proof
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,
iseg: l1 ≤ l2,
no_repeats: no_repeats(T;l),
l_member: (x ∈ l),
select: L[n],
length: ||as||,
list: T List,
rel_star: R^*,
nat_plus: ℕ+,
int_seg: {i..j-},
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],
multiply: n * m,
subtract: n - m,
add: n + m,
natural_number: $n,
int: ℤ,
universe: Type,
equal: s = t ∈ T,
ts-rel: ts-rel(ts),
ts-init: ts-init(ts),
ts-type: ts-type(ts)
Lemmas :
ts-reachable-induction3,
three-consensus-ts_wf,
nat_plus_subtype_nat,
all_wf,
l_member_wf,
list_wf,
consensus-rcv_wf,
iseg_wf,
subtype_rel_set,
ts-type_wf,
infix_ap_wf,
rel_star_wf,
ts-rel_wf,
ts-init_wf,
subtype_rel_self,
archive-condition_wf,
exists_wf,
no_repeats_wf,
length_wf,
int_seg_wf,
select_wf,
sq_stable__le,
subtract_wf,
less_than_transitivity1,
Id_wf,
le_weakening,
ts-reachable_wf,
subtype_rel_wf,
iseg_nil,
list-cases,
null_nil_lemma,
archive-condition-nil,
product_subtype_list,
null_cons_lemma,
nil_wf,
set_wf,
nat_wf,
cs-rcv-vote_wf,
not_wf,
equal_wf,
append_wf,
cons_wf,
nat_plus_wf,
iseg_transitivity,
decidable__equal_Id,
subtype_base_sq,
atom2_subtype_base,
iseg_weakening,
iseg_append,
iff_weakening_equal,
iseg-append-one,
length_wf_nat,
archive-condition-append-init,
less_than_irreflexivity,
archive-condition-append-vote,
int_subtype_base,
less_than_wf,
consensus-rcv-crosses-size,
remove-repeats_wf,
id-deq_wf,
subtype_rel-deq,
sq_stable__l_member,
map_wf,
votes-from-inning_wf,
remove-repeats-no_repeats,
values-for-distinct_wf,
values-for-distinct-property,
vote-crosses-threshold,
decidable__le,
false_wf,
not-le-2,
less-iff-le,
condition-implies-le,
minus-one-mul,
zero-add,
minus-add,
minus-minus,
add-associates,
add-swap,
add-commutes,
add_functionality_wrt_le,
add-zero,
le-add-cancel,
le_wf,
member-remove-repeats,
select_member,
member_wf,
member-votes-from-inning,
squash_wf,
true_wf,
set_subtype_base,
member_append,
member_singleton,
or_wf,
three-cs-vote-invariant,
le_transitivity
\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:
2015_07_17-AM-11_52_59
Last ObjectModification:
2015_07_16-AM-10_13_04
Home
Index