Nuprl Lemma : mset_union_ident_r

s:DSet. ∀a:MSet{s}.  ((a ⋃ 0{s}) a ∈ MSet{s})


Proof




Definitions occuring in Statement :  mset_union: a ⋃ b null_mset: 0{s} mset: MSet{s} all: x:A. B[x] equal: t ∈ T dset: DSet
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q squash: T uall: [x:A]. B[x] prop: dset: DSet so_lambda: λ2x.t[x] subtype_rel: A ⊆B nat: true: True so_apply: x[s] uimplies: supposing a guard: {T} null_mset: 0{s} mset_count: #∈ a top: Top bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  decidable: Dec(P) or: P ∨ Q ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A bfalse: ff
Lemmas referenced :  eq_mset_iff_eq_counts mset_union_wf null_mset_wf all_wf squash_wf true_wf set_car_wf equal_wf mset_count_union mset_count_wf nat_wf iff_weakening_equal mset_wf dset_wf count_nil_lemma imax_unfold le_int_wf bool_wf uiff_transitivity equal-wf-T-base assert_wf le_wf eqtt_to_assert assert_of_le_int decidable__equal_int nat_properties satisfiable-full-omega-tt intformand_wf intformle_wf itermConstant_wf itermVar_wf intformnot_wf intformeq_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_formula_prop_eq_lemma int_formula_prop_wf lt_int_wf less_than_wf bnot_wf eqff_to_assert assert_functionality_wrt_uiff bnot_of_le_int assert_of_lt_int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis productElimination independent_functionElimination applyEquality lambdaEquality imageElimination isectElimination equalityTransitivity equalitySymmetry functionEquality cumulativity universeEquality setElimination rename sqequalRule because_Cache intEquality natural_numberEquality imageMemberEquality baseClosed independent_isectElimination isect_memberEquality voidElimination voidEquality unionElimination equalityElimination applyLambdaEquality dependent_pairFormation int_eqEquality independent_pairFormation computeAll

Latex:
\mforall{}s:DSet.  \mforall{}a:MSet\{s\}.    ((a  \mcup{}  0\{s\})  =  a)



Date html generated: 2017_10_01-AM-09_59_59
Last ObjectModification: 2017_03_03-PM-01_00_59

Theory : mset


Home Index