Nuprl Lemma : strict4-bag-combine
strict4(λx,y,z,w. ⋃b∈x.y[b])
Proof
Definitions occuring in Statement :
bag-combine: ⋃x∈bs.f[x],
strict4: strict4(F),
so_apply: x[s],
lambda: λx.A[x]
Definitions unfolded in proof :
bag-combine: ⋃x∈bs.f[x],
bag-map: bag-map(f;bs),
bag-union: bag-union(bbs)
Lemmas referenced :
strict4-concat-map
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
lemma_by_obid,
hypothesis
Latex:
strict4(\mlambda{}x,y,z,w. \mcup{}b\mmember{}x.y[b])
Date html generated:
2016_05_15-PM-02_28_06
Last ObjectModification:
2015_12_27-AM-09_51_01
Theory : bags
Home
Index