### Nuprl Lemma : bag-count-remove1

[T:Type]
∀eq:EqDecider(T). ∀x:T. ∀bs:bag(T).
((x ↓∈ bs ∧ ((#x in outl(bag-remove1(eq;bs;x))) ((#x in bs) 1) ∈ ℕ)) ∨ x ↓∈ bs))

Proof

Definitions occuring in Statement :  bag-remove1: bag-remove1(eq;bs;a) bag-count: (#x in bs) bag-member: x ↓∈ bs bag: bag(T) deq: EqDecider(T) nat: outl: outl(x) uall: [x:A]. B[x] all: x:A. B[x] not: ¬A or: P ∨ Q and: P ∧ Q subtract: m natural_number: \$n 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 exists: x:A. B[x] not: ¬A false: False prop: guard: {T} uimplies: supposing a subtype_rel: A ⊆B sq_type: SQType(T) true: True nat: single-bag: {x} deq: EqDecider(T) bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) eqof: eqof(d) ifthenelse: if then else fi  satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top bfalse: ff bnot: ¬bb assert: b squash: T iff: ⇐⇒ Q rev_implies:  Q isl: isl(x) outl: outl(x)
Lemmas referenced :  decidable__bag-member decidable-equal-deq bag-remove1-property not_wf bag-member_wf equal_wf nat_wf bag-count_wf bag_wf deq_wf subtype_base_sq int_subtype_base subtract_wf single-bag_wf cons_wf nil_wf list-subtype-bag ifthenelse_wf bool_wf eqtt_to_assert safe-assert-deq decidable__equal_int satisfiable-full-omega-tt intformnot_wf intformeq_wf itermSubtract_wf itermAdd_wf itermConstant_wf itermVar_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_subtract_lemma int_term_value_add_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot squash_wf true_wf bag-count-append iff_weakening_equal add_functionality_wrt_eq bag-count-single outl_wf assert_wf isl_wf unit_wf2 and_wf btrue_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality independent_functionElimination dependent_functionElimination unionElimination inlFormation independent_pairFormation because_Cache productElimination voidElimination cumulativity sqequalRule inrFormation productEquality equalityTransitivity equalitySymmetry universeEquality instantiate intEquality independent_isectElimination hyp_replacement applyLambdaEquality applyEquality natural_numberEquality lambdaEquality setElimination rename equalityElimination dependent_pairFormation int_eqEquality isect_memberEquality voidEquality computeAll promote_hyp imageElimination imageMemberEquality baseClosed unionEquality dependent_set_memberEquality

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

Date html generated: 2018_05_21-PM-09_48_21
Last ObjectModification: 2017_07_26-PM-06_30_37

Theory : bags_2

Home Index