---

Step * of Lemma permutation-filter

∀[A:Type]. ∀L1,L2:A List.  (permutation(A;L1;L2) ⇒ (∀p:A ⟶ 𝔹. permutation({a:A| ↑(p a)} ;filter(p;L1);filter(p;L2))))
BY
{ (InductionOnList THEN Reduce 0 THEN Auto) }

1
1. [A] : Type
2. L2 : A List
3. permutation(A;[];L2)
4. p : A ⟶ 𝔹
⊢ permutation({a:A| ↑(p a)} ;[];filter(p;L2))

2
1. [A] : Type
2. u : A
3. v : A List
4. ∀L2:A List. (permutation(A;v;L2) ⇒ (∀p:A ⟶ 𝔹. permutation({a:A| ↑(p a)} ;filter(p;v);filter(p;L2))))
5. L2 : A List
6. permutation(A;[u / v];L2)
7. p : A ⟶ 𝔹
⊢ permutation({a:A| ↑(p a)} ;if p u then [u / filter(p;v)] else filter(p;v) fi ;filter(p;L2))

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}L1,L2:A  List.
        (permutation(A;L1;L2)  {}\mRightarrow{}  (\mforall{}p:A  {}\mrightarrow{}  \mBbbB{}.  permutation(\{a:A|  \muparrow{}(p  a)\}  ;filter(p;L1);filter(p;L2))))


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto)

---

Home Index