### Nuprl Lemma : cpsquicksort-quicksort

`∀[T:Type]`
`  ∀[A:Type]. ∀[cmp:comparison(T)].  ∀L:T List. ∀[k:(T List) ⟶ A]. (cpsquicksort(cmp;L;k) ~ k quicksort(cmp;L)) `
`  supposing valueall-type(T)`

Proof

Definitions occuring in Statement :  cpsquicksort: `cpsquicksort(cmp;L;k)` quicksort: `quicksort(cmp;L)` 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]` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` all: `∀x:A. B[x]` nat: `ℕ` implies: `P `` Q` false: `False` ge: `i ≥ j ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` not: `¬A` top: `Top` and: `P ∧ Q` prop: `ℙ` guard: `{T}` int_seg: `{i..j-}` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` subtype_rel: `A ⊆r B` le: `A ≤ B` less_than': `less_than'(a;b)` less_than: `a < b` squash: `↓T` cpsquicksort: `cpsquicksort(cmp;L;k)` quicksort: `quicksort(cmp;L)` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` bfalse: `ff` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` cons: `[a / b]` sq_stable: `SqStable(P)` subtract: `n - m` true: `True` callbyvalueall: callbyvalueall listp: `A List+` has-value: `(a)↓` has-valueall: `has-valueall(a)` comparison: `comparison(T)` let: let cand: `A c∧ B` l_exists: `(∃x∈L. P[x])` equiv_rel: `EquivRel(T;x,y.E[x; y])` sq_type: `SQType(T)` lt_int: `i <z j` assert: `↑b` refl: `Refl(T;x,y.E[x; y])`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation thin extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality hypothesis setElimination rename intWeakElimination natural_numberEquality independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation computeAll independent_functionElimination sqequalAxiom functionEquality cumulativity because_Cache productElimination unionElimination applyEquality equalityTransitivity equalitySymmetry applyLambdaEquality hypothesis_subsumption dependent_set_memberEquality imageElimination equalityElimination baseClosed impliesFunctionality promote_hyp addEquality imageMemberEquality minusEquality callbyvalueReduce setEquality instantiate hyp_replacement productEquality universeEquality functionExtensionality

Latex:
\mforall{}[T:Type]
\mforall{}[A:Type].  \mforall{}[cmp:comparison(T)].
\mforall{}L:T  List.  \mforall{}[k:(T  List)  {}\mrightarrow{}  A].  (cpsquicksort(cmp;L;k)  \msim{}  k  quicksort(cmp;L))
supposing  valueall-type(T)

Date html generated: 2018_05_21-PM-07_34_57
Last ObjectModification: 2017_07_26-PM-05_09_12

Theory : general

Home Index