---

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


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)) ∈ ℤ
BY
{ (Subst ⌜(||v|| + 1) - 1 + reduce(λa,n. (if eq x a then 1 else 0 fi  + n);0;v) ~ ||v|| - reduce(λa,n. (if eq x a
                                                                                                  then 1
                                                                                                  else 0
                                                                                                  fi 
                                                                                                  + n);0;v)⌝ 0⋅
   THEN Auto
   ) }

---

Latex:

---

Latex:

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


By

---

Latex:
(Subst  \mkleeneopen{}(||v||  +  1)  -  1  +  reduce(\mlambda{}a,n.  (if  eq  x  a  then  1  else  0  fi    +  n);0;v)  \msim{}  ||v|| 
                -  reduce(\mlambda{}a,n.  (if  eq  x  a  then  1  else  0  fi    +  n);0;v)\mkleeneclose{}  0\mcdot{}
  THEN  Auto
  )

---

Home Index