---

Step * 1 of Lemma permutation-iff-count

.....assertion..... 
∀[T:Type]
  ∀eq:EqDecider(T). ∀a1,b1:T List.
    ((∀x:T. (||filter(eqof(eq) x;a1)|| = ||filter(eqof(eq) x;b1)|| ∈ ℤ)) ⇒ permutation(T;a1;b1))
BY
{ (RepeatFor 2 (InductionOnList) THEN Auto) }

1
1. [T] : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. (∀x:T. (||filter(eqof(eq) x;[])|| = ||filter(eqof(eq) x;v)|| ∈ ℤ)) ⇒ permutation(T;[];v)
6. ∀x:T. (||filter(eqof(eq) x;[])|| = ||filter(eqof(eq) x;[u / v])|| ∈ ℤ)
⊢ permutation(T;[];[u / v])

2
1. [T] : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. ∀b1:T List. ((∀x:T. (||filter(eqof(eq) x;v)|| = ||filter(eqof(eq) x;b1)|| ∈ ℤ)) ⇒ permutation(T;v;b1))
6. ∀x:T. (||filter(eqof(eq) x;[u / v])|| = ||filter(eqof(eq) x;[])|| ∈ ℤ)
⊢ permutation(T;[u / v];[])

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

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}a1,b1:T  List.
        ((\mforall{}x:T.  (||filter(eqof(eq)  x;a1)||  =  ||filter(eqof(eq)  x;b1)||))  {}\mRightarrow{}  permutation(T;a1;b1))


By

---

Latex:
(RepeatFor  2  (InductionOnList)  THEN  Auto)

---

Home Index