---

Step * of Lemma permutation-split2

∀[A:Type]
  ∀p,q:A ⟶ 𝔹.  ((∀a:A. (↑q[a] ⇐⇒ ¬↑p[a])) ⇒ (∀L:A List. permutation(A;filter(λx.p[x];L) @ filter(λx.q[x];L);L)))
BY
{ (InstLemma `permutation-split` []
   THEN RepeatFor 2 (ParallelLast')
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN ParallelOp -3
   THEN NthHypEq (-1)
   THEN RepeatFor 4 ((EqCD THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}p,q:A  {}\mrightarrow{}  \mBbbB{}.
        ((\mforall{}a:A.  (\muparrow{}q[a]  \mLeftarrow{}{}\mRightarrow{}  \mneg{}\muparrow{}p[a]))
        {}\mRightarrow{}  (\mforall{}L:A  List.  permutation(A;filter(\mlambda{}x.p[x];L)  @  filter(\mlambda{}x.q[x];L);L)))


By

---

Latex:
(InstLemma  `permutation-split`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  ParallelOp  -3
  THEN  NthHypEq  (-1)
  THEN  RepeatFor  4  ((EqCD  THEN  Auto)))

---

Home Index