### Nuprl Lemma : bag-function

`∀[T,A:Type]. ∀[f:(T List) ⟶ bag(A)].`
`  f ∈ bag(T) ⟶ bag(A) supposing ∀as,bs:T List.  (f[as @ bs] = (f[as] + f[bs]) ∈ bag(A))`

Proof

Definitions occuring in Statement :  bag-append: `as + bs` bag: `bag(T)` append: `as @ bs` list: `T List` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  member: `t ∈ T` squash: `↓T` uall: `∀[x:A]. B[x]` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` 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` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` top: `Top` so_apply: `x[s1;s2;s3]` bag: `bag(T)` quotient: `x,y:A//B[x; y]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` trans: `Trans(T;x,y.E[x; y])` refl: `Refl(T;x,y.E[x; y])`
Lemmas referenced :  all_wf squash_wf true_wf list_wf equal_wf bag_wf cons_wf nil_wf iff_weakening_equal list_ind_cons_lemma list_ind_nil_lemma permutation-invariant2 bag-append_wf bag-append-assoc-comm equal-wf-base permutation_wf bag-append-comm append_wf
Rules used in proof :  cut applyEquality thin sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaEquality sqequalHypSubstitution imageElimination introduction extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry functionEquality cumulativity universeEquality because_Cache sqequalRule functionExtensionality dependent_functionElimination natural_numberEquality imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination lambdaFormation isect_memberEquality voidElimination voidEquality pointwiseFunctionalityForEquality pertypeElimination productEquality isect_memberFormation axiomEquality

Latex:
\mforall{}[T,A:Type].  \mforall{}[f:(T  List)  {}\mrightarrow{}  bag(A)].
f  \mmember{}  bag(T)  {}\mrightarrow{}  bag(A)  supposing  \mforall{}as,bs:T  List.    (f[as  @  bs]  =  (f[as]  +  f[bs]))

Date html generated: 2017_10_01-AM-08_45_09
Last ObjectModification: 2017_07_26-PM-04_30_34

Theory : bags

Home Index