Nuprl Lemma : bag-bind-assoc

[A,B,C:Type]. ∀[f:A ⟶ bag(B)]. ∀[g:B ⟶ bag(C)]. ∀[bs:bag(A)].
  (bag-bind(bag-bind(bs;f);g) bag-bind(bs;λa.bag-bind(f a;g)) ∈ bag(C))


Proof




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

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[f:A  {}\mrightarrow{}  bag(B)].  \mforall{}[g:B  {}\mrightarrow{}  bag(C)].  \mforall{}[bs:bag(A)].
    (bag-bind(bag-bind(bs;f);g)  =  bag-bind(bs;\mlambda{}a.bag-bind(f  a;g)))



Date html generated: 2019_10_15-AM-11_05_44
Last ObjectModification: 2018_10_09-AM-10_52_35

Theory : bags


Home Index