Step * 2 2 2 of Lemma permr_iff_eq_counts


1. DSet
2. |s|
3. |s| List
4. ∀bs:|s| List. ((∀x:|s|. ((x #∈ v) (x #∈ bs) ∈ ℤ))  (↑(v ≡b bs)))
5. bs |s| List
6. ∀x:|s|. ((b2i(u (=bx) (x #∈ v)) (x #∈ bs) ∈ ℤ)
7. ↑(u ∈b bs)
⊢ ↑(v ≡b (bs u))
BY
((BackThruSomeHyp THEN Auto) THEN With (D 6) THEN Auto) }

1
1. DSet
2. |s|
3. |s| List
4. ∀bs:|s| List. ((∀x:|s|. ((x #∈ v) (x #∈ bs) ∈ ℤ))  (↑(v ≡b bs)))
5. bs |s| List
6. ↑(u ∈b bs)
7. |s|
8. (b2i(u (=bx) (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