Nuprl Lemma : rcvd-innings-nil
∀[V:Type]. ∀[A:Id List]. ∀[L:consensus-rcv(V;A) List]. ∀[i,n:ℤ].
(filter(λr.i <z inning(r);L) ~ []) supposing
((n ≤ i) and
(filter(λr.n <z inning(r);L) = [] ∈ (consensus-rcv(V;A) List)))
Proof
Definitions occuring in Statement :
rcvd-inning-gt: i <z inning(r),
consensus-rcv: consensus-rcv(V;A),
Id: Id,
filter: filter(P;l),
nil: [],
list: T List,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
le: A ≤ B,
lambda: λx.A[x],
int: ℤ,
universe: Type,
sqequal: s ~ t,
equal: s = t ∈ T
Lemmas :
filter_is_nil,
rcvd-inning-gt_wf,
l_all_iff,
l_member_wf,
not_wf,
assert_wf,
le_wf,
equal-wf-T-base,
list_wf,
consensus-rcv_wf,
filter_wf5,
Id_wf,
member_filter,
false_wf,
less_than_transitivity2,
less_than_wf,
assert_of_lt_int,
lt_int_wf,
length_wf_nat,
equal_wf,
nat_wf,
null_nil_lemma,
btrue_wf,
member-implies-null-eq-bfalse,
btrue_neq_bfalse
\mforall{}[V:Type]. \mforall{}[A:Id List]. \mforall{}[L:consensus-rcv(V;A) List]. \mforall{}[i,n:\mBbbZ{}].
(filter(\mlambda{}r.i <z inning(r);L) \msim{} []) supposing ((n \mleq{} i) and (filter(\mlambda{}r.n <z inning(r);L) = []))
Date html generated:
2015_07_17-AM-11_48_08
Last ObjectModification:
2015_01_28-AM-00_45_36
Home
Index