---

Step * of Lemma bag-rep-size-restrict

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[b:bag(T)].  (bag-rep(#((b|x));x) = (b|x) ∈ bag(T))
BY
{ xxx(Auto
      THEN BagToList (-1)
      THEN Auto
      THEN RepUR ``bag-rep bag-size bag-restrict bag-filter`` 0
      THEN ListInd (-1)
      THEN Reduce 0
      THEN Auto)xxx }

1
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. u : T
5. v : T List
6. primrec(||filter(λz.(eq x z);v)||;{};λi,r. x.r) = filter(λz.(eq x z);v) ∈ bag(T)
⊢ primrec(||if eq x u then [u / filter(λz.(eq x z);v)] else filter(λz.(eq x z);v) fi ||;{};λi,r. x.r)
= if eq x u then [u / filter(λz.(eq x z);v)] else filter(λz.(eq x z);v) fi 
∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[b:bag(T)].    (bag-rep(\#((b|x));x)  =  (b|x))


By

---

Latex:
xxx(Auto
        THEN  BagToList  (-1)
        THEN  Auto
        THEN  RepUR  ``bag-rep  bag-size  bag-restrict  bag-filter``  0
        THEN  ListInd  (-1)
        THEN  Reduce  0
        THEN  Auto)xxx

---

Home Index