Step
*
1
of Lemma
bsublist_append_diff
1. s : DSet
2. as : |s| List
3. bs : |s| List
4. ↑bsublist(s;as;bs)
⊢ ((bs - as) @ as) ≡(|s|) bs
BY
{ ((BLemma `permr_iff_eq_counts` THENA Auto)
THEN ((D 0 THENM RewriteWith [] ``count_diff count_append`` 0) THENA Auto)
) }
1
1. s : DSet
2. as : |s| List
3. bs : |s| List
4. ↑bsublist(s;as;bs)
5. x : |s|
⊢ (((x #∈ bs) -- (x #∈ as)) + (x #∈ as)) = (x #∈ bs) ∈ ℤ
Latex:
Latex:
1. s : DSet
2. as : |s| List
3. bs : |s| List
4. \muparrow{}bsublist(s;as;bs)
\mvdash{} ((bs - as) @ as) \mequiv{}(|s|) bs
By
Latex:
((BLemma `permr\_iff\_eq\_counts` THENA Auto)
THEN ((D 0 THENM RewriteWith [] ``count\_diff count\_append`` 0) THENA Auto)
)
Home
Index