### Nuprl Lemma : no_repeats_iff

`∀[T:Type]. ∀[l:T List].  uiff(no_repeats(T;l);∀[x,y:T].  ¬(x = y ∈ T) supposing x before y ∈ l)`

Proof

Definitions occuring in Statement :  l_before: `x before y ∈ l` no_repeats: `no_repeats(T;l)` list: `T List` uiff: `uiff(P;Q)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  l_before: `x before y ∈ l` no_repeats: `no_repeats(T;l)` sublist: `L1 ⊆ L2` uall: `∀[x:A]. B[x]` member: `t ∈ T` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` not: `¬A` implies: `P `` Q` false: `False` exists: `∃x:A. B[x]` int_seg: `{i..j-}` lelt: `i ≤ j < k` le: `A ≤ B` subtype_rel: `A ⊆r B` prop: `ℙ` all: `∀x:A. B[x]` less_than: `a < b` squash: `↓T` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` ge: `i ≥ j ` nat: `ℕ` guard: `{T}` subtract: `n - m` cons: `[a / b]` select: `L[n]` true: `True` less_than': `less_than'(a;b)` top: `Top` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` increasing: `increasing(f;k)` cand: `A c∧ B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` length: `||as||` list_ind: list_ind nil: `[]` it: `⋅` nequal: `a ≠ b ∈ T ` assert: `↑b` bnot: `¬bb` sq_type: `SQType(T)` bfalse: `ff` ifthenelse: `if b then t else f fi ` btrue: `tt` unit: `Unit` bool: `𝔹` eq_int: `(i =z j)`
Lemmas referenced :  int_seg_wf length_wf cons_wf nil_wf increasing_wf length_wf_nat select_wf length_of_cons_lemma length_of_nil_lemma int_seg_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_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_wf decidable__lt intformless_wf itermAdd_wf int_formula_prop_less_lemma int_term_value_add_lemma non_neg_length istype-le istype-less_than nat_properties istype-nat istype-void list_wf istype-universe lelt_wf false_wf iff_weakening_equal equal_wf true_wf squash_wf not_wf satisfiable-full-omega-tt int_seg_subtype_nat nat_wf int_formula_prop_eq_lemma intformeq_wf ifthenelse_wf eq_int_wf subtype_rel_dep_function int_seg_subtype istype-false neg_assert_of_eq_int assert-bnot bool_subtype_base subtype_base_sq bool_cases_sqequal eqff_to_assert assert_of_eq_int eqtt_to_assert bool_wf decidable__equal_int int_subtype_base int_seg_subtype_special int_seg_cases int_term_value_subtract_lemma itermSubtract_wf subtract_wf select-cons-tl select-cons-hd equal-wf-base le_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation_alt introduction cut independent_pairFormation lambdaFormation_alt thin hypothesis sqequalHypSubstitution independent_functionElimination voidElimination equalityIstype inhabitedIsType hypothesisEquality lambdaEquality_alt dependent_functionElimination because_Cache functionIsTypeImplies productIsType functionIsType universeIsType extract_by_obid isectElimination natural_numberEquality setElimination rename productElimination functionExtensionality applyEquality equalityTransitivity equalitySymmetry independent_isectElimination Error :memTop,  imageElimination unionElimination approximateComputation dependent_pairFormation_alt int_eqEquality addEquality dependent_set_memberEquality_alt applyLambdaEquality isect_memberEquality_alt isectIsTypeImplies isectIsType independent_pairEquality instantiate universeEquality baseClosed imageMemberEquality lambdaFormation dependent_set_memberEquality voidEquality isect_memberEquality computeAll intEquality lambdaEquality dependent_pairFormation cumulativity closedConclusion promote_hyp equalityElimination hypothesis_subsumption

Latex:
\mforall{}[T:Type].  \mforall{}[l:T  List].    uiff(no\_repeats(T;l);\mforall{}[x,y:T].    \mneg{}(x  =  y)  supposing  x  before  y  \mmember{}  l)

Date html generated: 2020_05_19-PM-09_42_24
Last ObjectModification: 2020_01_04-PM-08_14_09

Theory : list_1

Home Index