### Nuprl Lemma : no-repeats-bag-partitions

`∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].`
`  bag-no-repeats(bag(T) × bag(T);bag-partitions(eq;bs)) supposing valueall-type(T)`

Proof

Definitions occuring in Statement :  bag-partitions: `bag-partitions(eq;bs)` bag-no-repeats: `bag-no-repeats(T;bs)` bag: `bag(T)` deq: `EqDecider(T)` valueall-type: `valueall-type(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` product: `x:A × B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` bag-partitions: `bag-partitions(eq;bs)` callbyvalueall: callbyvalueall all: `∀x:A. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` implies: `P `` Q` has-value: `(a)↓` has-valueall: `has-valueall(a)` bag-no-repeats: `bag-no-repeats(T;bs)` squash: `↓T` product-deq: `product-deq(A;B;a;b)`
Lemmas referenced :  bag-deq_wf product-deq_wf no-repeats-bag-to-set valueall-type-has-valueall deq_wf valueall-type_wf product-valueall-type bag-valueall-type bag-splits_wf bag_wf evalall-reduce
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule callbyvalueReduce lemma_by_obid sqequalHypSubstitution isectElimination thin productEquality hypothesisEquality hypothesis dependent_functionElimination independent_isectElimination because_Cache lambdaEquality independent_functionElimination lambdaFormation imageElimination imageMemberEquality baseClosed isect_memberEquality equalityTransitivity equalitySymmetry universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].
bag-no-repeats(bag(T)  \mtimes{}  bag(T);bag-partitions(eq;bs))  supposing  valueall-type(T)

Date html generated: 2016_05_15-PM-08_05_57
Last ObjectModification: 2016_01_16-PM-01_28_14

Theory : bags_2

Home Index