### Nuprl Lemma : append_overlapping_sublists

`∀[T:Type]. ∀L1,L2,L:T List. ∀x:T.  L1 @ [x] ⊆ L `` [x / L2] ⊆ L `` L1 @ [x / L2] ⊆ L supposing no_repeats(T;L)`

Proof

Definitions occuring in Statement :  sublist: `L1 ⊆ L2` no_repeats: `no_repeats(T;l)` append: `as @ bs` cons: `[a / b]` nil: `[]` list: `T List` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` implies: `P `` Q` sublist: `L1 ⊆ L2` no_repeats: `no_repeats(T;l)` exists: `∃x:A. B[x]` and: `P ∧ Q` prop: `ℙ` top: `Top` ge: `i ≥ j ` le: `A ≤ B` less_than': `less_than'(a;b)` false: `False` not: `¬A` int_seg: `{i..j-}` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` bfalse: `ff` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` cand: `A c∧ B` subtype_rel: `A ⊆r B` nat: `ℕ` increasing: `increasing(f;k)` less_than: `a < b` squash: `↓T` subtract: `n - m` true: `True` so_apply: `x[s]` so_lambda: `λ2x.t[x]` cons: `[a / b]` select: `L[n]`
Lemmas referenced :  no_repeats_witness length_of_cons_lemma sublist_wf cons_wf append_wf nil_wf no_repeats_wf list_wf istype-universe length_wf istype-void length-append length_of_nil_lemma istype-false le_int_wf eqtt_to_assert assert_of_le_int decidable__lt full-omega-unsat intformand_wf intformnot_wf intformless_wf itermVar_wf itermAdd_wf itermConstant_wf intformle_wf istype-int int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_add_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf istype-le istype-less_than eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot iff_weakening_uiff assert_wf le_wf subtract_wf int_seg_properties decidable__le add-is-int-iff itermSubtract_wf int_term_value_subtract_lemma false_wf intformeq_wf int_formula_prop_eq_lemma int_seg_wf increasing_wf length_wf_nat select_wf length_cons non_neg_length length_append subtype_rel_list top_wf nat_properties add-associates minus-one-mul add-swap add-commutes less_than_wf squash_wf true_wf lelt_wf decidable__equal_int int_subtype_base increasing_implies nat_wf set_subtype_base equal_wf not_wf iff_weakening_equal subtype_rel_self select_append_back add-subtract-cancel length_nil product_subtype_list list-cases bnot_wf lt_int_wf equal-wf-T-base uiff_transitivity assert_functionality_wrt_uiff bnot_of_le_int assert_of_lt_int add-mul-special zero-mul select-cons-hd select_append_front
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_functionElimination hypothesis rename sqequalRule dependent_functionElimination Error :memTop,  productElimination universeIsType inhabitedIsType instantiate universeEquality natural_numberEquality addEquality voidElimination isect_memberEquality_alt independent_pairFormation dependent_pairFormation_alt lambdaEquality_alt setElimination because_Cache unionElimination equalityElimination independent_isectElimination applyEquality dependent_set_memberEquality_alt approximateComputation int_eqEquality productIsType equalityTransitivity equalitySymmetry equalityIstype promote_hyp cumulativity pointwiseFunctionality baseApply closedConclusion baseClosed functionExtensionality functionIsType applyLambdaEquality imageElimination multiplyEquality minusEquality hyp_replacement imageMemberEquality equalityIsType1 intEquality voidEquality hypothesis_subsumption

Latex:
\mforall{}[T:Type]
\mforall{}L1,L2,L:T  List.  \mforall{}x:T.
L1  @  [x]  \msubseteq{}  L  {}\mRightarrow{}  [x  /  L2]  \msubseteq{}  L  {}\mRightarrow{}  L1  @  [x  /  L2]  \msubseteq{}  L  supposing  no\_repeats(T;L)

Date html generated: 2020_05_19-PM-09_42_19
Last ObjectModification: 2020_02_06-PM-09_36_44

Theory : list_1

Home Index