Nuprl Lemma : votes-from-inning-is-nil
∀[V:Type]. ∀[A:Id List]. ∀[L:consensus-rcv(V;A) List]. ∀[i,n:ℤ].
(votes-from-inning(i;L) ~ []) supposing (n < i and (filter(λr.n <z inning(r);L) = [] ∈ (consensus-rcv(V;A) List)))
Proof
Definitions occuring in Statement :
votes-from-inning: votes-from-inning(i;L),
rcvd-inning-gt: i <z inning(r),
consensus-rcv: consensus-rcv(V;A),
Id: Id,
filter: filter(P;l),
nil: [],
list: T List,
less_than: a < b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
lambda: λx.A[x],
int: ℤ,
universe: Type,
sqequal: s ~ t,
equal: s = t ∈ T
Lemmas :
filter_is_nil,
rcvd-inning-eq_wf,
assert_wf,
select_wf,
sq_stable__le,
int_seg_wf,
length_wf,
map_nil_lemma,
less_than_wf,
equal-wf-T-base,
list_wf,
consensus-rcv_wf,
filter_wf5,
l_member_wf,
rcvd-inning-gt_wf,
Id_wf,
member_filter,
select_member,
false_wf,
less_than_transitivity1,
le_weakening,
equal-wf-base-T,
int_subtype_base,
assert_of_eq_int,
assert_of_lt_int,
eq_int_wf,
length_wf_nat,
equal_wf,
nat_wf,
null_nil_lemma,
btrue_wf,
member-implies-null-eq-bfalse,
and_wf,
null_wf3,
subtype_rel_set,
top_wf,
subtype_rel_list,
btrue_neq_bfalse
\mforall{}[V:Type]. \mforall{}[A:Id List]. \mforall{}[L:consensus-rcv(V;A) List]. \mforall{}[i,n:\mBbbZ{}].
(votes-from-inning(i;L) \msim{} []) supposing (n < i and (filter(\mlambda{}r.n <z inning(r);L) = []))
Date html generated:
2015_07_17-AM-11_48_03
Last ObjectModification:
2015_01_28-AM-00_45_44
Home
Index