---

Step * 1 of Lemma permutation-iff-count1

.....assertion..... 
∀[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 2 (InductionOnList) THEN Auto) }

1
1. [T] : Type
2. eq : T ⟶ T ⟶ 𝔹
3. ∀x,y:T.  (↑(eq x y) ⇐⇒ x = y ∈ T)
4. u : T
5. v : T List
6. (∀x:T. (||filter(eq x;[])|| = ||filter(eq x;v)|| ∈ ℤ)) ⇒ permutation(T;[];v)
7. ∀x:T. (||filter(eq x;[])|| = ||filter(eq x;[u / v])|| ∈ ℤ)
⊢ permutation(T;[];[u / v])

2
1. [T] : Type
2. eq : T ⟶ T ⟶ 𝔹
3. ∀x,y:T.  (↑(eq x y) ⇐⇒ x = y ∈ T)
4. u : T
5. v : T List
6. ∀b1:T List. ((∀x:T. (||filter(eq x;v)|| = ||filter(eq x;b1)|| ∈ ℤ)) ⇒ permutation(T;v;b1))
7. ∀x:T. (||filter(eq x;[u / v])|| = ||filter(eq x;[])|| ∈ ℤ)
⊢ permutation(T;[u / v];[])

3
1. [T] : Type
2. eq : T ⟶ T ⟶ 𝔹
3. ∀x,y:T.  (↑(eq x y) ⇐⇒ x = y ∈ T)
4. u : T
5. v : T List
6. ∀b1:T List. ((∀x:T. (||filter(eq x;v)|| = ||filter(eq x;b1)|| ∈ ℤ)) ⇒ permutation(T;v;b1))
7. u1 : T
8. v1 : T List
9. (∀x:T. (||filter(eq x;[u / v])|| = ||filter(eq x;v1)|| ∈ ℤ)) ⇒ permutation(T;[u / v];v1)
10. ∀x:T. (||filter(eq x;[u / v])|| = ||filter(eq x;[u1 / v1])|| ∈ ℤ)
⊢ permutation(T;[u / v];[u1 / v1])

---

Latex:

---

Latex:
.....assertion..... 
\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))))


By

---

Latex:
(RepeatFor  2  (InductionOnList)  THEN  Auto)

---

Home Index