### Nuprl Lemma : remove-repeats_property

`∀[T:Type]`
`  ∀eq:EqDecider(T). ∀L:T List.  (no_repeats(T;remove-repeats(eq;L)) ∧ (∀a:T. ((a ∈ remove-repeats(eq;L)) `⇐⇒` (a ∈ L))))`

Proof

Definitions occuring in Statement :  remove-repeats: `remove-repeats(eq;L)` no_repeats: `no_repeats(T;l)` l_member: `(x ∈ l)` list: `T List` deq: `EqDecider(T)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` prop: `ℙ` and: `P ∧ Q` so_apply: `x[s]` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` remove-repeats: `remove-repeats(eq;L)` so_lambda: `so_lambda(x,y,z.t[x; y; z])` top: `Top` so_apply: `x[s1;s2;s3]` cand: `A c∧ B` deq: `EqDecider(T)` uiff: `uiff(P;Q)` uimplies: `b supposing a` not: `¬A` false: `False` eqof: `eqof(d)` or: `P ∨ Q` guard: `{T}` decidable: `Dec(P)`
Lemmas referenced :  list_induction no_repeats_wf remove-repeats_wf all_wf iff_wf l_member_wf list_wf list_ind_nil_lemma no_repeats_nil nil_wf list_ind_cons_lemma no_repeats_cons filter_wf5 bnot_wf no_repeats_filter cons_wf deq_wf member_filter not_wf assert_wf member_wf eqof_wf equal_wf iff_transitivity iff_weakening_uiff assert_of_bnot safe-assert-deq cons_member decidable-equal-deq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality productEquality cumulativity hypothesis independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality independent_pairFormation because_Cache rename productElimination applyEquality setElimination setEquality independent_isectElimination universeEquality addLevel impliesFunctionality andLevelFunctionality levelHypothesis impliesLevelFunctionality unionElimination inlFormation inrFormation

Latex:
\mforall{}[T:Type]
\mforall{}eq:EqDecider(T).  \mforall{}L:T  List.
(no\_repeats(T;remove-repeats(eq;L))  \mwedge{}  (\mforall{}a:T.  ((a  \mmember{}  remove-repeats(eq;L))  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  L))))

Date html generated: 2017_04_17-AM-09_10_16
Last ObjectModification: 2017_02_27-PM-05_18_28

Theory : decidable!equality

Home Index