---

Step * 1 of Lemma bag-append-eq-empty


1. T : Type
2. b1 : bag(T)
3. b2 : bag(T)
4. (b1 + b2) = {} ∈ bag(T)
⊢ (b1 = {} ∈ bag(T)) ∧ (b2 = {} ∈ bag(T))
BY
{ TACTIC:TACTIC:((Assert (b1 + b2) = {} ∈ (Top List) BY
                        (SubsumeC ⌜bag(T)⌝⋅ THEN Auto))
                 THEN RepUR ``bag-append empty-bag`` (-1)
                 THEN (RWO "append_is_nil" (-1) THENA Auto)
                 THEN ParallelLast
                 THEN Fold `empty-bag` (-1)) }

1
1. T : Type
2. b1 : bag(T)
3. b2 : bag(T)
4. (b1 + b2) = {} ∈ bag(T)
5. b2 = [] ∈ (Top List)
6. b1 = {} ∈ (Top List)
⊢ b1 = {} ∈ bag(T)

2
1. T : Type
2. b1 : bag(T)
3. b2 : bag(T)
4. (b1 + b2) = {} ∈ bag(T)
5. b1 = [] ∈ (Top List)
6. b2 = {} ∈ (Top List)
⊢ b2 = {} ∈ bag(T)

---

Latex:

---

Latex:

1.  T  :  Type
2.  b1  :  bag(T)
3.  b2  :  bag(T)
4.  (b1  +  b2)  =  \{\}
\mvdash{}  (b1  =  \{\})  \mwedge{}  (b2  =  \{\})


By

---

Latex:
TACTIC:TACTIC:((Assert  (b1  +  b2)  =  \{\}  BY
                                            (SubsumeC  \mkleeneopen{}bag(T)\mkleeneclose{}\mcdot{}  THEN  Auto))
                              THEN  RepUR  ``bag-append  empty-bag``  (-1)
                              THEN  (RWO  "append\_is\_nil"  (-1)  THENA  Auto)
                              THEN  ParallelLast
                              THEN  Fold  `empty-bag`  (-1))

---

Home Index