### Nuprl Lemma : member-iseg-sorted-by

`∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].`
`  ∀sa,sb:T List.`
`    (sa ≤ sb`
`       `` sorted-by(R;sb)`
`       `` (∀x:T. ((x ∈ sa) `⇐⇒` (¬↑null(sa)) ∧ (x ∈ sb) ∧ ((x = last(sa) ∈ T) ∨ (R x last(sa)))))) supposing `
`       (AntiSym(T;x,y.R x y) and `
`       Irrefl(T;x,y.R x y))`

Proof

Definitions occuring in Statement :  sorted-by: `sorted-by(R;L)` iseg: `l1 ≤ l2` last: `last(L)` l_member: `(x ∈ l)` null: `null(as)` list: `T List` irrefl: `Irrefl(T;x,y.E[x; y])` anti_sym: `AntiSym(T;x,y.R[x; y])` assert: `↑b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` not: `¬A` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` irrefl: `Irrefl(T;x,y.E[x; y])` not: `¬A` implies: `P `` Q` false: `False` anti_sym: `AntiSym(T;x,y.R[x; y])` iff: `P `⇐⇒` Q` and: `P ∧ Q` prop: `ℙ` rev_implies: `P `` Q` or: `P ∨ Q` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` istype: `istype(T)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` last: `last(L)` lelt: `i ≤ j < k` int_seg: `{i..j-}` top: `Top` satisfiable_int_formula: `satisfiable_int_formula(fmla)` squash: `↓T` less_than: `a < b` ge: `i ≥ j ` guard: `{T}` sq_type: `SQType(T)` decidable: `Dec(P)` nat: `ℕ` cand: `A c∧ B` exists: `∃x:A. B[x]` l_member: `(x ∈ l)` sorted-by: `sorted-by(R;L)` true: `True` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` select: `L[n]` nil: `[]` it: `⋅` cons: `[a / b]` bfalse: `ff` nat_plus: `ℕ+` uiff: `uiff(P;Q)`
Lemmas referenced :  assert_elim null_wf member-implies-null-eq-bfalse btrue_neq_bfalse istype-assert iseg_member l_member_wf istype-void last_wf subtype_rel_self sorted-by_wf subtype_rel_dep_function iseg_wf anti_sym_wf irrefl_wf list_wf istype-universe iseg-sorted-by istype-less_than istype-le int_formula_prop_less_lemma intformless_wf decidable__lt int_formula_prop_wf int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_subtract_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma istype-int intformeq_wf itermVar_wf itermSubtract_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf full-omega-unsat decidable__le nat_properties select_wf int_subtype_base subtype_base_sq length_wf subtract_wf decidable__equal_int last_member iseg_select iff_weakening_equal true_wf squash_wf equal_wf list-cases length_of_nil_lemma null_nil_lemma stuck-spread istype-base product_subtype_list length_of_cons_lemma null_cons_lemma add_nat_plus length_wf_nat nat_plus_properties add-is-int-iff itermAdd_wf int_term_value_add_lemma false_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt cut introduction sqequalRule sqequalHypSubstitution isect_memberEquality_alt isectElimination thin hypothesisEquality lambdaEquality_alt dependent_functionElimination voidElimination functionIsTypeImplies inhabitedIsType isectIsTypeImplies rename axiomEquality hypothesis independent_pairFormation extract_by_obid independent_isectElimination equalityTransitivity equalitySymmetry independent_functionElimination universeIsType productElimination productIsType functionIsType unionIsType equalityIstype applyEquality instantiate universeEquality cumulativity functionEquality setEquality setIsType setElimination because_Cache dependent_set_memberEquality_alt closedConclusion inrFormation_alt int_eqEquality dependent_pairFormation_alt approximateComputation imageElimination intEquality inlFormation_alt unionElimination natural_numberEquality hyp_replacement applyLambdaEquality baseClosed imageMemberEquality Error :memTop,  promote_hyp hypothesis_subsumption pointwiseFunctionality baseApply

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
\mforall{}sa,sb:T  List.
(sa  \mleq{}  sb
{}\mRightarrow{}  sorted-by(R;sb)
{}\mRightarrow{}  (\mforall{}x:T
((x  \mmember{}  sa)  \mLeftarrow{}{}\mRightarrow{}  (\mneg{}\muparrow{}null(sa))  \mwedge{}  (x  \mmember{}  sb)  \mwedge{}  ((x  =  last(sa))  \mvee{}  (R  x  last(sa))))))  supposing
(AntiSym(T;x,y.R  x  y)  and
Irrefl(T;x,y.R  x  y))

Date html generated: 2020_05_19-PM-09_43_12
Last ObjectModification: 2019_12_31-PM-00_12_56

Theory : list_1

Home Index