### Nuprl Lemma : comparison-sort-permutation

`∀T:Type. (valueall-type(T) `` (∀cmp:comparison(T). ∀L:T List.  permutation(T;comparison-sort(cmp;L);L)))`

Proof

Definitions occuring in Statement :  comparison-sort: `comparison-sort(cmp;L)` comparison: `comparison(T)` permutation: `permutation(T;L1;L2)` list: `T List` valueall-type: `valueall-type(T)` all: `∀x:A. B[x]` implies: `P `` Q` universe: `Type`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` comparison-sort: `comparison-sort(cmp;L)` uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` prop: `ℙ` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a` so_apply: `x[s]` subtype_rel: `A ⊆r B` top: `Top` eager-accum: `eager-accum(x,a.f[x; a];y;l)` list_ind: list_ind nil: `[]` it: `⋅` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` callbyvalueall: callbyvalueall has-value: `(a)↓` has-valueall: `has-valueall(a)` append: `as @ bs` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q`
Lemmas referenced :  list_induction all_wf list_wf permutation_wf eager-accum_wf insert-no-combine_wf list-valueall-type append_wf append-nil subtype_rel_list top_wf list_ind_cons_lemma valueall-type-has-valueall evalall-reduce comparison_wf valueall-type_wf cons_wf nil_wf insert-no-combine-permutation permutation-nil permutation_functionality_wrt_permutation permutation_weakening permutation-rotate append_functionality_wrt_permutation append_assoc list_ind_nil_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut thin lemma_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality cumulativity hypothesis because_Cache functionEquality independent_isectElimination independent_functionElimination applyEquality isect_memberEquality voidElimination voidEquality rename dependent_functionElimination callbyvalueReduce universeEquality productElimination

Latex:
\mforall{}T:Type
(valueall-type(T)  {}\mRightarrow{}  (\mforall{}cmp:comparison(T).  \mforall{}L:T  List.    permutation(T;comparison-sort(cmp;L);L)))

Date html generated: 2016_05_14-PM-02_44_11
Last ObjectModification: 2015_12_26-PM-02_41_17

Theory : list_1

Home Index