### Nuprl Lemma : bag-union-append

`∀[A:Type]. ∀[b1,b2:bag(bag(A))].  (bag-union(b1 + b2) = (bag-union(b1) + bag-union(b2)) ∈ bag(A))`

Proof

Definitions occuring in Statement :  bag-union: `bag-union(bbs)` bag-append: `as + bs` bag: `bag(T)` uall: `∀[x:A]. B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` squash: `↓T` prop: `ℙ` all: `∀x:A. B[x]` true: `True` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q`
Lemmas referenced :  equal_wf squash_wf true_wf bag_wf bag-append-union bag-append_wf bag-union_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry universeEquality dependent_functionElimination cumulativity because_Cache natural_numberEquality sqequalRule imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination isect_memberEquality axiomEquality

Latex:
\mforall{}[A:Type].  \mforall{}[b1,b2:bag(bag(A))].    (bag-union(b1  +  b2)  =  (bag-union(b1)  +  bag-union(b2)))

Date html generated: 2017_10_01-AM-08_47_01
Last ObjectModification: 2017_07_26-PM-04_31_42

Theory : bags

Home Index