---

Step * 2 2 of Lemma permutation-filter


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. as : A List
7. bs : A List
8. L2 = (as @ [u / bs]) ∈ (A List)
9. permutation(A;v;as @ bs)
10. p : A ⟶ 𝔹
11. ¬↑(p u)
12. ¬False
⊢ permutation({a:A| ↑(p a)} ;filter(p;v);filter(p;as) @ filter(p;bs))
BY
{ ((RWO "filter_append_sq<" 0 THENA Auto)⋅ THEN BackThruSomeHyp THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  u  :  A
3.  v  :  A  List
4.  \mforall{}L2:A  List
          (permutation(A;v;L2)  {}\mRightarrow{}  (\mforall{}p:A  {}\mrightarrow{}  \mBbbB{}.  permutation(\{a:A|  \muparrow{}(p  a)\}  ;filter(p;v);filter(p;L2))))
5.  L2  :  A  List
6.  as  :  A  List
7.  bs  :  A  List
8.  L2  =  (as  @  [u  /  bs])
9.  permutation(A;v;as  @  bs)
10.  p  :  A  {}\mrightarrow{}  \mBbbB{}
11.  \mneg{}\muparrow{}(p  u)
12.  \mneg{}False
\mvdash{}  permutation(\{a:A|  \muparrow{}(p  a)\}  ;filter(p;v);filter(p;as)  @  filter(p;bs))


By

---

Latex:
((RWO  "filter\_append\_sq<"  0  THENA  Auto)\mcdot{}  THEN  BackThruSomeHyp  THEN  Auto)

---

Home Index