Nuprl Lemma : sorted-by-single

[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x:T. sorted-by(R;[x])


Proof




Definitions occuring in Statement :  sorted-by: sorted-by(R;L) cons: [a b] nil: [] uall: [x:A]. B[x] prop: all: x:A. B[x] function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] sorted-by: sorted-by(R;L) member: t ∈ T top: Top guard: {T} int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False implies:  Q not: ¬A prop:
Lemmas referenced :  int_seg_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 satisfiable-full-omega-tt int_seg_properties length_of_nil_lemma length_of_cons_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation sqequalHypSubstitution sqequalRule cut lemma_by_obid dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis isectElimination natural_numberEquality setElimination rename hypothesisEquality productElimination independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality independent_pairFormation computeAll functionEquality cumulativity universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}x:T.  sorted-by(R;[x])



Date html generated: 2016_05_14-PM-01_47_18
Last ObjectModification: 2016_01_15-AM-08_18_48

Theory : list_1


Home Index