---

Step * 1 of Lemma sv-bag-tail-single-valued


1. A : Type
2. bs : bag(A)
3. single-valued-bag(bs;A)@i
4. 0 < #(bs)@i
⊢ single-valued-bag(sv-bag-tail(bs);A)
BY
{ ((FLemma `single-valued-bag-sv-list` [3] THENA Auto)
   THEN (FLemma `single-valued-bag-is-list` [3] THENA Auto)
   THEN Unfold `bag-size` 4
   THEN (FLemma `sv-list-tail` [5] THEN Auto)
   THEN Unfold `sv-bag-tail` 0) }

1
1. A : Type
2. bs : bag(A)
3. single-valued-bag(bs;A)@i
4. 0 < ||bs||@i
5. single-valued-list(bs;A)
6. bs ∈ A List
7. single-valued-list(tl(bs);A)
⊢ single-valued-bag(tl(bs);A)

---

Latex:

---

Latex:

1.  A  :  Type
2.  bs  :  bag(A)
3.  single-valued-bag(bs;A)@i
4.  0  <  \#(bs)@i
\mvdash{}  single-valued-bag(sv-bag-tail(bs);A)


By

---

Latex:
((FLemma  `single-valued-bag-sv-list`  [3]  THENA  Auto)
  THEN  (FLemma  `single-valued-bag-is-list`  [3]  THENA  Auto)
  THEN  Unfold  `bag-size`  4
  THEN  (FLemma  `sv-list-tail`  [5]  THEN  Auto)
  THEN  Unfold  `sv-bag-tail`  0)

---

Home Index