---

Step * of Lemma bag-count-rep

∀[T:Type]. ∀[n:ℕ]. ∀[eq:EqDecider(T)]. ∀[x,y:T].  ((#x in bag-rep(n;y)) = if eq x y then n else 0 fi  ∈ ℤ)
BY
{ ((PrimrecInductionOn `n' THENA Auto)
   THEN AutoSplit
   THEN (RepUR ``bag-count count cons-bag`` 0
         THEN Fold `count` 0
         THEN Fold `bag-count` 0
         THEN RWO "5" 0
         THEN Auto
         THEN AutoSplit)⋅) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x,y:T].
    ((\#x  in  bag-rep(n;y))  =  if  eq  x  y  then  n  else  0  fi  )


By

---

Latex:
((PrimrecInductionOn  `n'  THENA  Auto)
  THEN  AutoSplit
  THEN  (RepUR  ``bag-count  count  cons-bag``  0
              THEN  Fold  `count`  0
              THEN  Fold  `bag-count`  0
              THEN  RWO  "5"  0
              THEN  Auto
              THEN  AutoSplit)\mcdot{})

---

Home Index