Nuprl Lemma : three-cs-no-repeated-votes
∀V:Type. ∀A:Id List. ∀t:ℕ+. ∀f:(V List) ─→ V. ∀s:ts-reachable(three-consensus-ts(V;A;t;f)). ∀a:{a:Id| (a ∈ A)} .
no_repeats(consensus-rcv(V;A);filter(λx.rcv-vote?(x);s a))
Proof
Definitions occuring in Statement :
three-consensus-ts: three-consensus-ts(V;A;t;f),
rcv-vote?: rcv-vote?(x),
consensus-rcv: consensus-rcv(V;A),
Id: Id,
no_repeats: no_repeats(T;l),
l_member: (x ∈ l),
filter: filter(P;l),
list: T List,
nat_plus: ℕ+,
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x],
function: x:A ─→ B[x],
universe: Type,
ts-reachable: ts-reachable(ts)
Lemmas :
ts-reachable-induction,
three-consensus-ts_wf,
nat_plus_subtype_nat,
all_wf,
l_member_wf,
no_repeats_wf,
consensus-rcv_wf,
filter_wf5,
subtype_rel_set,
ts-type_wf,
list_wf,
infix_ap_wf,
rel_star_wf,
ts-rel_wf,
ts-init_wf,
subtype_rel_self,
rcv-vote?_wf,
ts-reachable_wf,
subtype_rel_wf,
nat_plus_wf,
Id_wf,
set_wf,
sq_stable__no_repeats,
sq_stable__all,
no_repeats_nil,
filter_nil_lemma,
subtype_rel_dep_function,
decidable__equal_Id,
atom2_subtype_base,
subtype_base_sq,
nat_wf,
equal_wf,
length_wf_nat,
l_disjoint_nil2,
assert-bnot,
bool_subtype_base,
bool_cases_sqequal,
eqff_to_assert,
eqtt_to_assert,
bool_wf,
filter_cons_lemma,
no_repeats_singleton,
no_repeats_filter,
nil_wf,
cons_wf,
no_repeats-append,
filter_append_sq,
member_filter,
l_disjoint_singleton,
cs-rcv-vote_wf,
iff_weakening_equal,
true_wf,
squash_wf
\mforall{}V:Type. \mforall{}A:Id List. \mforall{}t:\mBbbN{}\msupplus{}. \mforall{}f:(V List) {}\mrightarrow{} V. \mforall{}s:ts-reachable(three-consensus-ts(V;A;t;f)).
\mforall{}a:\{a:Id| (a \mmember{} A)\} .
no\_repeats(consensus-rcv(V;A);filter(\mlambda{}x.rcv-vote?(x);s a))
Date html generated:
2015_07_17-AM-11_53_23
Last ObjectModification:
2015_07_16-AM-09_46_19
Home
Index