Nuprl Lemma : permr_iff_eq_counts_a
∀s:DSet. ∀as,bs:|s| List. (as ≡(|s|) bs ⇐⇒ {∀x:|s|. ((x #∈ as) = (x #∈ bs) ∈ ℤ)})
Proof
Definitions occuring in Statement :
count: a #∈ as,
permr: as ≡(T) bs,
list: T List,
guard: {T},
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
int: ℤ,
equal: s = t ∈ T,
dset: DSet,
set_car: |p|
Definitions unfolded in proof :
guard: {T}
Lemmas referenced :
permr_iff_eq_counts
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lemma_by_obid
Latex:
\mforall{}s:DSet. \mforall{}as,bs:|s| List. (as \mequiv{}(|s|) bs \mLeftarrow{}{}\mRightarrow{} \{\mforall{}x:|s|. ((x \#\mmember{} as) = (x \#\mmember{} bs))\})
Date html generated:
2016_05_16-AM-07_39_50
Last ObjectModification:
2015_12_28-PM-05_43_06
Theory : list_2
Home
Index