---

Step * of Lemma sub-bag-of-bag-rep

∀[T:Type]. ∀x:T. ∀n:ℕ.  ∀[b:bag(T)]. b = bag-rep(#(b);x) ∈ bag(T) supposing sub-bag(T;b;bag-rep(n;x))
BY
{ (Auto
   THEN (Assert single-valued-bag(b;T) BY
               (D 0
                THEN Auto
                THEN RepeatFor 2 ((FLemma `sub-bag-member` [5;-2] THENA Auto))
                THEN RepeatFor 2 ((FLemma `member-bag-rep` [-2] THENA Auto))
                THEN Auto))
   THEN ( Decide ⌜#(b) = 0 ∈ ℤ⌝⋅ THENA Auto)) }

1
1. T : Type
2. x : T@i
3. n : ℕ@i
4. b : bag(T)
5. sub-bag(T;b;bag-rep(n;x))
6. single-valued-bag(b;T)
7. #(b) = 0 ∈ ℤ
⊢ b = bag-rep(#(b);x) ∈ bag(T)

2
1. T : Type
2. x : T@i
3. n : ℕ@i
4. b : bag(T)
5. sub-bag(T;b;bag-rep(n;x))
6. single-valued-bag(b;T)
7. ¬(#(b) = 0 ∈ ℤ)
⊢ b = bag-rep(#(b);x) ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x:T.  \mforall{}n:\mBbbN{}.    \mforall{}[b:bag(T)].  b  =  bag-rep(\#(b);x)  supposing  sub-bag(T;b;bag-rep(n;x))


By

---

Latex:
(Auto
  THEN  (Assert  single-valued-bag(b;T)  BY
                          (D  0
                            THEN  Auto
                            THEN  RepeatFor  2  ((FLemma  `sub-bag-member`  [5;-2]  THENA  Auto))
                            THEN  RepeatFor  2  ((FLemma  `member-bag-rep`  [-2]  THENA  Auto))
                            THEN  Auto))
  THEN  (  Decide  \mkleeneopen{}\#(b)  =  0\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index