### Nuprl Lemma : count-related-pairs

[T,S:Type]. ∀[K:T List]. ∀[L:S List]. ∀[R:T ⟶ S ⟶ 𝔹].
(||filter(R t;L)|| t ∈ K) = Σ(||filter(λt.(R s);K)|| s ∈ L) ∈ ℤ)

Proof

Definitions occuring in Statement :  lsum: Σ(f[x] x ∈ L) length: ||as|| filter: filter(P;l) list: List bool: 𝔹 uall: [x:A]. B[x] apply: a lambda: λx.A[x] function: x:A ⟶ B[x] int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] prop: uimplies: supposing a all: x:A. B[x] istype: istype(T) true: True so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] squash: T guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q
Lemmas referenced :  bool_wf list_wf istype-universe subtype_rel_dep_function l_member_wf double-lsum-swap ifthenelse_wf equal_wf squash_wf true_wf lsum_wf istype-int length-filter-lsum subtype_rel_self iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt functionIsType universeIsType hypothesisEquality cut introduction extract_by_obid hypothesis sqequalHypSubstitution isectElimination thin inhabitedIsType instantiate universeEquality intEquality applyEquality setElimination rename because_Cache sqequalRule lambdaEquality_alt setEquality setIsType independent_isectElimination lambdaFormation_alt natural_numberEquality imageElimination equalityTransitivity equalitySymmetry imageMemberEquality baseClosed productElimination independent_functionElimination

Latex:
\mforall{}[T,S:Type].  \mforall{}[K:T  List].  \mforall{}[L:S  List].  \mforall{}[R:T  {}\mrightarrow{}  S  {}\mrightarrow{}  \mBbbB{}].
(\mSigma{}(||filter(R  t;L)||  |  t  \mmember{}  K)  =  \mSigma{}(||filter(\mlambda{}t.(R  t  s);K)||  |  s  \mmember{}  L))

Date html generated: 2020_05_19-PM-09_48_21
Last ObjectModification: 2019_11_12-PM-11_50_49

Theory : list_1

Home Index