Nuprl Lemma : bag-remove-size

[T:Type]
  ∀eq:EqDecider(T). ∀bs:bag(T). ∀x:T.
    ((x ↓∈ bs ∧ (#(bs x) (#(bs) (#x in bs)) ∈ ℤ)) ∨ ((¬x ↓∈ bs) ∧ (#(bs x) #(bs) ∈ ℤ)))


Proof




Definitions occuring in Statement :  bag-remove: bs x bag-count: (#x in bs) bag-member: x ↓∈ bs bag-size: #(bs) bag: bag(T) deq: EqDecider(T) uall: [x:A]. B[x] all: x:A. B[x] not: ¬A or: P ∨ Q and: P ∧ Q subtract: m int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] member: t ∈ T implies:  Q decidable: Dec(P) or: P ∨ Q and: P ∧ Q cand: c∧ B prop: subtype_rel: A ⊆B nat: guard: {T} squash: T uimplies: supposing a true: True iff: ⇐⇒ Q rev_implies:  Q exists: x:A. B[x] bag-count: (#x in bs) bag-size: #(bs) bag-remove: bs x bag-filter: [x∈b|p[x]] count: count(P;L) so_lambda: λ2x.t[x] deq: EqDecider(T) bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  uiff: uiff(P;Q) eqof: eqof(d) bfalse: ff sq_type: SQType(T) bnot: ¬bb assert: b false: False not: ¬A so_apply: x[s] top: Top subtract: m satisfiable_int_formula: satisfiable_int_formula(fmla)
Lemmas referenced :  bag_wf deq_wf decidable__bag-member decidable-equal-deq not_wf bag-member_wf equal_wf bag-size_wf bag-remove_wf nat_wf squash_wf true_wf bag-remove-trivial iff_weakening_equal subtract_wf bag-count_wf bag_to_squash_list bag-member-list list_induction all_wf length_wf filter_wf5 l_member_wf bnot_wf reduce_wf bool_wf eqtt_to_assert safe-assert-deq eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot list_wf filter_nil_lemma length_of_nil_lemma reduce_nil_lemma filter_cons_lemma length_of_cons_lemma reduce_cons_lemma int_subtype_base decidable__equal_int ifthenelse_wf satisfiable-full-omega-tt intformnot_wf intformeq_wf itermSubtract_wf itermAdd_wf itermVar_wf itermConstant_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_subtract_lemma int_term_value_add_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_wf add_functionality_wrt_eq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation hypothesisEquality cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesis universeEquality independent_functionElimination because_Cache dependent_functionElimination unionElimination inlFormation independent_pairFormation productEquality intEquality applyEquality lambdaEquality setElimination rename sqequalRule inrFormation imageElimination equalityTransitivity equalitySymmetry independent_isectElimination natural_numberEquality imageMemberEquality baseClosed productElimination promote_hyp hyp_replacement applyLambdaEquality setEquality addEquality equalityElimination dependent_pairFormation instantiate voidElimination isect_memberEquality voidEquality int_eqEquality computeAll

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}bs:bag(T).  \mforall{}x:T.
        ((x  \mdownarrow{}\mmember{}  bs  \mwedge{}  (\#(bs  -  x)  =  (\#(bs)  -  (\#x  in  bs))))  \mvee{}  ((\mneg{}x  \mdownarrow{}\mmember{}  bs)  \mwedge{}  (\#(bs  -  x)  =  \#(bs))))



Date html generated: 2018_05_21-PM-09_47_52
Last ObjectModification: 2017_07_26-PM-06_30_27

Theory : bags_2


Home Index