---

Step * 2 of Lemma permutation-iff-count


1. ∀[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))
⊢ ∀[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 4 (ParallelLast) THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)@i
3. a1 : T List@i
4. b1 : T List@i
5. (∀x:T. (||filter(eqof(eq) x;a1)|| = ||filter(eqof(eq) x;b1)|| ∈ ℤ)) ⇒ permutation(T;a1;b1)
6. permutation(T;a1;b1)
7. x : T@i
⊢ ||filter(eqof(eq) x;a1)|| = ||filter(eqof(eq) x;b1)|| ∈ ℤ

---

Latex:

---

Latex:

1.  \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))
\mvdash{}  \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)||)  \mLeftarrow{}{}\mRightarrow{}  permutation(T;a1;b1))


By

---

Latex:
(RepeatFor  4  (ParallelLast)  THEN  Auto)

---

Home Index