Nuprl Lemma : quicksort-int_wf

L:ℤ List. (quicksort-int(L) ∈ {srtd:ℤ List| sorted-by(λx,y. (x ≤ y);srtd) ∧ permutation(ℤ;srtd;L)} )

Proof

Definitions occuring in Statement :  quicksort-int: quicksort-int(L) permutation: permutation(T;L1;L2) sorted-by: sorted-by(R;L) list: List le: A ≤ B all: x:A. B[x] and: P ∧ Q member: t ∈ T set: {x:A| B[x]}  lambda: λx.A[x] int:
Definitions unfolded in proof :  all: x:A. B[x] quicksort-int: quicksort-int(L) uall: [x:A]. B[x] member: t ∈ T comparison: comparison(T) and: P ∧ Q cand: c∧ B decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False implies:  Q not: ¬A top: Top prop: so_lambda: λ2x.t[x] so_apply: x[s] squash: T sorted-by: sorted-by(R;L) guard: {T} int_seg: {i..j-} lelt: i ≤ j < k less_than: a < b le: A ≤ B uiff: uiff(P;Q)
Lemmas referenced :  length_wf int_seg_wf false_wf subtract-is-int-iff int_formula_prop_less_lemma intformless_wf decidable__lt select_wf int_seg_properties permutation_wf l_member_wf sorted-by_wf and_wf list_wf int-valueall-type equal-wf-T-base all_wf le_wf int_formula_prop_le_lemma intformle_wf decidable__le equal_wf int_term_value_constant_lemma int_formula_prop_and_lemma itermConstant_wf intformand_wf int_formula_prop_wf int_term_value_minus_lemma int_term_value_var_lemma int_term_value_subtract_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma itermMinus_wf itermVar_wf itermSubtract_wf intformeq_wf intformnot_wf satisfiable-full-omega-tt decidable__equal_int subtract_wf quicksort_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin intEquality dependent_set_memberEquality lambdaEquality hypothesisEquality hypothesis sqequalRule dependent_functionElimination because_Cache unionElimination natural_numberEquality independent_isectElimination dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality computeAll independent_pairFormation productEquality applyEquality minusEquality functionEquality baseClosed setElimination rename imageMemberEquality setEquality introduction imageElimination equalityTransitivity equalitySymmetry productElimination pointwiseFunctionality promote_hyp baseApply closedConclusion

Latex:
\mforall{}L:\mBbbZ{}  List.  (quicksort-int(L)  \mmember{}  \{srtd:\mBbbZ{}  List|  sorted-by(\mlambda{}x,y.  (x  \mleq{}  y);srtd)  \mwedge{}  permutation(\mBbbZ{};srtd;L)\}  \000C)

Date html generated: 2016_05_15-PM-04_29_46
Last ObjectModification: 2016_01_16-AM-11_14_38

Theory : general

Home Index