---

Step * 4 of Lemma fset_of_mset_mem


1. s : DSet
2. c : |s|
⊢ ∀ys,ys':MSet{s}.
    (c ∈b fset_of_mset(s;ys) = c ∈b ys
    ⇒ c ∈b fset_of_mset(s;ys') = c ∈b ys'
    ⇒ c ∈b fset_of_mset(s;ys + ys') = c ∈b ys + ys')
BY
{ ((RepD 
THENM Unfold `fset_of_mset` 0 
THENM RWH (LemmaC `mset_mem_char`) 0 
THENM RW mset_for_normC 0 
THENM RWH (RevLemmaC `mset_mem_char`) 0 
THENM Fold `fset_of_mset` 0  
THENM Reduce 0 
) THENA Auto) }

1
1. s : DSet
2. c : |s|
3. ys : MSet{s}
4. ys' : MSet{s}
5. c ∈b fset_of_mset(s;ys) = c ∈b ys
6. c ∈b fset_of_mset(s;ys') = c ∈b ys'
⊢ c ∈b fset_of_mset(s;ys) ⋃ fset_of_mset(s;ys') = (c ∈b ys) ∨b(c ∈b ys')

---

Latex:

---

Latex:

1.  s  :  DSet
2.  c  :  |s|
\mvdash{}  \mforall{}ys,ys':MSet\{s\}.
        (c  \mmember{}\msubb{}  fset\_of\_mset(s;ys)  =  c  \mmember{}\msubb{}  ys
        {}\mRightarrow{}  c  \mmember{}\msubb{}  fset\_of\_mset(s;ys')  =  c  \mmember{}\msubb{}  ys'
        {}\mRightarrow{}  c  \mmember{}\msubb{}  fset\_of\_mset(s;ys  +  ys')  =  c  \mmember{}\msubb{}  ys  +  ys')


By

---

Latex:
((RepD 
THENM  Unfold  `fset\_of\_mset`  0 
THENM  RWH  (LemmaC  `mset\_mem\_char`)  0 
THENM  RW  mset\_for\_normC  0 
THENM  RWH  (RevLemmaC  `mset\_mem\_char`)  0 
THENM  Fold  `fset\_of\_mset`  0   
THENM  Reduce  0 
)  THENA  Auto)

---

Home Index