Nuprl Lemma : member-count-repeats2

∀[T:Type]
  ∀eq:EqDecider(T). ∀L:T List. ∀i:ℕ||count-repeats(L,eq)||.
    let x,n = count-repeats(L,eq)[i]
    in n = ||filter(λy.(eq y x);L)|| ∈ ℤ

Proof

Definitions occuring in Statement : count-repeats: count-repeats(L,eq), select: L[n], length: ||as||, filter: filter(P;l), list: T List, deq: EqDecider(T), int_seg: {i..j^-}, uall: ∀[x:A]. B[x], all: ∀x:A. B[x], apply: f a, lambda: λx.A[x], spread: spread def, natural_number: $n, int: ℤ, universe: Type, equal: s = t ∈ T
Definitions unfolded in proof : uall: ∀[x:A]. B[x], all: ∀x:A. B[x], member: t ∈ T, int_seg: {i..j^-}, uimplies: b supposing a, guard: {T}, lelt: i ≤ j < k, and: P ∧ Q, decidable: Dec(P), or: P ∨ Q, not: ¬A, implies: P ⇒ Q, satisfiable_int_formula: satisfiable_int_formula(fmla), exists: ∃x:A. B[x], false: False, top: Top, prop: ℙ, less_than: a < b, squash: ↓T, sq_type: SQType(T), uiff: uiff(P;Q), iff: P ⇐⇒ Q, ifthenelse: if b then t else f fi , btrue: tt, rev_implies: P ⇐ Q, bfalse: ff, l_member: (x ∈ l), subtype_rel: A ⊆r B, le: A ≤ B, less_than': less_than'(a;b), cand: A c∧ B, nat_plus: ℕ⁺, nat: ℕ, ge: i ≥ j , so_lambda: λ₂x.t[x], so_apply: x[s], outl: outl(x), deq: EqDecider(T), isl: isl(x), assert: ↑b, true: True, pi1: fst(t)
Lemmas referenced : select_wf, nat_plus_wf, count-repeats_wf, int_seg_properties, length_wf, decidable__le, full-omega-unsat, intformand_wf, intformnot_wf, intformle_wf, itermConstant_wf, itermVar_wf, istype-int, int_formula_prop_and_lemma, istype-void, int_formula_prop_not_lemma, int_formula_prop_le_lemma, int_term_value_constant_lemma, int_term_value_var_lemma, int_formula_prop_wf, decidable__lt, intformless_wf, int_formula_prop_less_lemma, int_seg_wf, list_wf, deq_wf, istype-universe, apply-alist-count-repeats, deq-member_wf, assert_wf, bnot_wf, not_wf, l_member_wf, istype-assert, bool_cases, subtype_base_sq, bool_wf, bool_subtype_base, eqtt_to_assert, assert-deq-member, eqff_to_assert, iff_transitivity, iff_weakening_uiff, assert_of_bnot, apply-alist-no_repeats, no_repeats-count-repeats1, int_seg_subtype_nat, istype-false, nat_plus_properties, istype-less_than, nat_properties, equal-wf-base-T, unit_wf2, union_subtype_base, set_subtype_base, less_than_wf, int_subtype_base, unit_subtype_base, length_wf_nat, filter_wf5, outl_wf, equal_wf, btrue_wf, bfalse_wf, nat_plus_subtype_nat, subtype_rel_wf, nat_wf, member-count-repeats1, map-length, map_wf, istype-nat, squash_wf, true_wf, map_select, subtype_rel_self, iff_weakening_equal
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, Error :isect_memberFormation_alt, Error :lambdaFormation_alt, cut, introduction, extract_by_obid, sqequalHypSubstitution, isectElimination, thin, productEquality, hypothesisEquality, hypothesis, because_Cache, setElimination, rename, independent_isectElimination, natural_numberEquality, productElimination, dependent_functionElimination, unionElimination, approximateComputation, independent_functionElimination, Error :dependent_pairFormation_alt, Error :lambdaEquality_alt, int_eqEquality, Error :isect_memberEquality_alt, voidElimination, sqequalRule, independent_pairFormation, Error :universeIsType, imageElimination, Error :inhabitedIsType, Error :equalityIstype, equalityTransitivity, equalitySymmetry, instantiate, universeEquality, Error :functionIsType, cumulativity, applyEquality, Error :productIsType, hyp_replacement, applyLambdaEquality, unionEquality, intEquality, closedConclusion, Error :setIsType, Error :dependent_set_memberEquality_alt, baseApply, baseClosed, sqequalBase, promote_hyp, imageMemberEquality

Latex:
\mforall{}[T:Type] \mforall{}eq:EqDecider(T). \mforall{}L:T List. \mforall{}i:\mBbbN{}||count-repeats(L,eq)||. let x,n = count-repeats(L,eq)[i] in n = ||filter(\mlambda{}y.(eq y x);L)|| Date html generated: 2019_06_20-PM-01_54_50 Last ObjectModification: 2018_11_28-PM-05_14_38 Theory : decidable!equality Home Index