Nuprl Lemma : l_contains-cons

  ∀u:T. ∀v,bs:T List.
    ([u v] ⊆ bs ⇐⇒ ∃cs,ds:T List. ((bs (cs [u ds]) ∈ (T List)) ∧ v ⊆ cs ds)) supposing 
       (no_repeats(T;bs) and 
       no_repeats(T;[u v]))


Definitions occuring in Statement :  l_contains: A ⊆ B no_repeats: no_repeats(T;l) append: as bs cons: [a b] list: List uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q 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 implies:  Q iff: ⇐⇒ Q and: P ∧ Q prop: rev_implies:  Q so_lambda: λ2x.t[x] top: Top so_apply: x[s] l_contains: A ⊆ B l_all: (∀x∈L.P[x]) int_seg: {i..j-} lelt: i ≤ j < k le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A nat_plus: + less_than: a < b squash: T true: True guard: {T} decidable: Dec(P) or: P ∨ Q uiff: uiff(P;Q) satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] append: as bs so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] cand: c∧ B sq_type: SQType(T) select: L[n] cons: [a b] ge: i ≥ 
Lemmas referenced :  no_repeats_witness cons_wf l_contains_wf exists_wf list_wf equal_wf append_wf length_wf length-append no_repeats_wf length_of_cons_lemma false_wf add_nat_plus length_wf_nat less_than_wf nat_plus_wf nat_plus_properties decidable__lt add-is-int-iff satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf itermAdd_wf intformeq_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_term_value_add_lemma int_formula_prop_eq_lemma int_formula_prop_wf lelt_wf select-cons-hd l_member_decomp list_ind_cons_lemma list_ind_nil_lemma l_all_iff l_member_wf cons_member nat_wf member_append or_wf no_repeats_cons and_wf select_wf int_seg_properties decidable__le intformle_wf int_formula_prop_le_lemma decidable__equal_int subtype_base_sq int_subtype_base int_seg_wf all_wf select-cons-tl subtract_wf itermSubtract_wf int_term_value_subtract_lemma non_neg_length
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality cumulativity hypothesis independent_functionElimination rename because_Cache independent_pairFormation sqequalRule lambdaEquality productEquality applyLambdaEquality isect_memberEquality voidElimination voidEquality universeEquality dependent_functionElimination dependent_set_memberEquality natural_numberEquality imageMemberEquality baseClosed equalityTransitivity equalitySymmetry setElimination unionElimination pointwiseFunctionality promote_hyp baseApply closedConclusion productElimination independent_isectElimination dependent_pairFormation int_eqEquality intEquality computeAll addEquality setEquality inrFormation hyp_replacement addLevel orFunctionality inlFormation levelHypothesis allFunctionality imageElimination instantiate allLevelFunctionality

    \mforall{}u:T.  \mforall{}v,bs:T  List.
        ([u  /  v]  \msubseteq{}  bs  \mLeftarrow{}{}\mRightarrow{}  \mexists{}cs,ds:T  List.  ((bs  =  (cs  @  [u  /  ds]))  \mwedge{}  v  \msubseteq{}  cs  @  ds))  supposing 
              (no\_repeats(T;bs)  and 
              no\_repeats(T;[u  /  v]))

Date html generated: 2017_04_17-AM-07_29_37
Last ObjectModification: 2017_02_27-PM-04_07_51

Theory : list_1

Home Index