### Nuprl Lemma : member-count-repeats3

`∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. ∀[x:T]. ∀[n:ℕ+].`
`  n = ||filter(λy.(eq y x);L)|| ∈ ℤ supposing (<x, n> ∈ count-repeats(L,eq))`

Proof

Definitions occuring in Statement :  count-repeats: `count-repeats(L,eq)` l_member: `(x ∈ l)` length: `||as||` filter: `filter(P;l)` list: `T List` deq: `EqDecider(T)` nat_plus: `ℕ+` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` apply: `f a` lambda: `λx.A[x]` pair: `<a, b>` product: `x:A × B[x]` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` l_member: `(x ∈ l)` exists: `∃x:A. B[x]` cand: `A c∧ B` prop: `ℙ` all: `∀x:A. B[x]` nat: `ℕ` int_seg: `{i..j-}` lelt: `i ≤ j < k` and: `P ∧ Q` le: `A ≤ B` nat_plus: `ℕ+` deq: `EqDecider(T)`
Lemmas referenced :  l_member_wf nat_plus_wf count-repeats_wf list_wf deq_wf member-count-repeats2 lelt_wf length_wf equal_wf filter_wf5
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin hypothesis extract_by_obid isectElimination productEquality cumulativity hypothesisEquality independent_pairEquality sqequalRule isect_memberEquality axiomEquality because_Cache equalityTransitivity equalitySymmetry universeEquality dependent_functionElimination setElimination rename dependent_set_memberEquality independent_pairFormation hyp_replacement Error :applyLambdaEquality,  spreadEquality intEquality lambdaEquality applyEquality setEquality

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L:T  List].  \mforall{}[x:T].  \mforall{}[n:\mBbbN{}\msupplus{}].
n  =  ||filter(\mlambda{}y.(eq  y  x);L)||  supposing  (<x,  n>  \mmember{}  count-repeats(L,eq))

Date html generated: 2016_10_21-AM-10_37_54
Last ObjectModification: 2016_07_12-AM-05_48_57

Theory : decidable!equality

Home Index