---

Step * 2 1 2 1 2 1 of Lemma remove-repeats_functionality_wrt_permutation


1. [T] : Type
2. eq : EqDecider(T)
3. n : ℕ
4. u : T
5. L2 : T List
6. as : T List
7. bs : T List
8. ∀L2:T List
     ((||L2|| ≤ ||as @ bs||)
     ⇒ (∀L3:T List. (permutation(T;L2;L3) ⇒ permutation(T;remove-repeats(eq;L2);remove-repeats(eq;L3)))))
⊢ permutation(T;[u / filter(λx.(¬b(eq x u));remove-repeats(eq;as @ bs))];remove-repeats(eq;as @ [u / bs]))
BY
{ ((RWO "remove-repeats-append-sq" 0 THENA Auto)
   THEN Unfold `remove-repeats` 0
   THEN Reduce 0
   THEN Fold `remove-repeats` 0
   THEN (RWO "filter_append_sq" 0 THENA Auto)
   THEN (RW (AddrC [2;2;2] (LemmaC `swap-filter-filter`)) 0 THENA Auto)
   THEN GenConclAtAddr [2;2;2]
   THEN AutoSplit)⋅ }

1
1. [T] : Type
2. eq : EqDecider(T)
3. n : ℕ
4. u : T
5. L2 : T List
6. as : T List
7. bs : T List
8. ∀L2:T List
     ((||L2|| ≤ ||as @ bs||)
     ⇒ (∀L3:T List. (permutation(T;L2;L3) ⇒ permutation(T;remove-repeats(eq;L2);remove-repeats(eq;L3)))))
9. v : T List
10. filter(λx.(¬bx ∈b as);filter(λx.(¬b(eq x u));remove-repeats(eq;bs))) = v ∈ (T List)
11. (u ∈ as)
⊢ permutation(T;[u / (filter(λx.(¬b(eq x u));remove-repeats(eq;as)) @ v)];remove-repeats(eq;as) @ v)

2
1. [T] : Type
2. eq : EqDecider(T)
3. n : ℕ
4. u : T
5. L2 : T List
6. as : T List
7. ¬(u ∈ as)
8. bs : T List
9. ∀L2:T List
     ((||L2|| ≤ ||as @ bs||)
     ⇒ (∀L3:T List. (permutation(T;L2;L3) ⇒ permutation(T;remove-repeats(eq;L2);remove-repeats(eq;L3)))))
10. v : T List
11. filter(λx.(¬bx ∈b as);filter(λx.(¬b(eq x u));remove-repeats(eq;bs))) = v ∈ (T List)
⊢ permutation(T;[u / (filter(λx.(¬b(eq x u));remove-repeats(eq;as)) @ v)];remove-repeats(eq;as) @ [u / v])

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  eq  :  EqDecider(T)
3.  n  :  \mBbbN{}
4.  u  :  T
5.  L2  :  T  List
6.  as  :  T  List
7.  bs  :  T  List
8.  \mforall{}L2:T  List
          ((||L2||  \mleq{}  ||as  @  bs||)
          {}\mRightarrow{}  (\mforall{}L3:T  List
                      (permutation(T;L2;L3)  {}\mRightarrow{}  permutation(T;remove-repeats(eq;L2);remove-repeats(eq;L3)))))
\mvdash{}  permutation(T;[u  /  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));remove-repeats(eq;as  @  bs))];remove-repeats(eq;as
                            @  [u  /  bs]))


By

---

Latex:
((RWO  "remove-repeats-append-sq"  0  THENA  Auto)
  THEN  Unfold  `remove-repeats`  0
  THEN  Reduce  0
  THEN  Fold  `remove-repeats`  0
  THEN  (RWO  "filter\_append\_sq"  0  THENA  Auto)
  THEN  (RW  (AddrC  [2;2;2]  (LemmaC  `swap-filter-filter`))  0  THENA  Auto)
  THEN  GenConclAtAddr  [2;2;2]
  THEN  AutoSplit)\mcdot{}

---

Home Index