---

Step * 1 3 of Lemma bag-mapfilter-fast-eq


1. A : Type
2. B : Type
3. L : A List
4. bs : bag(A)
5. P : A ⟶ 𝔹
6. f : {x:A| ↑P[x]}  ⟶ B
7. bs = L ∈ bag(A)
8. z : bag(A)
9. b : bag(B)
10. x : A
11. y : A
⊢ if P[x] then f[x].if P[y] then f[y].b else b fi 
if P[y] then f[y].b
else b
fi 
= if P[y] then f[y].if P[x] then f[x].b else b fi 
  if P[x] then f[x].b
  else b
  fi 
∈ bag(B)
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.  B  :  Type
3.  L  :  A  List
4.  bs  :  bag(A)
5.  P  :  A  {}\mrightarrow{}  \mBbbB{}
6.  f  :  \{x:A|  \muparrow{}P[x]\}    {}\mrightarrow{}  B
7.  bs  =  L
8.  z  :  bag(A)
9.  b  :  bag(B)
10.  x  :  A
11.  y  :  A
\mvdash{}  if  P[x]  then  f[x].if  P[y]  then  f[y].b  else  b  fi 
if  P[y]  then  f[y].b
else  b
fi 
=  if  P[y]  then  f[y].if  P[x]  then  f[x].b  else  b  fi 
    if  P[x]  then  f[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