---

Step * 2 1 of Lemma permutation-iff-count


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)|| ∈ ℤ
BY
{ ((BLemma `permutation-length` THEN Auto)
   THEN InstLemma `permutation-filter` [⌜T⌝;⌜a1⌝;⌜b1⌝;⌜eqof(eq) x⌝]⋅
   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
8. {permutation({a:T| ↑(eqof(eq) x a)} ;filter(eqof(eq) x;a1);filter(eqof(eq) x;b1))}
9. permutation({a:T| ↑(eqof(eq) x a)} ;filter(eqof(eq) x;a1);filter(eqof(eq) x;b1))
⊢ ...system_error_message... permutation(T;filter(eqof(eq) x;a1);filter(eqof(eq) x;b1))

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)@i
3.  a1  :  T  List@i
4.  b1  :  T  List@i
5.  (\mforall{}x:T.  (||filter(eqof(eq)  x;a1)||  =  ||filter(eqof(eq)  x;b1)||))  {}\mRightarrow{}  permutation(T;a1;b1)
6.  permutation(T;a1;b1)
7.  x  :  T@i
\mvdash{}  ||filter(eqof(eq)  x;a1)||  =  ||filter(eqof(eq)  x;b1)||


By

---

Latex:
((BLemma  `permutation-length`  THEN  Auto)
  THEN  InstLemma  `permutation-filter`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}eqof(eq)  x\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index