### Nuprl Lemma : bag-append-ac

`∀[T:Type]. ∀[as,bs,cs:bag(T)].  ((as + bs + cs) = (bs + as + cs) ∈ bag(T))`

Proof

Definitions occuring in Statement :  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` top: `Top` squash: `↓T` prop: `ℙ` 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 :  bag_wf bag-append-assoc equal_wf squash_wf true_wf bag-append_wf bag-append-comm iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality sqequalRule isect_memberEquality axiomEquality because_Cache universeEquality voidElimination voidEquality applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry natural_numberEquality imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs,cs:bag(T)].    ((as  +  bs  +  cs)  =  (bs  +  as  +  cs))

Date html generated: 2017_10_01-AM-08_45_06
Last ObjectModification: 2017_07_26-PM-04_30_33

Theory : bags

Home Index