---

Step * 1 1 1 1 2 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)|| + 1) = ((||v|| + 1) - 0 + reduce(λa,n. (if eq x a then 1 else 0 fi  + n);0;v)) ∈ ℤ
BY
{ (Subst ⌜(||v|| + 1) - 0 + 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))
          + 1⌝ 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.  \mneg{}(x  =  u)
\mvdash{}  (||filter(\mlambda{}y.(\mneg{}\msubb{}(eq  x  y));v)||  +  1)
=  ((||v||  +  1)  -  0  +  reduce(\mlambda{}a,n.  (if  eq  x  a  then  1  else  0  fi    +  n);0;v))


By

---

Latex:
(Subst  \mkleeneopen{}(||v||  +  1)  -  0  +  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))
                +  1\mkleeneclose{}  0\mcdot{}
  THEN  Auto
  )

---

Home Index