### Nuprl Lemma : insert-no-combine-sorted-by

`∀[T:Type]`
`  ∀cmp:comparison(T)`
`    ((∀u,x,z:T.  ((0 ≤ (cmp x u)) `` (0 ≤ (cmp u z)) `` (0 ≤ (cmp x z))))`
`    `` (∀L:T List. ∀x:T.  (sorted-by(λx,y. (0 ≤ (cmp x y));L) `` sorted-by(λx,y. (0 ≤ (cmp x y));insert-no-combine(cmp;x\000C;L)))))`

Proof

Definitions occuring in Statement :  insert-no-combine: `insert-no-combine(cmp;x;l)` comparison: `comparison(T)` sorted-by: `sorted-by(R;L)` list: `T List` uall: `∀[x:A]. B[x]` le: `A ≤ B` all: `∀x:A. B[x]` implies: `P `` Q` apply: `f a` lambda: `λx.A[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  so_apply: `x[s]` comparison: `comparison(T)` prop: `ℙ` so_lambda: `λ2x.t[x]` member: `t ∈ T` implies: `P `` Q` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` le: `A ≤ B` false: `False` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` and: `P ∧ Q` lelt: `i ≤ j < k` int_seg: `{i..j-}` guard: `{T}` so_apply: `x[s1;s2;s3]` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2]` top: `Top` so_lambda: `λ2x y.t[x; y]` it: `⋅` nil: `[]` uimplies: `b supposing a` select: `L[n]` sorted-by: `sorted-by(R;L)` insert-no-combine: `insert-no-combine(cmp;x;l)` assert: `↑b` bnot: `¬bb` sq_type: `SQType(T)` or: `P ∨ Q` bfalse: `ff` cand: `A c∧ B` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` btrue: `tt` unit: `Unit` bool: `𝔹` squash: `↓T` less_than: `a < b` decidable: `Dec(P)` l_all: `(∀x∈L.P[x])` subtype_rel: `A ⊆r B` true: `True` sq_stable: `SqStable(P)`
Lemmas referenced :  comparison_wf list_wf insert-no-combine_wf le_wf l_member_wf sorted-by_wf all_wf list_induction int_seg_wf nil_wf cons_wf select_wf less_than'_wf int_formula_prop_wf int_term_value_constant_lemma int_formula_prop_le_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_and_lemma itermConstant_wf intformle_wf itermVar_wf intformless_wf intformand_wf full-omega-unsat int_seg_properties length_of_cons_lemma list_ind_nil_lemma base_wf stuck-spread length_of_nil_lemma assert-bnot bool_subtype_base subtype_base_sq bool_cases_sqequal equal_wf eqff_to_assert sorted-by-cons assert_of_le_int eqtt_to_assert bool_wf le_int_wf list_ind_cons_lemma decidable__lt int_formula_prop_not_lemma intformnot_wf satisfiable-full-omega-tt decidable__le length_wf l_all_cons cons_member member-insert-no-combine l_all_iff int_term_value_minus_lemma itermMinus_wf iff_weakening_equal true_wf squash_wf sq_stable__le
Rules used in proof :  universeEquality independent_functionElimination dependent_functionElimination setEquality applyEquality natural_numberEquality rename setElimination hypothesis because_Cache functionEquality cumulativity lambdaEquality sqequalRule hypothesisEquality isectElimination sqequalHypSubstitution extract_by_obid introduction thin cut lambdaFormation isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution equalitySymmetry equalityTransitivity axiomEquality independent_pairEquality independent_pairFormation intEquality int_eqEquality dependent_pairFormation approximateComputation productElimination voidEquality voidElimination isect_memberEquality independent_isectElimination baseClosed instantiate promote_hyp equalityElimination unionElimination imageElimination computeAll applyLambdaEquality hyp_replacement minusEquality imageMemberEquality functionExtensionality

Latex:
\mforall{}[T:Type]
\mforall{}cmp:comparison(T)
((\mforall{}u,x,z:T.    ((0  \mleq{}  (cmp  x  u))  {}\mRightarrow{}  (0  \mleq{}  (cmp  u  z))  {}\mRightarrow{}  (0  \mleq{}  (cmp  x  z))))
{}\mRightarrow{}  (\mforall{}L:T  List.  \mforall{}x:T.
(sorted-by(\mlambda{}x,y.  (0  \mleq{}  (cmp  x  y));L)
{}\mRightarrow{}  sorted-by(\mlambda{}x,y.  (0  \mleq{}  (cmp  x  y));insert-no-combine(cmp;x;L)))))

Date html generated: 2018_05_21-PM-00_43_57
Last ObjectModification: 2018_05_18-PM-04_18_29

Theory : list_1

Home Index