### Nuprl Lemma : sum-count-repeats

`∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List].  (Σ(snd(count-repeats(L,eq)[i]) | i < ||count-repeats(L,eq)||) = ||L|| ∈ ℤ)`

Proof

Definitions occuring in Statement :  count-repeats: `count-repeats(L,eq)` sum: `Σ(f[x] | x < k)` select: `L[n]` length: `||as||` list: `T List` deq: `EqDecider(T)` uall: `∀[x:A]. B[x]` pi2: `snd(t)` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  member: `t ∈ T` uall: `∀[x:A]. B[x]` prop: `ℙ` and: `P ∧ Q` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` uimplies: `b supposing a` ge: `i ≥ j ` false: `False` implies: `P `` Q` nat: `ℕ` all: `∀x:A. B[x]` sum_aux: `sum_aux(k;v;i;x.f[x])` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` so_apply: `x[s]` so_lambda: `λ2x.t[x]` bfalse: `ff` ifthenelse: `if b then t else f fi ` assert: `↑b` sum: `Σ(f[x] | x < k)` top: `Top` subtype_rel: `A ⊆r B` pi1: `fst(t)` bnot: `¬bb` guard: `{T}` sq_type: `SQType(T)` squash: `↓T` true: `True` less_than': `less_than'(a;b)` less_than: `a < b` uiff: `uiff(P;Q)` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` le: `A ≤ B` or: `P ∨ Q` decidable: `Dec(P)` lelt: `i ≤ j < k` int_seg: `{i..j-}` deq: `EqDecider(T)` nat_plus: `ℕ+` pi2: `snd(t)` no_repeats: `no_repeats(T;l)` cons: `[a / b]` colength: `colength(L)` nil: `[]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` eqof: `eqof(d)` l_all: `(∀x∈L.P[x])`
Lemmas referenced :  istype-universe deq_wf list_wf istype-nat subtract-1-ge-0 istype-less_than ge_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_and_lemma istype-int intformless_wf itermVar_wf itermConstant_wf intformle_wf intformand_wf full-omega-unsat nat_properties length_wf le_wf length_of_nil_lemma l_member_wf false_wf not_wf l_all_iff bfalse_wf filter_is_nil deq_member_nil_lemma top_wf subtype_rel_list count-repeats_wf nat_plus_wf map_wf first0 less_than_wf assert_wf iff_weakening_uiff assert-bnot bool_subtype_base bool_wf bool_cases_sqequal eqff_to_assert decidable__lt map-length pi1_wf istype-le firstn_decomp int_subtype_base subtype_base_sq istype-top assert_of_lt_int eqtt_to_assert lt_int_wf sum-unroll int_term_value_subtract_lemma int_formula_prop_not_lemma itermSubtract_wf intformnot_wf subtract_wf decidable__le select-map filter_wf5 length_wf_nat set_subtype_base select_wf member-count-repeats2 member_firstn nat_plus_properties istype-void no_repeats-count-repeats1 intformeq_wf int_formula_prop_eq_lemma firstn_wf list-cases filter_nil_lemma product_subtype_list colength-cons-not-zero colength_wf_list spread_cons_lemma decidable__equal_int itermAdd_wf int_term_value_add_lemma filter_cons_lemma deq-member_wf equal-wf-T-base istype-assert equal_wf append_wf cons_wf nil_wf bnot_wf member_append eqof_wf length_of_cons_lemma add-is-int-iff cons_member iff_transitivity assert-deq-member assert_of_bnot uiff_transitivity safe-assert-deq member_singleton int_seg_wf iff_weakening_equal subtype_rel_self map_length_nat true_wf squash_wf firstn_all int_seg_properties filter_trivial select_member member-count-repeats1
Rules used in proof :  universeEquality instantiate inhabitedIsType isectIsTypeImplies axiomEquality isect_memberEquality_alt sqequalRule hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid universeIsType hypothesis cut introduction isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution functionIsTypeImplies voidElimination independent_pairFormation Error :memTop,  dependent_functionElimination int_eqEquality lambdaEquality_alt dependent_pairFormation_alt independent_functionElimination approximateComputation independent_isectElimination natural_numberEquality intWeakElimination rename setElimination lambdaFormation_alt lambdaFormation setEquality voidEquality isect_memberEquality applyEquality productElimination lambdaEquality because_Cache cumulativity productEquality promote_hyp equalityIstype productIsType dependent_set_memberEquality_alt intEquality imageElimination baseClosed imageMemberEquality axiomSqEquality lessCases equalitySymmetry equalityTransitivity equalityElimination unionElimination sqequalBase setIsType closedConclusion applyLambdaEquality baseApply hypothesis_subsumption functionIsType inlFormation_alt pointwiseFunctionality inrFormation_alt hyp_replacement

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L:T  List].
(\mSigma{}(snd(count-repeats(L,eq)[i])  |  i  <  ||count-repeats(L,eq)||)  =  ||L||)

Date html generated: 2020_05_19-PM-09_52_21
Last ObjectModification: 2020_03_11-PM-07_57_43

Theory : decidable!equality

Home Index