Nuprl Lemma : s-insert-no-repeats

[T:Type]. ∀[x:T]. ∀[L:T List].  (no_repeats(T;s-insert(x;L))) supposing (no_repeats(T;L) and sorted(L)) supposing T ⊆\000Cℤ


Definitions occuring in Statement :  s-insert: s-insert(x;l) no_repeats: no_repeats(T;l) sorted: sorted(L) list: List uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] int: universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a so_lambda: λ2x.t[x] prop: so_apply: x[s] implies:  Q all: x:A. B[x] s-insert: s-insert(x;l) no_repeats: no_repeats(T;l) sorted: sorted(L) select: L[n] nil: [] it: so_lambda: λ2y.t[x; y] top: Top so_apply: x[s1;s2] so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] not: ¬A false: False nat: ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] and: P ∧ Q decidable: Dec(P) or: P ∨ Q le: A ≤ B subtype_rel: A ⊆B int_seg: {i..j-} guard: {T} lelt: i ≤ j < k uiff: uiff(P;Q) cand: c∧ B bool: 𝔹 unit: Unit btrue: tt ifthenelse: if then else fi  bfalse: ff iff: ⇐⇒ Q rev_implies:  Q label: ...$L... t
Lemmas referenced :  list_induction isect_wf sorted_wf no_repeats_wf s-insert_wf list_wf no_repeats_witness subtype_rel_wf length_of_nil_lemma stuck-spread base_wf list_ind_nil_lemma length_of_cons_lemma nat_properties satisfiable-full-omega-tt intformand_wf intformnot_wf intformeq_wf itermVar_wf intformless_wf itermConstant_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_formula_prop_le_lemma decidable__equal_int int_formula_prop_wf le_wf equal-wf-base int_subtype_base equal_wf select_wf cons_wf nil_wf not_wf nat_wf less_than_wf uall_wf all_wf int_seg_wf int_seg_properties list_ind_cons_lemma ifthenelse_wf eq_int_wf lt_int_wf bool_wf equal-wf-T-base assert_wf bnot_wf no_repeats_cons le_int_wf uiff_transitivity eqtt_to_assert assert_of_eq_int iff_transitivity iff_weakening_uiff eqff_to_assert assert_of_bnot assert_of_lt_int assert_functionality_wrt_uiff bnot_of_lt_int assert_of_le_int sorted-cons l_all_iff subtype_rel_transitivity l_member_wf cons_member or_wf equal_functionality_wrt_subtype_rel2 member-s-insert
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin extract_by_obid sqequalHypSubstitution isectElimination because_Cache sqequalRule lambdaEquality cumulativity hypothesisEquality independent_isectElimination hypothesis independent_functionElimination lambdaFormation rename dependent_functionElimination isect_memberEquality equalityTransitivity equalitySymmetry intEquality universeEquality baseClosed voidElimination voidEquality setElimination natural_numberEquality dependent_pairFormation int_eqEquality independent_pairFormation unionElimination computeAll dependent_set_memberEquality productElimination applyEquality equalityElimination impliesFunctionality setEquality promote_hyp addLevel

    \mforall{}[x:T].  \mforall{}[L:T  List].    (no\_repeats(T;s-insert(x;L)))  supposing  (no\_repeats(T;L)  and  sorted(L)) 
    supposing  T  \msubseteq{}r  \mBbbZ{}

Date html generated: 2017_04_17-AM-08_32_18
Last ObjectModification: 2017_02_27-PM-04_53_04

Theory : list_1

Home Index