Nuprl Lemma : int-bag-product_wf

[b:bag(ℤ)]. (b) ∈ ℤ)


Proof




Definitions occuring in Statement :  int-bag-product: Π(b) bag: bag(T) uall: [x:A]. B[x] member: t ∈ T int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T int-bag-product: Π(b) so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a and: P ∧ Q cand: c∧ B assoc: Assoc(T;op) infix_ap: y all: x:A. B[x] decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False implies:  Q not: ¬A top: Top prop: comm: Comm(T;op)
Lemmas referenced :  bag_wf int_formula_prop_wf int_term_value_var_lemma int_term_value_mul_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma itermVar_wf itermMultiply_wf intformeq_wf intformnot_wf satisfiable-full-omega-tt decidable__equal_int bag-product_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin intEquality because_Cache lambdaEquality multiplyEquality hypothesisEquality natural_numberEquality independent_isectElimination dependent_functionElimination hypothesis unionElimination dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality computeAll axiomEquality independent_pairFormation equalityTransitivity equalitySymmetry

Latex:
\mforall{}[b:bag(\mBbbZ{})].  (\mPi{}(b)  \mmember{}  \mBbbZ{})



Date html generated: 2016_05_15-PM-02_33_14
Last ObjectModification: 2016_01_16-AM-08_52_56

Theory : bags


Home Index