---

Step * 1 1 1 1 of Lemma bag-remove-size


1. T : Type
2. eq : EqDecider(T)
3. bs : T List
4. x : T
5. (x ∈ bs)
⊢ ||filter(λy.(¬b(eq x y));bs)|| = (||bs|| - reduce(λa,n. (if eq x a then 1 else 0 fi  + n);0;bs)) ∈ ℤ
BY
{ (Thin (-1)
   THEN MoveToConcl (-1)
   THEN ListInd (-1)
   THEN Reduce 0
   THEN Auto
   THEN AutoSplit
   THEN (All (RW ListC) THENA Auto)) }

1
1. T : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. ∀x:T. (||filter(λy.(¬b(eq x y));v)|| = (||v|| - reduce(λa,n. (if eq x a then 1 else 0 fi  + n);0;v)) ∈ ℤ)
6. x : T
7. x = u ∈ T
⊢ ||filter(λy.(¬b(eq x y));v)|| = ((||v|| + 1) - 1 + reduce(λa,n. (if eq x a then 1 else 0 fi  + n);0;v)) ∈ ℤ

2
1. T : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. ∀x:T. (||filter(λy.(¬b(eq x y));v)|| = (||v|| - reduce(λa,n. (if eq x a then 1 else 0 fi  + n);0;v)) ∈ ℤ)
6. x : T
7. ¬(x = u ∈ T)
⊢ (||filter(λy.(¬b(eq x y));v)|| + 1) = ((||v|| + 1) - 0 + reduce(λa,n. (if eq x a then 1 else 0 fi  + n);0;v)) ∈ ℤ

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  bs  :  T  List
4.  x  :  T
5.  (x  \mmember{}  bs)
\mvdash{}  ||filter(\mlambda{}y.(\mneg{}\msubb{}(eq  x  y));bs)||  =  (||bs||  -  reduce(\mlambda{}a,n.  (if  eq  x  a  then  1  else  0  fi    +  n);0;bs))


By

---

Latex:
(Thin  (-1)
  THEN  MoveToConcl  (-1)
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  AutoSplit
  THEN  (All  (RW  ListC)  THENA  Auto))

---

Home Index