---

Step * 2 of Lemma bag-filter-as-accum


1. A : Type
2. p : A ⟶ 𝔹
3. L : A List
4. bs : bag(A)
5. bs = L ∈ bag(A)
6. z : bag(A)
7. b : bag({x:A| ↑p[x]} )
8. x : A
9. y : A
⊢ if p[x] then x.if p[y] then y.b else b fi 
if p[y] then y.b
else b
fi 
= if p[y] then y.if p[x] then x.b else b fi 
  if p[x] then x.b
  else b
  fi 
∈ bag({x:A| ↑p[x]} )
BY
{ (Repeat AutoSplit
   THEN Repeat ((RWO "cons-bag-as-append" 0 THENA Auto))
   THEN (RWO "bag-append-assoc<" 0 THENA Auto)
   THEN (MemCD THEN Auto)
   THEN BLemma `bag-append-comm`
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  p  :  A  {}\mrightarrow{}  \mBbbB{}
3.  L  :  A  List
4.  bs  :  bag(A)
5.  bs  =  L
6.  z  :  bag(A)
7.  b  :  bag(\{x:A|  \muparrow{}p[x]\}  )
8.  x  :  A
9.  y  :  A
\mvdash{}  if  p[x]  then  x.if  p[y]  then  y.b  else  b  fi 
if  p[y]  then  y.b
else  b
fi 
=  if  p[y]  then  y.if  p[x]  then  x.b  else  b  fi 
    if  p[x]  then  x.b
    else  b
    fi 


By

---

Latex:
(Repeat  AutoSplit
  THEN  Repeat  ((RWO  "cons-bag-as-append"  0  THENA  Auto))
  THEN  (RWO  "bag-append-assoc<"  0  THENA  Auto)
  THEN  (MemCD  THEN  Auto)
  THEN  BLemma  `bag-append-comm`
  THEN  Auto)

---

Home Index