Nuprl Lemma : bag-bind-append2

[A,B:Type]. ∀[F,G:A ⟶ bag(B)]. ∀[ba:bag(A)].
  (bag-bind(ba;λa.((F a) (G a))) (bag-bind(ba;F) bag-bind(ba;G)) ∈ bag(B))


Proof




Definitions occuring in Statement :  bag-bind: bag-bind(bs;f) bag-append: as bs bag: bag(T) uall: [x:A]. B[x] apply: a lambda: λx.A[x] function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T bag: bag(T) quotient: x,y:A//B[x; y] and: P ∧ Q subtype_rel: A ⊆B squash: T true: True prop: uimplies: supposing a implies:  Q all: x:A. B[x] empty-bag: {} so_apply: x[s1;s2;s3] so_lambda: so_lambda(x,y,z.t[x; y; z]) append: as bs concat: concat(ll) top: Top bag-union: bag-union(bbs) bag-map: bag-map(f;bs) bag-append: as bs bag-bind: bag-bind(bs;f) so_apply: x[s] so_lambda: λ2x.t[x] rev_implies:  Q iff: ⇐⇒ Q guard: {T}
Lemmas referenced :  bag_wf bag-bind_wf subtype_rel_self bag-append_wf equal_wf list-subtype-bag istype-universe list_wf permutation_wf reduce_cons_lemma map_cons_lemma empty-bag_wf list_ind_nil_lemma reduce_nil_lemma map_nil_lemma list_induction iff_weakening_equal bag-append-ac true_wf squash_wf bag-append-assoc2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalHypSubstitution pointwiseFunctionalityForEquality extract_by_obid isectElimination thin hypothesisEquality hypothesis sqequalRule pertypeElimination productElimination rename equalitySymmetry dependent_set_memberEquality_alt independent_pairFormation equalityTransitivity productIsType equalityIsType1 inhabitedIsType applyLambdaEquality setElimination applyEquality because_Cache lambdaEquality_alt imageElimination universeIsType universeEquality natural_numberEquality imageMemberEquality baseClosed hyp_replacement independent_isectElimination equalityIsType4 isect_memberEquality_alt axiomEquality functionIsType independent_functionElimination dependent_functionElimination lambdaFormation cumulativity voidEquality voidElimination isect_memberEquality functionExtensionality lambdaEquality levelHypothesis equalityUniverse

Latex:
\mforall{}[A,B:Type].  \mforall{}[F,G:A  {}\mrightarrow{}  bag(B)].  \mforall{}[ba:bag(A)].
    (bag-bind(ba;\mlambda{}a.((F  a)  +  (G  a)))  =  (bag-bind(ba;F)  +  bag-bind(ba;G)))



Date html generated: 2019_10_15-AM-11_05_53
Last ObjectModification: 2018_10_09-AM-10_52_22

Theory : bags


Home Index