### Nuprl Lemma : bag-to-list_wf

`∀[T:Type]`
`  ∀[b:bag(T)]. ∀[cmp:comparison({x:T| x ↓∈ b} )].`
`    bag-to-list(cmp;b) ∈ T List supposing ∀x,y:{x:T| x ↓∈ b} .  (((cmp x y) = 0 ∈ ℤ) `` (x = y ∈ T)) `
`  supposing valueall-type(T)`

Proof

Definitions occuring in Statement :  bag-to-list: `bag-to-list(cmp;b)` bag-member: `x ↓∈ bs` bag: `bag(T)` comparison: `comparison(T)` list: `T List` valueall-type: `valueall-type(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` set: `{x:A| B[x]} ` apply: `f a` natural_number: `\$n` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` bag: `bag(T)` quotient: `x,y:A//B[x; y]` and: `P ∧ Q` all: `∀x:A. B[x]` implies: `P `` Q` guard: `{T}` ext-eq: `A ≡ B` subtype_rel: `A ⊆r B` uiff: `uiff(P;Q)` squash: `↓T` prop: `ℙ` linorder: `Linorder(T;x,y.R[x; y])` order: `Order(T;x,y.R[x; y])` cand: `A c∧ B` comparison: `comparison(T)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` bag-to-list: `bag-to-list(cmp;b)` le: `A ≤ B` sorted-by: `sorted-by(R;L)` int_seg: `{i..j-}` sq_stable: `SqStable(P)` not: `¬A` false: `False`
Lemmas referenced :  list_wf member-permutation bag-member-iff-sq-list-member l_member_wf bag-member_wf list-subtype-bag comparison-refl comparison-trans comparison-antisym equal-wf-T-base set_wf comparison-connex subtype_rel_comparison ext-eq_inversion subtype_rel_weakening equal-wf-base permutation_wf all_wf equal_wf comparison_wf bag_wf valueall-type_wf list-subtype subtype_rel_list permutation-sorted-by-unique le_wf comparison-sort_wf set-valueall-type sorted-by_wf sq_stable__all int_seg_wf length_wf sq_stable__le less_than'_wf squash_wf comparison-sort-permutation permutation_functionality_wrt_permutation permutation-strong-subtype strong-subtype-set2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution pointwiseFunctionalityForEquality extract_by_obid isectElimination thin cumulativity hypothesisEquality hypothesis sqequalRule pertypeElimination productElimination dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination because_Cache independent_pairFormation lambdaEquality setElimination rename independent_isectElimination imageElimination dependent_set_memberEquality setEquality applyEquality imageMemberEquality baseClosed lambdaFormation intEquality promote_hyp productEquality axiomEquality functionEquality isect_memberEquality universeEquality natural_numberEquality independent_pairEquality voidElimination

Latex:
\mforall{}[T:Type]
\mforall{}[b:bag(T)].  \mforall{}[cmp:comparison(\{x:T|  x  \mdownarrow{}\mmember{}  b\}  )].
bag-to-list(cmp;b)  \mmember{}  T  List  supposing  \mforall{}x,y:\{x:T|  x  \mdownarrow{}\mmember{}  b\}  .    (((cmp  x  y)  =  0)  {}\mRightarrow{}  (x  =  y))
supposing  valueall-type(T)

Date html generated: 2017_10_01-AM-08_56_53
Last ObjectModification: 2017_07_26-PM-04_39_08

Theory : bags

Home Index