Nuprl Lemma : sorted-by-nil

`∀[R:Top]. uiff(sorted-by(R;[]);True)`

Proof

Definitions occuring in Statement :  sorted-by: `sorted-by(R;L)` nil: `[]` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` top: `Top` true: `True`
Definitions unfolded in proof :  sorted-by: `sorted-by(R;L)` uall: `∀[x:A]. B[x]` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` member: `t ∈ T` true: `True` prop: `ℙ` so_lambda: `λ2x.t[x]` int_seg: `{i..j-}` select: `L[n]` all: `∀x:A. B[x]` nil: `[]` it: `⋅` so_lambda: `λ2x y.t[x; y]` top: `Top` so_apply: `x[s1;s2]` guard: `{T}` lelt: `i ≤ j < k` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` implies: `P `` Q` not: `¬A` so_apply: `x[s]`
Lemmas referenced :  top_wf true_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 base_wf stuck-spread length_of_nil_lemma nil_wf length_wf int_seg_wf all_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation independent_pairFormation introduction cut natural_numberEquality sqequalHypSubstitution axiomEquality equalityTransitivity hypothesis equalitySymmetry lemma_by_obid isectElimination thin voidEquality because_Cache lambdaEquality setElimination rename hypothesisEquality baseClosed independent_isectElimination lambdaFormation isect_memberEquality voidElimination productElimination dependent_pairFormation int_eqEquality intEquality dependent_functionElimination computeAll

Latex:
\mforall{}[R:Top].  uiff(sorted-by(R;[]);True)

Date html generated: 2016_05_14-PM-01_46_55
Last ObjectModification: 2016_01_15-AM-08_19_30

Theory : list_1

Home Index