---

Step * 2 of Lemma permutation-iff-count1


1. ∀[T:Type]
     ∀eq:T ⟶ T ⟶ 𝔹
       ((∀x,y:T.  (↑(eq x y) ⇐⇒ x = y ∈ T))
       ⇒ (∀a1,b1:T List.  ((∀x:T. (||filter(eq x;a1)|| = ||filter(eq x;b1)|| ∈ ℤ)) ⇒ permutation(T;a1;b1))))
⊢ ∀[T:Type]
    ∀eq:T ⟶ T ⟶ 𝔹
      ((∀x,y:T.  (↑(eq x y) ⇐⇒ x = y ∈ T))
      ⇒ (∀a1,b1:T List.  (∀x:T. (||filter(eq x;a1)|| = ||filter(eq x;b1)|| ∈ ℤ) ⇐⇒ permutation(T;a1;b1))))
BY
{ (RepeatFor 4 (ParallelLast) THEN Auto)⋅ }

1
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)|| ∈ ℤ

---

Latex:

---

Latex:

1.  \mforall{}[T:Type]
          \mforall{}eq:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
              ((\mforall{}x,y:T.    (\muparrow{}(eq  x  y)  \mLeftarrow{}{}\mRightarrow{}  x  =  y))
              {}\mRightarrow{}  (\mforall{}a1,b1:T  List.
                          ((\mforall{}x:T.  (||filter(eq  x;a1)||  =  ||filter(eq  x;b1)||))  {}\mRightarrow{}  permutation(T;a1;b1))))
\mvdash{}  \mforall{}[T:Type]
        \mforall{}eq:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
            ((\mforall{}x,y:T.    (\muparrow{}(eq  x  y)  \mLeftarrow{}{}\mRightarrow{}  x  =  y))
            {}\mRightarrow{}  (\mforall{}a1,b1:T  List.
                        (\mforall{}x:T.  (||filter(eq  x;a1)||  =  ||filter(eq  x;b1)||)  \mLeftarrow{}{}\mRightarrow{}  permutation(T;a1;b1))))


By

---

Latex:
(RepeatFor  4  (ParallelLast)  THEN  Auto)\mcdot{}

---

Home Index