---

Step * 2 1 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
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))
BY
{ TACTIC:(Unfold `label` 0 THEN RepeatFor 4 (ParallelLast)) }

---

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
8.  \{permutation(\{a:T|  \muparrow{}(eqof(eq)  x  a)\}  ;filter(eqof(eq)  x;a1);filter(eqof(eq)  x;b1))\}
9.  permutation(\{a:T|  \muparrow{}(eqof(eq)  x  a)\}  ;filter(eqof(eq)  x;a1);filter(eqof(eq)  x;b1))
\mvdash{}  ...system\_error\_message...  permutation(T;filter(eqof(eq)  x;a1);filter(eqof(eq)  x;b1))


By

---

Latex:
TACTIC:(Unfold  `label`  0  THEN  RepeatFor  4  (ParallelLast))

---

Home Index