---

Step * 2 of Lemma permr_iff_eq_counts


1. s : DSet
2. as : |s| List
3. bs : |s| List
⊢ (as ≡(|s|) bs) ⇐ ∀x:|s|. ((x #∈ as) = (x #∈ bs) ∈ ℤ)
BY
{ (((InvertRel 0 THEN (RWH (RevLemmaC `assert_of_bpermr`) 0 THENA Auto)) THEN MoveToConcl 3)
   THEN (ListInd 2)
   THEN Reduce 0
   THEN (UnivCD THENA Auto)) }

1
1. s : DSet
2. bs : |s| List
3. ∀x:|s|. (0 = (x #∈ bs) ∈ ℤ)
⊢ ↑null(bs)

2
1. s : DSet
2. u : |s|
3. v : |s| List
4. ∀bs:|s| List. ((∀x:|s|. ((x #∈ v) = (x #∈ bs) ∈ ℤ)) ⇒ (↑(v ≡b bs)))
5. bs : |s| List
6. ∀x:|s|. ((b2i(u (=b) x) + (x #∈ v)) = (x #∈ bs) ∈ ℤ)
⊢ ↑((u ∈b bs) ∧b (v ≡b (bs \ u)))

---

Latex:

---

Latex:

1.  s  :  DSet
2.  as  :  |s|  List
3.  bs  :  |s|  List
\mvdash{}  (as  \mequiv{}(|s|)  bs)  \mLeftarrow{}{}  \mforall{}x:|s|.  ((x  \#\mmember{}  as)  =  (x  \#\mmember{}  bs))


By

---

Latex:
(((InvertRel  0  THEN  (RWH  (RevLemmaC  `assert\_of\_bpermr`)  0  THENA  Auto))  THEN  MoveToConcl  3)
  THEN  (ListInd  2)
  THEN  Reduce  0
  THEN  (UnivCD  THENA  Auto))

---

Home Index