### Nuprl Lemma : remove-repeats-append

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

Proof

Definitions occuring in Statement :  remove-repeats: `remove-repeats(eq;L)` length: `||as||` append: `as @ bs` list: `T List` deq: `EqDecider(T)` uall: `∀[x:A]. B[x]` 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]`
Lemmas referenced :  remove-repeats-set-equal append_wf set-equal-permute
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_isectElimination dependent_functionElimination because_Cache sqequalRule isect_memberEquality axiomEquality

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

Date html generated: 2016_05_14-PM-03_26_15
Last ObjectModification: 2015_12_26-PM-06_23_02

Theory : decidable!equality

Home Index