Nuprl Lemma : bag-bind-com

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


Proof




Definitions occuring in Statement :  bag-bind: bag-bind(bs;f) bag: bag(T) uall: [x:A]. B[x] so_apply: x[s1;s2] 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 prop: all: x:A. B[x] implies:  Q so_apply: x[s1;s2] subtype_rel: A ⊆B uimplies: supposing a so_lambda: λ2x.t[x] so_apply: x[s] bag-map: bag-map(f;bs) bag-union: bag-union(bbs) top: Top concat: concat(ll) empty-bag: {} bag-append: as bs true: True squash: T guard: {T} iff: ⇐⇒ Q rev_implies:  Q so_lambda: λ2y.t[x; y]
Lemmas referenced :  bag_wf equal-wf-base list_wf permutation_wf equal_wf bag-union_wf bag-map_wf list-subtype-bag list_induction map_nil_lemma reduce_nil_lemma bag-bind-empty-right empty-bag_wf map_cons_lemma reduce_cons_lemma bag-append_wf squash_wf true_wf iff_weakening_equal bag-bind-append2 bag-bind_wf quotient-member-eq permutation-equiv and_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution pointwiseFunctionalityForEquality extract_by_obid isectElimination thin cumulativity hypothesisEquality hypothesis pertypeElimination productElimination productEquality because_Cache isect_memberEquality axiomEquality functionEquality equalityTransitivity equalitySymmetry lambdaFormation rename dependent_functionElimination independent_functionElimination hyp_replacement applyLambdaEquality lambdaEquality applyEquality functionExtensionality independent_isectElimination voidElimination voidEquality equalityUniverse levelHypothesis natural_numberEquality imageElimination universeEquality imageMemberEquality baseClosed dependent_set_memberEquality independent_pairFormation setElimination

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



Date html generated: 2017_10_01-AM-09_06_10
Last ObjectModification: 2017_07_26-PM-04_46_20

Theory : bags


Home Index