---

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