Nuprl Lemma : member-iseg-sorted-by

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


Definitions occuring in Statement :  sorted-by: sorted-by(R;L) iseg: l1 ≤ l2 last: last(L) l_member: (x ∈ l) null: null(as) list: List irrefl: Irrefl(T;x,y.E[x; y]) anti_sym: AntiSym(T;x,y.R[x; y]) assert: b uimplies: supposing a uall: [x:A]. B[x] prop: all: x:A. B[x] iff: ⇐⇒ Q not: ¬A implies:  Q or: P ∨ Q and: P ∧ Q apply: a function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] uimplies: supposing a member: t ∈ T irrefl: Irrefl(T;x,y.E[x; y]) not: ¬A implies:  Q false: False anti_sym: AntiSym(T;x,y.R[x; y]) iff: ⇐⇒ Q and: P ∧ Q prop: rev_implies:  Q or: P ∨ Q subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] istype: istype(T) so_lambda: λ2y.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 ≥  guard: {T} sq_type: SQType(T) decidable: Dec(P) nat: cand: c∧ B exists: x:A. B[x] l_member: (x ∈ l) sorted-by: sorted-by(R;L) true: True assert: b ifthenelse: if then else 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

\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