---

Step * 1 of Lemma bag-count_wf


1. T : Type
2. eq : EqDecider(T)
3. x : T
4. as : T List
5. bs : T List
6. permutation(T;as;bs)
7. a1 : T List
8. a : T
9. count(eq x;[a / a1]) = count(eq x;bs) ∈ ℕ
⊢ count(eq x;a1 @ [a]) = count(eq x;[a / a1]) ∈ ℕ
BY
{ xxx((RWW "count-append count-single" 0 THENA Auto)
      THEN Unfold `count` 0
      THEN Reduce 0
      THEN Fold `count` 0⋅
      THEN AutoSplit)⋅xxx }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  T
4.  as  :  T  List
5.  bs  :  T  List
6.  permutation(T;as;bs)
7.  a1  :  T  List
8.  a  :  T
9.  count(eq  x;[a  /  a1])  =  count(eq  x;bs)
\mvdash{}  count(eq  x;a1  @  [a])  =  count(eq  x;[a  /  a1])


By

---

Latex:
xxx((RWW  "count-append  count-single"  0  THENA  Auto)
        THEN  Unfold  `count`  0
        THEN  Reduce  0
        THEN  Fold  `count`  0\mcdot{}
        THEN  AutoSplit)\mcdot{}xxx

---

Home Index