### Nuprl Lemma : quicksort_wf

`∀[T:Type]. ∀[cmp:comparison(T)].`
`  ∀L:T List. (quicksort(cmp;L) ∈ {srtd:T List| sorted-by(λx,y. (0 ≤ (cmp x y));srtd) ∧ permutation(T;srtd;L)} ) supposin\000Cg valueall-type(T)`

Proof

Definitions occuring in Statement :  quicksort: `quicksort(cmp;L)` comparison: `comparison(T)` permutation: `permutation(T;L1;L2)` sorted-by: `sorted-by(R;L)` list: `T List` valueall-type: `valueall-type(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` le: `A ≤ B` all: `∀x:A. B[x]` and: `P ∧ Q` member: `t ∈ T` set: `{x:A| B[x]} ` apply: `f a` lambda: `λx.A[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` bfalse: `ff` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` quicksort: `quicksort(cmp;L)` squash: `↓T` less_than: `a < b` less_than': `less_than'(a;b)` le: `A ≤ B` subtype_rel: `A ⊆r B` or: `P ∨ Q` decidable: `Dec(P)` lelt: `i ≤ j < k` int_seg: `{i..j-}` guard: `{T}` prop: `ℙ` and: `P ∧ Q` top: `Top` not: `¬A` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` ge: `i ≥ j ` false: `False` implies: `P `` Q` nat: `ℕ` comparison: `comparison(T)` true: `True` rev_uimplies: `rev_uimplies(P;Q)` cand: `A c∧ B` has-valueall: `has-valueall(a)` has-value: `(a)↓` listp: `A List+` callbyvalueall: callbyvalueall subtract: `n - m` sq_stable: `SqStable(P)` cons: `[a / b]` refl: `Refl(T;x,y.E[x; y])` assert: `↑b` lt_int: `i <z j` sq_type: `SQType(T)` equiv_rel: `EquivRel(T;x,y.E[x; y])` so_apply: `x[s]` so_lambda: `λ2x.t[x]` sorted-by: `sorted-by(R;L)` trans: `Trans(T;x,y.E[x; y])` sym: `Sym(T;x,y.E[x; y])` nequal: `a ≠ b ∈ T ` band: `p ∧b q`
Rules used in proof :  universeEquality isect_memberEquality because_Cache equalitySymmetry equalityTransitivity axiomEquality dependent_functionElimination lambdaEquality sqequalRule hypothesisEquality cumulativity thin isectElimination extract_by_obid hypothesis sqequalHypSubstitution lambdaFormation cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution addEquality impliesFunctionality baseClosed equalityElimination imageElimination dependent_set_memberEquality hypothesis_subsumption applyLambdaEquality applyEquality unionElimination productElimination independent_functionElimination computeAll independent_pairFormation voidEquality voidElimination intEquality int_eqEquality dependent_pairFormation independent_isectElimination natural_numberEquality intWeakElimination rename setElimination setEquality productEquality callbyvalueReduce minusEquality imageMemberEquality promote_hyp instantiate addLevel levelHypothesis functionEquality impliesLevelFunctionality allLevelFunctionality allFunctionality functionExtensionality closedConclusion baseApply pointwiseFunctionality hyp_replacement lambdaEquality_alt universeIsType inhabitedIsType functionExtensionality_alt lambdaFormation_alt approximateComputation dependent_pairFormation_alt Error :memTop,  equalityIstype sqequalBase productIsType isect_memberEquality_alt setIsType

Latex:
\mforall{}[T:Type].  \mforall{}[cmp:comparison(T)].
\mforall{}L:T  List
(quicksort(cmp;L)  \mmember{}  \{srtd:T  List|  sorted-by(\mlambda{}x,y.  (0  \mleq{}  (cmp  x  y));srtd)  \mwedge{}  permutation(T;srtd;L)\}\000C  )
supposing  valueall-type(T)

Date html generated: 2020_05_20-AM-08_09_03
Last ObjectModification: 2020_01_08-PM-01_55_15

Theory : general

Home Index