Nuprl Lemma : descending-append

[A:Type]. ∀[<:A ⟶ A ⟶ ℙ].
  ∀L1,L2:A List.
    (descending(a,b.<[a;b];L1 L2)
    ⇐⇒ descending(a,b.<[a;b];L1)
        ∧ descending(a,b.<[a;b];L2)
        ∧ (<[hd(L2);last(L1)]) supposing (0 < ||L2|| and 0 < ||L1||))


Definitions occuring in Statement :  descending: descending(a,b.<[a; b];L) last: last(L) length: ||as|| append: as bs hd: hd(l) list: List less_than: a < b uimplies: supposing a uall: [x:A]. B[x] prop: so_apply: x[s1;s2] all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q function: x:A ⟶ B[x] natural_number: $n universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] prop: rev_implies:  Q uimplies: supposing a ge: i ≥  decidable: Dec(P) or: P ∨ Q less_than: a < b squash: T not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False assert: b ifthenelse: if then else fi  btrue: tt less_than': less_than'(a;b) cons: [a b] bfalse: ff subtype_rel: A ⊆B descending: descending(a,b.<[a; b];L) cand: c∧ B true: True guard: {T} subtract: m uiff: uiff(P;Q) top: Top le: A ≤ B lelt: i ≤ j < k int_seg: {i..j-} nat: last: last(L) sq_type: SQType(T) it: nil: [] select: L[n] so_apply: x[s1;s2;s3] so_lambda: so_lambda3 append: as bs nat_plus: +
Lemmas referenced :  descending_wf append_wf istype-less_than length_wf hd_wf decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf last_wf list-cases null_nil_lemma length_of_nil_lemma product_subtype_list null_cons_lemma length_of_cons_lemma istype-void list_wf istype-universe length-append int_seg_wf subtract_wf member-less_than iff_weakening_equal subtype_rel_self false_wf subtract-is-int-iff int_seg_properties select_wf add-member-int_seg2 select_append_front true_wf squash_wf equal_wf istype-le int_term_value_add_lemma int_term_value_subtract_lemma itermAdd_wf itermSubtract_wf decidable__lt non_neg_length less_than_wf le_wf add-zero zero-mul add-mul-special add-swap minus-one-mul add-associates add-commutes select_append_back zero-add select-nthtl subtype_rel_list top_wf nth_tl_append add-is-int-iff decidable__equal_int int_subtype_base subtype_base_sq istype-base stuck-spread length_wf_nat int_formula_prop_eq_lemma intformeq_wf general_arith_equation1 list_ind_cons_lemma list_ind_nil_lemma nat_plus_properties add_nat_plus
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt independent_pairFormation universeIsType cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule lambdaEquality_alt applyEquality inhabitedIsType hypothesis productIsType isectIsType natural_numberEquality because_Cache independent_isectElimination dependent_functionElimination unionElimination imageElimination productElimination approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality Error :memTop,  voidElimination promote_hyp hypothesis_subsumption functionIsType universeEquality instantiate rename imageMemberEquality baseClosed baseApply pointwiseFunctionality closedConclusion cumulativity functionEquality equalitySymmetry equalityTransitivity isect_memberEquality_alt addEquality dependent_set_memberEquality_alt setElimination productEquality hyp_replacement minusEquality intEquality equalityIsType1 applyLambdaEquality

\mforall{}[A:Type].  \mforall{}[<:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}L1,L2:A  List.
        (descending(a,b.<[a;b];L1  @  L2)
        \mLeftarrow{}{}\mRightarrow{}  descending(a,b.<[a;b];L1)
                \mwedge{}  descending(a,b.<[a;b];L2)
                \mwedge{}  (<[hd(L2);last(L1)])  supposing  (0  <  ||L2||  and  0  <  ||L1||))

Date html generated: 2020_05_20-AM-08_07_28
Last ObjectModification: 2019_12_31-PM-06_30_35

Theory : general

Home Index