---

Step * of Lemma filter_functionality_wrt_permutation

∀[A:Type]. ∀L1,L2:A List. ∀p:A ⟶ 𝔹.  (permutation(A;L1;L2) ⇒ permutation(A;filter(p;L1);filter(p;L2)))
BY
{ (InstLemma `permutation-filter` []
   THEN RepeatFor 3 ((ParallelLast' THENA Auto))
   THEN Auto
   THEN ThinTrivial
   THEN InstHyp [⌜p⌝] (-1)⋅
   THEN Auto
   THEN Try (Unfold `label` 0)
   THEN RepeatFor 4 ((ParallelLast' THENA Auto))) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `permutation-filter`  []
  THEN  RepeatFor  3  ((ParallelLast'  THENA  Auto))
  THEN  Auto
  THEN  ThinTrivial
  THEN  InstHyp  [\mkleeneopen{}p\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Auto
  THEN  Try  (Unfold  `label`  0)
  THEN  RepeatFor  4  ((ParallelLast'  THENA  Auto)))

---

Home Index