Nuprl Lemma : bag-size-bound

[T:Type]. ∀[as,bs:bag(T)]. ∀[n:ℕ].  #(as bs) n < #(bs) supposing #(as) < n


Proof




Definitions occuring in Statement :  bag-size: #(bs) bag-append: as bs bag: bag(T) nat: less_than: a < b uimplies: supposing a uall: [x:A]. B[x] subtract: m universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a top: Top nat: ge: i ≥  all: x:A. B[x] subtype_rel: A ⊆B decidable: Dec(P) or: P ∨ Q less_than: a < b squash: T and: P ∧ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False implies:  Q not: ¬A prop:
Lemmas referenced :  bag_wf bag-append_wf member-less_than nat_wf less_than_wf int_formula_prop_wf int_term_value_var_lemma int_term_value_add_lemma int_term_value_subtract_lemma int_formula_prop_less_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermAdd_wf itermSubtract_wf intformless_wf intformnot_wf intformand_wf satisfiable-full-omega-tt bag-size_wf subtract_wf decidable__lt nat_properties bag-size-append
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin isect_memberEquality voidElimination voidEquality hypothesis hypothesisEquality setElimination rename dependent_functionElimination addEquality applyEquality because_Cache unionElimination imageElimination productElimination lambdaEquality natural_numberEquality independent_isectElimination dependent_pairFormation int_eqEquality intEquality independent_pairFormation computeAll equalityTransitivity equalitySymmetry universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:bag(T)].  \mforall{}[n:\mBbbN{}].    \#(as  +  bs)  -  n  <  \#(bs)  supposing  \#(as)  <  n



Date html generated: 2016_05_15-PM-02_25_12
Last ObjectModification: 2016_01_16-AM-08_57_03

Theory : bags


Home Index