---

Step * of Lemma permutation-split

∀[A:Type]. ∀p:A ⟶ 𝔹. ∀L:A List.  permutation(A;filter(λx.p[x];L) @ filter(λx.(¬bp[x]);L);L)
BY
{ (InductionOnList THEN Reduce 0 THEN Auto) }

1
1. [A] : Type
2. p : A ⟶ 𝔹
3. u : A
4. v : A List
5. permutation(A;filter(λx.p[x];v) @ filter(λx.(¬bp[x]);v);v)
⊢ permutation(A;if p[u] then [u / filter(λx.p[x];v)] else filter(λx.p[x];v) fi 
              @ if ¬bp[u] then [u / filter(λx.(¬bp[x]);v)] else filter(λx.(¬bp[x]);v) fi ;[u / v])

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}p:A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:A  List.    permutation(A;filter(\mlambda{}x.p[x];L)  @  filter(\mlambda{}x.(\mneg{}\msubb{}p[x]);L);L)


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto)

---

Home Index