Nuprl Lemma : bag-count-member-no-repeats

[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].  ((#x in bs) 1 ∈ ℤsupposing (bag-no-repeats(T;bs) and x ↓∈ bs)


Definitions occuring in Statement :  bag-count: (#x in bs) bag-member: x ↓∈ bs bag-no-repeats: bag-no-repeats(T;bs) bag: bag(T) deq: EqDecider(T) uimplies: supposing a uall: [x:A]. B[x] natural_number: $n int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a rev_uimplies: rev_uimplies(P;Q) prop:
Lemmas referenced :  bag-no-repeats-count bag-no-repeats_wf bag-member_wf bag_wf deq_wf bag-member-count
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality productElimination introduction independent_isectElimination independent_pairFormation sqequalRule isect_memberEquality axiomEquality because_Cache equalityTransitivity equalitySymmetry universeEquality

\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].  \mforall{}[x:T].
    ((\#x  in  bs)  =  1)  supposing  (bag-no-repeats(T;bs)  and  x  \mdownarrow{}\mmember{}  bs)

Date html generated: 2016_05_15-PM-07_59_26
Last ObjectModification: 2015_12_27-PM-04_16_25

Theory : bags_2

Home Index