Nuprl Lemma : apply-alist-count-repeats

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[L:T List].

  (apply-alist(eq;count-repeats(L,eq);x) = if x ∈_b L then inl ||filter(λy.(eq y x);L)|| else inr ⋅  fi  ∈ (ℕ⁺?))

Proof

Definitions occuring in Statement : count-repeats: count-repeats(L,eq), apply-alist: apply-alist(eq;L;x), length: ||as||, deq-member: x ∈_b L, filter: filter(P;l), list: T List, deq: EqDecider(T), nat_plus: ℕ⁺, ifthenelse: if b then t else f fi , it: ⋅, uall: ∀[x:A]. B[x], unit: Unit, apply: f a, lambda: λx.A[x], inr: inr x , inl: inl x, union: left + right, universe: Type, equal: s = t ∈ T
Definitions unfolded in proof : uall: ∀[x:A]. B[x], member: t ∈ T, so_lambda: λ₂x.t[x], so_apply: x[s], implies: P ⇒ Q, guard: {T}, all: ∀x:A. B[x], exposed-bfalse: exposed-bfalse, bool: 𝔹, unit: Unit, it: ⋅, btrue: tt, uiff: uiff(P;Q), and: P ∧ Q, uimplies: b supposing a, iff: P ⇐⇒ Q, ifthenelse: if b then t else f fi , bfalse: ff, exists: ∃x:A. B[x], or: P ∨ Q, sq_type: SQType(T), bnot: ¬_bb, assert: ↑b, false: False, not: ¬A, rev_implies: P ⇐ Q, prop: ℙ, nat_plus: ℕ⁺, deq: EqDecider(T), eqof: eqof(d), rev_uimplies: rev_uimplies(P;Q), so_apply: x[s1;s2;s3], so_lambda: so_lambda(x,y,z.t[x; y; z]), so_apply: x[s1;s2], so_lambda: λ₂x y.t[x; y], top: Top, apply-alist: apply-alist(eq;L;x), count-repeats: count-repeats(L,eq), satisfiable_int_formula: satisfiable_int_formula(fmla), le: A ≤ B, subtract: n - m, decidable: Dec(P), true: True, less_than': less_than'(a;b), less_than: a < b, squash: ↓T, subtype_rel: A ⊆r B
Lemmas referenced : last_induction, list_wf, deq_wf, equal_wf, nat_plus_wf, unit_wf2, apply-alist_wf, count-repeats_wf, deq-member_wf, eqtt_to_assert, assert-deq-member, eqff_to_assert, bool_cases_sqequal, subtype_base_sq, bool_wf, bool_subtype_base, assert-bnot, l_member_wf, it_wf, length_wf, filter_wf5, member-exists2, member_filter, safe-assert-deq, less_than_wf, list_ind_nil_lemma, filter_nil_lemma, deq_member_nil_lemma, list_accum_nil_lemma, equal-wf-T-base, cons_member, length_of_nil_lemma, length_of_cons_lemma, member_append, append_back_nil, length-singleton, length-append, int_formula_prop_wf, int_term_value_var_lemma, int_term_value_add_lemma, int_term_value_constant_lemma, int_formula_prop_less_lemma, int_formula_prop_not_lemma, int_formula_prop_and_lemma, itermVar_wf, itermAdd_wf, itermConstant_wf, intformless_wf, intformnot_wf, intformand_wf, satisfiable-full-omega-tt, filter_cons_lemma, filter_append_sq, iff_weakening_equal, le-add-cancel, add-zero, add-associates, add_functionality_wrt_le, add-commutes, minus-one-mul-top, zero-add, minus-one-mul, minus-add, condition-implies-le, less-iff-le, not-lt-2, false_wf, decidable__lt, apply-updated-alist, true_wf, squash_wf, list_accum_cons_lemma, top_wf, subtype_rel_list, list_accum_append, nil_wf, cons_wf, append_wf, and_wf, assert_wf, not_wf, l_all_iff, filter_is_nil, or_wf, member_singleton
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, Error :isect_memberFormation_alt, introduction, cut, thin, extract_by_obid, sqequalHypSubstitution, isectElimination, hypothesisEquality, sqequalRule, independent_functionElimination, hypothesis, dependent_functionElimination, Error :universeIsType, Error :isect_memberEquality_alt, axiomEquality, because_Cache, universeEquality, Error :lambdaEquality_alt, unionEquality, Error :inhabitedIsType, Error :lambdaFormation_alt, unionElimination, equalityElimination, equalityTransitivity, equalitySymmetry, productElimination, independent_isectElimination, Error :inlEquality_alt, Error :dependent_pairFormation_alt, Error :equalityIsType1, promote_hyp, instantiate, cumulativity, voidElimination, Error :inrEquality_alt, Error :dependent_set_memberEquality_alt, setElimination, rename, applyEquality, Error :setIsType, independent_pairFormation, natural_numberEquality, inrEquality, voidEquality, isect_memberEquality, inrFormation, inlFormation, applyLambdaEquality, hyp_replacement, computeAll, int_eqEquality, inlEquality, minusEquality, intEquality, addEquality, baseClosed, imageMemberEquality, dependent_set_memberEquality, levelHypothesis, equalityUniverse, imageElimination, dependent_pairFormation, setEquality, lambdaEquality, lambdaFormation, addLevel, orFunctionality

Latex:
\mforall{}[T:Type]. \mforall{}[eq:EqDecider(T)]. \mforall{}[x:T]. \mforall{}[L:T List]. (apply-alist(eq;count-repeats(L,eq);x) = if x \mmember{}\msubb{} L then inl ||filter(\mlambda{}y.(eq y x);L)|| else inr \mcdot{} fi ) Date html generated: 2019_06_20-PM-01_54_46 Last ObjectModification: 2018_10_05-AM-10_55_37 Theory : decidable!equality Home Index