Nuprl Lemma : bag-append-assoc-comm

`∀[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 :  top: `Top` member: `t ∈ T` squash: `↓T` uall: `∀[x:A]. B[x]` 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-append_wf squash_wf true_wf equal_wf bag_wf bag-append-comm iff_weakening_equal bag-append-assoc
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberEquality voidElimination voidEquality cut applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination introduction extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry because_Cache cumulativity natural_numberEquality sqequalRule imageMemberEquality baseClosed universeEquality independent_isectElimination productElimination independent_functionElimination isect_memberFormation axiomEquality

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_03
Last ObjectModification: 2017_07_26-PM-04_30_29

Theory : bags

Home Index