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 < and (filter(λr.n <inning(r);L) [] ∈ (consensus-rcv(V;A) List)))


Definitions occuring in Statement :  votes-from-inning: votes-from-inning(i;L) rcvd-inning-gt: i <inning(r) consensus-rcv: consensus-rcv(V;A) Id: Id filter: filter(P;l) nil: [] list: List less_than: a < b uimplies: supposing a uall: [x:A]. B[x] lambda: λx.A[x] int: universe: Type sqequal: t equal: 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