---

Step * 1 2 2 1 of Lemma bag-union-is-single


1. T : Type
2. x : T
3. v : bag(T) List
4. bag-union(v) = {x} ∈ bag(T)
5. bbs' : bag(bag(T))
6. v = {x}.bbs' ∈ bag(bag(T))
7. bag-union(bbs') = {} ∈ bag(T)
⊢ {}.{x}.bbs' = {x}.{}.bbs' ∈ bag(bag(T))
BY
{ ((Subst ⌜{}.{x}.bbs' ~ {{}} + {{x}} + bbs'⌝ 0⋅ THENA (RepUR ``single-bag cons-bag empty-bag bag-append`` 0 THEN Auto))
   THEN (Subst ⌜{x}.{}.bbs' ~ {{x}} + {{}} + bbs'⌝ 0⋅
         THENA (RepUR ``single-bag cons-bag empty-bag bag-append`` 0 THEN Auto)
         )
   THEN BLemma `bag-append-assoc-comm`
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  T
3.  v  :  bag(T)  List
4.  bag-union(v)  =  \{x\}
5.  bbs'  :  bag(bag(T))
6.  v  =  \{x\}.bbs'
7.  bag-union(bbs')  =  \{\}
\mvdash{}  \{\}.\{x\}.bbs'  =  \{x\}.\{\}.bbs'


By

---

Latex:
((Subst  \mkleeneopen{}\{\}.\{x\}.bbs'  \msim{}  \{\{\}\}  +  \{\{x\}\}  +  bbs'\mkleeneclose{}  0\mcdot{}
    THENA  (RepUR  ``single-bag  cons-bag  empty-bag  bag-append``  0  THEN  Auto)
    )
  THEN  (Subst  \mkleeneopen{}\{x\}.\{\}.bbs'  \msim{}  \{\{x\}\}  +  \{\{\}\}  +  bbs'\mkleeneclose{}  0\mcdot{}
              THENA  (RepUR  ``single-bag  cons-bag  empty-bag  bag-append``  0  THEN  Auto)
              )
  THEN  BLemma  `bag-append-assoc-comm`
  THEN  Auto)

---

Home Index