---

Step * 2 1 of Lemma permutation-iff-count1


1. T : Type
2. eq : T ⟶ T ⟶ 𝔹@i
3. ∀x,y:T.  (↑(eq x y) ⇐⇒ x = y ∈ T)
4. a1 : T List@i
5. ∀b1:T List. ((∀x:T. (||filter(eq x;a1)|| = ||filter(eq x;b1)|| ∈ ℤ)) ⇒ permutation(T;a1;b1))
6. b1 : T List@i
7. permutation(T;a1;b1)
8. x : T@i
⊢ ||filter(eq x;a1)|| = ||filter(eq x;b1)|| ∈ ℤ
BY
{ ((BLemma `permutation-length` THEN Auto)
   THEN InstLemma `permutation-filter` [⌜T⌝;⌜a1⌝;⌜b1⌝;⌜eq x⌝]⋅
   THEN Try (Complete (Auto))
   THEN RepeatFor 4 (ParallelLast))⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}@i
3.  \mforall{}x,y:T.    (\muparrow{}(eq  x  y)  \mLeftarrow{}{}\mRightarrow{}  x  =  y)
4.  a1  :  T  List@i
5.  \mforall{}b1:T  List.  ((\mforall{}x:T.  (||filter(eq  x;a1)||  =  ||filter(eq  x;b1)||))  {}\mRightarrow{}  permutation(T;a1;b1))
6.  b1  :  T  List@i
7.  permutation(T;a1;b1)
8.  x  :  T@i
\mvdash{}  ||filter(eq  x;a1)||  =  ||filter(eq  x;b1)||


By

---

Latex:
((BLemma  `permutation-length`  THEN  Auto)
  THEN  InstLemma  `permutation-filter`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}eq  x\mkleeneclose{}]\mcdot{}
  THEN  Try  (Complete  (Auto))
  THEN  RepeatFor  4  (ParallelLast))\mcdot{}

---

Home Index