---

Step * 2 2 1 of Lemma permr_iff_eq_counts


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)
BY
{ ((D -1 With ⌜u⌝  THENA Auto) THEN (RWH (LemmaC `dset_eq_refl`) (-1) THENA Auto) THEN Reduce -1) }

1
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. (1 + (u #∈ v)) = (u #∈ bs) ∈ ℤ
⊢ ↑(u ∈b bs)

---

Latex:

---

Latex:

1.  s  :  DSet
2.  u  :  |s|
3.  v  :  |s|  List
4.  \mforall{}bs:|s|  List.  ((\mforall{}x:|s|.  ((x  \#\mmember{}  v)  =  (x  \#\mmember{}  bs)))  {}\mRightarrow{}  (\muparrow{}(v  \mequiv{}\msubb{}  bs)))
5.  bs  :  |s|  List
6.  \mforall{}x:|s|.  ((b2i(u  (=\msubb{})  x)  +  (x  \#\mmember{}  v))  =  (x  \#\mmember{}  bs))
\mvdash{}  \muparrow{}(u  \mmember{}\msubb{}  bs)


By

---

Latex:
((D  -1  With  \mkleeneopen{}u\mkleeneclose{}    THENA  Auto)  THEN  (RWH  (LemmaC  `dset\_eq\_refl`)  (-1)  THENA  Auto)  THEN  Reduce  -1)

---

Home Index