Nuprl Lemma : bag-remove-size-member-no-repeats

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


Definitions occuring in Statement :  bag-remove: bs x bag-member: x ↓∈ bs bag-no-repeats: bag-no-repeats(T;bs) bag-size: #(bs) bag: bag(T) deq: EqDecider(T) uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] subtract: m natural_number: $n int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] or: P ∨ Q and: P ∧ Q uimplies: supposing a squash: T prop: subtype_rel: A ⊆B nat: true: True guard: {T} iff: ⇐⇒ Q implies:  Q not: ¬A false: False
Lemmas referenced :  bag-remove-size equal_wf squash_wf true_wf subtract_wf bag-size_wf nat_wf bag-count-member-no-repeats iff_weakening_equal bag-member_wf bag-no-repeats_wf bag_wf deq_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaFormation dependent_functionElimination unionElimination productElimination applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry universeEquality intEquality cumulativity setElimination rename sqequalRule independent_isectElimination natural_numberEquality imageMemberEquality baseClosed because_Cache independent_functionElimination isect_memberEquality axiomEquality voidElimination

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

Date html generated: 2018_05_21-PM-09_47_54
Last ObjectModification: 2017_07_26-PM-06_30_29

Theory : bags_2

Home Index