---

Step * of Lemma single-valued-bag-append

No Annotations
∀[A:Type]. ∀[as,bs:bag(A)].
  (single-valued-bag(as + bs;A)) supposing 
     (similar-bags(A;as;bs) and 
     single-valued-bag(as;A) and 
     single-valued-bag(bs;A))
BY
{ (Auto
   THEN All (Unfold `single-valued-bag`)
   THEN Auto
   THEN BagMemberD (-2)
   THEN BagMemberD (-1)
   THEN SquashExRepD
   THEN ThinTrivial
   THEN SplitOrHyps
   THEN Auto
   THEN Unfold `similar-bags` (-5)
   THEN (Assert ⌜(#(as) = 0 ∈ ℤ) ∨ 0 < #(as)⌝⋅ THEN Auto')
   THEN Assert ⌜(#(bs) = 0 ∈ ℤ) ∨ 0 < #(bs)⌝⋅
   THEN Auto'
   THEN SplitOrHyps
   THEN Try (Complete (Auto))) }

1
1. A : Type
2. as : bag(A)
3. bs : bag(A)
4. ∀x,y:A.  (x ↓∈ bs ⇒ y ↓∈ bs ⇒ (x = y ∈ A))
5. ∀x,y:A.  (x ↓∈ as ⇒ y ↓∈ as ⇒ (x = y ∈ A))
6. ∀a:A. (a ↓∈ as ∧ 0 < #(bs) ⇐⇒ a ↓∈ bs ∧ 0 < #(as))
7. x : A
8. y : A
9. x ↓∈ bs
10. y ↓∈ as
11. #(as) = 0 ∈ ℤ
12. #(bs) = 0 ∈ ℤ
⊢ x = y ∈ A

2
1. A : Type
2. as : bag(A)
3. bs : bag(A)
4. ∀x,y:A.  (x ↓∈ bs ⇒ y ↓∈ bs ⇒ (x = y ∈ A))
5. ∀x,y:A.  (x ↓∈ as ⇒ y ↓∈ as ⇒ (x = y ∈ A))
6. ∀a:A. (a ↓∈ as ∧ 0 < #(bs) ⇐⇒ a ↓∈ bs ∧ 0 < #(as))
7. x : A
8. y : A
9. x ↓∈ as
10. y ↓∈ bs
11. #(as) = 0 ∈ ℤ
12. #(bs) = 0 ∈ ℤ
⊢ x = y ∈ A

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:Type].  \mforall{}[as,bs:bag(A)].
    (single-valued-bag(as  +  bs;A))  supposing 
          (similar-bags(A;as;bs)  and 
          single-valued-bag(as;A)  and 
          single-valued-bag(bs;A))


By

---

Latex:
(Auto
  THEN  All  (Unfold  `single-valued-bag`)
  THEN  Auto
  THEN  BagMemberD  (-2)
  THEN  BagMemberD  (-1)
  THEN  SquashExRepD
  THEN  ThinTrivial
  THEN  SplitOrHyps
  THEN  Auto
  THEN  Unfold  `similar-bags`  (-5)
  THEN  (Assert  \mkleeneopen{}(\#(as)  =  0)  \mvee{}  0  <  \#(as)\mkleeneclose{}\mcdot{}  THEN  Auto')
  THEN  Assert  \mkleeneopen{}(\#(bs)  =  0)  \mvee{}  0  <  \#(bs)\mkleeneclose{}\mcdot{}
  THEN  Auto'
  THEN  SplitOrHyps
  THEN  Try  (Complete  (Auto)))

---

Home Index