---

Step * 2 1 2 1 of Lemma remove-repeats_functionality_wrt_permutation

.....assertion..... 
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)
9. as : T List
10. bs : T List
11. permutation(T;v;as @ bs)
12. permutation(T;remove-repeats(eq;v);remove-repeats(eq;as @ bs))
13. permutation(T;[u / filter(λx.(¬b(eq x u));remove-repeats(eq;v))];[u / 
                                                                      filter(λx.(¬b(eq x u));remove-repeats(eq;as
                                                                                             @ bs))])
⊢ permutation(T;[u / filter(λx.(¬b(eq x u));remove-repeats(eq;as @ bs))];remove-repeats(eq;as @ [u / bs]))
BY
{ Assert ⌜∀L2:T List
            ((||L2|| ≤ ||as @ bs||)
            ⇒ (∀L3:T List. (permutation(T;L2;L3) ⇒ permutation(T;remove-repeats(eq;L2);remove-repeats(eq;L3)))))⌝⋅ }

1
.....assertion..... 
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)
9. as : T List
10. bs : T List
11. permutation(T;v;as @ bs)
12. permutation(T;remove-repeats(eq;v);remove-repeats(eq;as @ bs))
13. permutation(T;[u / filter(λx.(¬b(eq x u));remove-repeats(eq;v))];[u / 
                                                                      filter(λx.(¬b(eq x u));remove-repeats(eq;as
                                                                                             @ bs))])
⊢ ∀L2:T List
    ((||L2|| ≤ ||as @ bs||)
    ⇒ (∀L3:T List. (permutation(T;L2;L3) ⇒ permutation(T;remove-repeats(eq;L2);remove-repeats(eq;L3)))))

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)
9. as : T List
10. bs : T List
11. permutation(T;v;as @ bs)
12. permutation(T;remove-repeats(eq;v);remove-repeats(eq;as @ bs))
13. permutation(T;[u / filter(λx.(¬b(eq x u));remove-repeats(eq;v))];[u / 
                                                                      filter(λx.(¬b(eq x u));remove-repeats(eq;as
                                                                                             @ bs))])
14. ∀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]))

---

Latex:

---

Latex:
.....assertion..... 
1.  [T]  :  Type
2.  eq  :  EqDecider(T)
3.  n  :  \mBbbN{}
4.  u  :  T
5.  v  :  T  List
6.  \mforall{}L2:T  List
          (||L2||  <  ||[u  /  v]||
          {}\mRightarrow{}  (\mforall{}L3:T  List
                      (permutation(T;L2;L3)  {}\mRightarrow{}  permutation(T;remove-repeats(eq;L2);remove-repeats(eq;L3)))))
7.  L2  :  T  List
8.  permutation(T;[u  /  v];L2)
9.  as  :  T  List
10.  bs  :  T  List
11.  permutation(T;v;as  @  bs)
12.  permutation(T;remove-repeats(eq;v);remove-repeats(eq;as  @  bs))
13.  permutation(T;[u  /  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));remove-repeats(eq;v))];[u  / 
                                                                                                                                            filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));
                                                                                                                                                          remove-repeats(eq;as
                                                                                                                                                          @  bs))])
\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:
Assert  \mkleeneopen{}\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)))))\mkleeneclose{}\mcdot{}

---

Home Index