---

Step * 1 of Lemma permutation-filter


1. [A] : Type
2. L2 : A List
3. permutation(A;[];L2)
4. p : A ⟶ 𝔹
⊢ permutation({a:A| ↑(p a)} ;[];filter(p;L2))
BY
{ (DVar `L2' THEN Reduce 0) }

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

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

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  L2  :  A  List
3.  permutation(A;[];L2)
4.  p  :  A  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  permutation(\{a:A|  \muparrow{}(p  a)\}  ;[];filter(p;L2))


By

---

Latex:
(DVar  `L2'  THEN  Reduce  0)

---

Home Index