### Nuprl Lemma : length-remove-repeats

`∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L1,L2:T List].`
`  ||remove-repeats(eq;L1)|| = ||remove-repeats(eq;L2)|| ∈ ℤ supposing ∀x:T. ((x ∈ L1) `⇐⇒` (x ∈ L2))`

Proof

Definitions occuring in Statement :  remove-repeats: `remove-repeats(eq;L)` l_member: `(x ∈ l)` length: `||as||` list: `T List` deq: `EqDecider(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` all: `∀x:A. B[x]` and: `P ∧ Q` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` set-equal: `set-equal(T;x;y)` iff: `P `⇐⇒` Q` implies: `P `` Q` rev_implies: `P `` Q`
Lemmas referenced :  set-equal-no_repeats-length remove-repeats_wf remove-repeats_property all_wf iff_wf l_member_wf member-remove-repeats
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_isectElimination because_Cache dependent_functionElimination productElimination sqequalRule lambdaEquality isect_memberEquality axiomEquality equalityTransitivity equalitySymmetry addLevel allFunctionality independent_pairFormation impliesFunctionality independent_functionElimination

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L1,L2:T  List].
||remove-repeats(eq;L1)||  =  ||remove-repeats(eq;L2)||  supposing  \mforall{}x:T.  ((x  \mmember{}  L1)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L2))

Date html generated: 2016_05_14-PM-03_26_38
Last ObjectModification: 2015_12_26-PM-06_23_09

Theory : decidable!equality

Home Index