---

Step * 1 1 of Lemma bag-moebius-property1


1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. b : T List
5. b = {} ∈ bag(T)
⊢ Σ(c∈sub-bags(eq;b)). bag-moebius(eq;c) = 1 ∈ ℤ
BY
{ TACTIC:((HypSubst' (-1) 0 THENA Auto)
          THEN Try ((D 0 THEN Reduce 0 THEN Auto))
          THEN RW (SubC (TagC (mk_tag_term 200))) 0
          THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  valueall-type(T)
3.  eq  :  EqDecider(T)
4.  b  :  T  List
5.  b  =  \{\}
\mvdash{}  \mSigma{}(c\mmember{}sub-bags(eq;b)).  bag-moebius(eq;c)  =  1


By

---

Latex:
TACTIC:((HypSubst'  (-1)  0  THENA  Auto)
                THEN  Try  ((D  0  THEN  Reduce  0  THEN  Auto))
                THEN  RW  (SubC  (TagC  (mk\_tag\_term  200)))  0
                THEN  Auto)

---

Home Index