Nuprl Lemma : bag-count-drop

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


Proof




Definitions occuring in Statement :  bag-drop: bag-drop(eq;bs;a) bag-count: (#x in bs) bag-member: x ↓∈ bs bag: bag(T) deq: EqDecider(T) nat: 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 or: P ∨ Q exists: x:A. B[x] and: P ∧ Q cand: c∧ B sq_stable: SqStable(P) implies:  Q squash: T prop: guard: {T} not: ¬A false: False iff: ⇐⇒ Q rev_implies:  Q sq_or: a ↓∨ b uiff: uiff(P;Q) 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 eqof: eqof(d) ifthenelse: if then else fi  decidable: Dec(P) satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top bfalse: ff bnot: ¬bb assert: b bag-drop: bag-drop(eq;bs;a)
Lemmas referenced :  bag-remove1-property sq_stable__bag-member not_wf bag-member_wf equal_wf nat_wf bag-count_wf bag-drop_wf bag_wf deq_wf bag-member-append single-bag_wf bag-member-single subtype_base_sq int_subtype_base subtract_wf cons_wf nil_wf list-subtype-bag ifthenelse_wf bool_wf eqtt_to_assert safe-assert-deq decidable__equal_int full-omega-unsat 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 member_wf squash_wf true_wf bag-count-append subtype_rel_self iff_weakening_equal add_functionality_wrt_eq bag-count-single unit_wf2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache dependent_functionElimination hypothesisEquality unionElimination inlFormation productElimination hypothesis independent_functionElimination sqequalRule imageMemberEquality baseClosed imageElimination independent_pairFormation productEquality inrFormation cumulativity voidElimination universeEquality hyp_replacement equalitySymmetry applyLambdaEquality independent_isectElimination instantiate intEquality applyEquality natural_numberEquality equalityTransitivity lambdaEquality setElimination rename equalityElimination approximateComputation dependent_pairFormation int_eqEquality isect_memberEquality voidEquality promote_hyp unionEquality

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



Date html generated: 2019_10_16-AM-11_31_24
Last ObjectModification: 2018_08_21-PM-01_59_33

Theory : bags_2


Home Index