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 ⊆r \000Cℤ`

Proof

Definitions occuring in Statement :  s-insert: `s-insert(x;l)` no_repeats: `no_repeats(T;l)` sorted: `sorted(L)` list: `T List` uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` int: `ℤ` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` so_lambda: `λ2x.t[x]` prop: `ℙ` so_apply: `x[s]` implies: `P `` 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: `λ2x y.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 ≥ j ` 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 ⊆r B` int_seg: `{i..j-}` guard: `{T}` lelt: `i ≤ j < k` uiff: `uiff(P;Q)` cand: `A c∧ B` bool: `𝔹` unit: `Unit` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` iff: `P `⇐⇒` Q` rev_implies: `P `` 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

Latex:
\mforall{}[T:Type]
\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