Nuprl Lemma : mset_union_comm

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


Proof




Definitions occuring in Statement :  mset_union: a ⋃ b 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] true: True so_apply: x[s] subtype_rel: A ⊆B uimplies: supposing a guard: {T} nat:
Lemmas referenced :  nat_wf mset_count_wf imax_com dset_wf mset_wf iff_weakening_equal mset_count_union equal_wf set_car_wf true_wf squash_wf all_wf mset_union_wf eq_mset_iff_eq_counts
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_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

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



Date html generated: 2016_05_16-AM-07_49_19
Last ObjectModification: 2016_01_16-PM-11_39_41

Theory : mset


Home Index