Nuprl Lemma : bag-splits_wf

T:Type. ∀b:bag(T).  (bag-splits(b) ∈ bag(bag(T) × bag(T)))


Proof




Definitions occuring in Statement :  bag-splits: bag-splits(b) bag: bag(T) all: x:A. B[x] member: t ∈ T product: x:A × B[x] universe: Type
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T bag: bag(T) uall: [x:A]. B[x] quotient: x,y:A//B[x; y] and: P ∧ Q so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] uimplies: supposing a implies:  Q prop:
Lemmas referenced :  bag_wf quotient-member-eq list_wf permutation_wf permutation-equiv bag-splits_wf_list bag-splits-permutation equal-wf-base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalHypSubstitution pointwiseFunctionalityForEquality lemma_by_obid isectElimination thin productEquality hypothesisEquality hypothesis sqequalRule pertypeElimination productElimination lambdaEquality independent_isectElimination dependent_functionElimination independent_functionElimination equalityTransitivity equalitySymmetry because_Cache cumulativity universeEquality

Latex:
\mforall{}T:Type.  \mforall{}b:bag(T).    (bag-splits(b)  \mmember{}  bag(bag(T)  \mtimes{}  bag(T)))



Date html generated: 2016_05_15-PM-02_53_16
Last ObjectModification: 2015_12_27-AM-09_32_00

Theory : bags


Home Index