---

Step * of Lemma permutation-iff-count

∀[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
{ Assert ⌜∀[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))⌝⋅ }

1
.....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))

2
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))

---

Latex:

---

Latex:
\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:
Assert  \mkleeneopen{}\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))\mkleeneclose{}\mcdot{}

---

Home Index