### Nuprl Lemma : list-to-set-is-remove-repeats

`∀[T:Type]. ∀eq:EqDecider(T). ∀L:T List.  permutation(T;list-to-set(eq;L);remove-repeats(eq;L))`

Proof

Definitions occuring in Statement :  remove-repeats: `remove-repeats(eq;L)` list-to-set: `list-to-set(eq;L)` permutation: `permutation(T;L1;L2)` list: `T List` deq: `EqDecider(T)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` deq: `EqDecider(T)` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` eqof: `eqof(d)` uiff: `uiff(P;Q)` uimplies: `b supposing a` prop: `ℙ` rev_implies: `P `` Q` rev_uimplies: `rev_uimplies(P;Q)` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` false: `False` ge: `i ≥ j ` le: `A ≤ B` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top`
Lemmas referenced :  permutation-iff-count1 safe-assert-deq assert_wf equal_wf assert_witness list-to-set_wf remove-repeats_wf list-to-set-property no-repeats-iff-count remove-repeats-no_repeats list_wf deq_wf decidable__le length_wf filter_wf5 subtype_rel_dep_function l_member_wf bool_wf set_wf subtype_rel_self remove-repeats_property l_member-iff-length-filter equal-wf-T-base non_neg_length decidable__equal_int satisfiable-full-omega-tt intformand_wf intformnot_wf intformeq_wf itermVar_wf intformle_wf itermConstant_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_formula_prop_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination setElimination rename hypothesis independent_functionElimination independent_pairFormation sqequalRule because_Cache productElimination independent_isectElimination applyEquality cumulativity independent_pairEquality lambdaEquality axiomEquality universeEquality natural_numberEquality setEquality unionElimination equalityTransitivity equalitySymmetry promote_hyp voidElimination instantiate baseClosed dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidEquality computeAll

Latex:
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}L:T  List.    permutation(T;list-to-set(eq;L);remove-repeats(eq;L))

Date html generated: 2017_04_17-AM-09_11_30
Last ObjectModification: 2017_02_27-PM-05_19_29

Theory : decidable!equality

Home Index