Step * of Lemma remove-repeats_functionality_wrt_permutation

`∀[T:Type]`
`  ∀eq:EqDecider(T). ∀L1,L2:T List.  (permutation(T;L1;L2) `` permutation(T;remove-repeats(eq;L1);remove-repeats(eq;L2)))`
BY
`{ TACTIC:(InductionOnLength THEN Reduce 0 THEN Auto THEN DVar `L1') }`

1
`1. [T] : Type`
`2. eq : EqDecider(T)`
`3. n : ℕ`
`4. ∀L2:T List`
`     (||L2|| < ||[]||`
`     `` (∀L3:T List. (permutation(T;L2;L3) `` permutation(T;remove-repeats(eq;L2);remove-repeats(eq;L3)))))`
`5. L2 : T List`
`6. permutation(T;[];L2)`
`⊢ permutation(T;remove-repeats(eq;[]);remove-repeats(eq;L2))`

2
`1. [T] : Type`
`2. eq : EqDecider(T)`
`3. n : ℕ`
`4. u : T`
`5. v : T List`
`6. ∀L2:T List`
`     (||L2|| < ||[u / v]||`
`     `` (∀L3:T List. (permutation(T;L2;L3) `` permutation(T;remove-repeats(eq;L2);remove-repeats(eq;L3)))))`
`7. L2 : T List`
`8. permutation(T;[u / v];L2)`
`⊢ permutation(T;remove-repeats(eq;[u / v]);remove-repeats(eq;L2))`

Latex:

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

By

Latex:
TACTIC:(InductionOnLength  THEN  Reduce  0  THEN  Auto  THEN  DVar  `L1')

Home Index