Nuprl Lemma : iseg-remainder-as-filter

[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[sa,s,sb:T List].
  (∀[dR:T ⟶ T ⟶ 𝔹]
     (sb filter(dR last(sa);s) ∈ (T List)) supposing ((¬↑null(sa)) and (∀x,y:T.  (↑(dR y) ⇐⇒ y)))) supposing 
     (Trans(T;a,b.R b) and 
     sorted-by(R;s) and 
     (s (sa sb) ∈ (T List)) and 
     AntiSym(T;x,y.R y) and 
     Irrefl(T;x,y.R y))


Definitions occuring in Statement :  sorted-by: sorted-by(R;L) last: last(L) null: null(as) filter: filter(P;l) append: as bs list: List irrefl: Irrefl(T;x,y.E[x; y]) anti_sym: AntiSym(T;x,y.R[x; y]) trans: Trans(T;x,y.E[x; y]) assert: b bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] prop: all: x:A. B[x] iff: ⇐⇒ Q not: ¬A apply: a function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] uimplies: supposing a implies:  Q iseg: l1 ≤ l2 exists: x:A. B[x] prop: subtype_rel: A ⊆B top: Top so_lambda: λ2x.t[x] so_apply: x[s] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] not: ¬A false: False guard: {T} irrefl: Irrefl(T;x,y.E[x; y]) set-equal: set-equal(T;x;y) iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q cand: c∧ B or: P ∨ Q l_member: (x ∈ l) squash: T int_seg: {i..j-} nat: lelt: i ≤ j < k ge: i ≥  decidable: Dec(P) satisfiable_int_formula: satisfiable_int_formula(fmla) less_than: a < b true: True subtract: m sq_type: SQType(T) uiff: uiff(P;Q) assert: b ifthenelse: if then else fi  btrue: tt cons: [a b] bfalse: ff le: A ≤ B less_than': less_than'(a;b) last: last(L) sorted-by: sorted-by(R;L) anti_sym: AntiSym(T;x,y.R[x; y])
Lemmas referenced :  member-iseg-sorted-by equal_wf list_wf append_wf not_wf assert_wf null_wf3 subtype_rel_list top_wf all_wf iff_wf bool_wf trans_wf sorted-by_wf subtype_rel_dep_function l_member_wf subtype_rel_self set_wf anti_sym_wf irrefl_wf sorted-by-strict-unique filter_wf5 last_wf member_filter member_append squash_wf true_wf select_append_back length_wf nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermVar_wf itermAdd_wf itermConstant_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_var_lemma int_term_value_add_lemma int_term_value_constant_lemma int_formula_prop_wf decidable__lt intformless_wf int_formula_prop_less_lemma lelt_wf iff_weakening_equal add-associates minus-one-mul add-swap add-mul-special zero-mul add-zero subtype_base_sq int_subtype_base select_wf add_nat_wf length_wf_nat nat_wf add-is-int-iff intformeq_wf int_formula_prop_eq_lemma false_wf length-append less_than_wf list-cases length_of_nil_lemma null_nil_lemma product_subtype_list length_of_cons_lemma null_cons_lemma not-lt-2 condition-implies-le minus-add zero-add minus-one-mul-top add-commutes add_functionality_wrt_le le-add-cancel subtract_wf itermSubtract_wf int_term_value_subtract_lemma select_append_front and_wf sorted-by-filter sublist_append2 sublist_wf sublist-sorted-by
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination independent_isectElimination independent_functionElimination dependent_pairFormation cumulativity applyEquality lambdaEquality isect_memberEquality voidElimination voidEquality because_Cache sqequalRule axiomEquality equalityTransitivity equalitySymmetry functionExtensionality functionEquality instantiate universeEquality setEquality setElimination rename lambdaFormation addLevel productElimination independent_pairFormation impliesFunctionality andLevelFunctionality productEquality inrFormation hyp_replacement applyLambdaEquality dependent_set_memberEquality imageElimination addEquality unionElimination natural_numberEquality int_eqEquality intEquality computeAll imageMemberEquality baseClosed pointwiseFunctionality promote_hyp baseApply closedConclusion hypothesis_subsumption minusEquality

\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[sa,s,sb:T  List].
    (\mforall{}[dR:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}]
          (sb  =  filter(dR  last(sa);s))  supposing 
                ((\mneg{}\muparrow{}null(sa))  and 
                (\mforall{}x,y:T.    (\muparrow{}(dR  x  y)  \mLeftarrow{}{}\mRightarrow{}  R  x  y))))  supposing 
          (Trans(T;a,b.R  a  b)  and 
          sorted-by(R;s)  and 
          (s  =  (sa  @  sb))  and 
          AntiSym(T;x,y.R  x  y)  and 
          Irrefl(T;x,y.R  x  y))

Date html generated: 2018_05_21-PM-06_47_12
Last ObjectModification: 2017_07_26-PM-04_56_33

Theory : general

Home Index