Nuprl Lemma : bag-size-cons

[b:bag(Top)]. ∀[x:Top].  (#(x.b) #(b))


Proof




Definitions occuring in Statement :  bag-size: #(bs) cons-bag: x.b bag: bag(T) uall: [x:A]. B[x] top: Top add: m natural_number: $n sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T top: Top nat: subtype_rel: A ⊆B guard: {T} ge: i ≥  all: x:A. B[x] decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False implies:  Q not: ¬A and: P ∧ Q prop: so_lambda: λ2x.t[x] so_apply: x[s] bag-size: #(bs) cons-bag: x.b uiff: uiff(P;Q) le: A ≤ B less_than': less_than'(a;b) sq_type: SQType(T)
Lemmas referenced :  bag-size_wf top_wf cons-bag_wf nat_properties decidable__le nat_wf satisfiable-full-omega-tt intformand_wf intformle_wf itermConstant_wf itermVar_wf intformnot_wf itermAdd_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_not_lemma int_term_value_add_lemma int_formula_prop_wf le_wf subtype_base_sq set_subtype_base int_subtype_base length_of_cons_lemma decidable__equal_int add-is-int-iff intformeq_wf int_formula_prop_eq_lemma false_wf add_nat_wf equal_wf bag_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis isect_memberEquality voidElimination voidEquality hypothesisEquality dependent_set_memberEquality addEquality natural_numberEquality applyEquality because_Cache sqequalRule equalityTransitivity equalitySymmetry applyLambdaEquality setElimination rename dependent_functionElimination lambdaEquality unionElimination independent_isectElimination dependent_pairFormation int_eqEquality intEquality independent_pairFormation computeAll instantiate cumulativity pointwiseFunctionality promote_hyp baseClosed baseApply closedConclusion productElimination lambdaFormation independent_functionElimination sqequalAxiom

Latex:
\mforall{}[b:bag(Top)].  \mforall{}[x:Top].    (\#(x.b)  \msim{}  1  +  \#(b))



Date html generated: 2017_10_01-AM-08_45_46
Last ObjectModification: 2017_07_26-PM-04_30_54

Theory : bags


Home Index