Step
*
2
2
2
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) ∈ ℤ)
7. ↑(u ∈b bs)
⊢ ↑(v ≡b (bs \ u))
BY
{ ((BackThruSomeHyp THEN Auto) THEN With x (D 6) THEN Auto) }
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. ↑(u ∈b bs)
7. x : |s|
8. (b2i(u (=b) x) + (x #∈ v)) = (x #∈ bs) ∈ ℤ
⊢ (x #∈ v) = (x #∈ (bs \ u)) ∈ ℤ
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))
7. \muparrow{}(u \mmember{}\msubb{} bs)
\mvdash{} \muparrow{}(v \mequiv{}\msubb{} (bs \mbackslash{} u))
By
Latex:
((BackThruSomeHyp THEN Auto) THEN With x (D 6) THEN Auto)
Home
Index