---

Step * 1 1 of Lemma count-bag-remove-repeats


1. T : Type
2. eq : EqDecider(T)
3. x : T
4. b2 : T List
5. 1 ≤ ||filter(eq x;list-to-set(eq;b2))|| ⇐⇒ (x ∈ b2)
⊢ ||filter(λy.(eq x y);list-to-set(eq;b2))|| = if x ∈b b2 then 1 else 0 fi  ∈ ℕ
BY
{ TACTIC:Subst' ||filter(λy.(eq x y);list-to-set(eq;b2))|| ~ ||filter(eq x;list-to-set(eq;b2))|| 0 }

1
.....equality..... 
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. b2 : T List
5. 1 ≤ ||filter(eq x;list-to-set(eq;b2))|| ⇐⇒ (x ∈ b2)
⊢ ||filter(λy.(eq x y);list-to-set(eq;b2))|| ~ ||filter(eq x;list-to-set(eq;b2))||

2
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. b2 : T List
5. 1 ≤ ||filter(eq x;list-to-set(eq;b2))|| ⇐⇒ (x ∈ b2)
⊢ ||filter(eq x;list-to-set(eq;b2))|| = if x ∈b b2 then 1 else 0 fi  ∈ ℕ

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  T
4.  b2  :  T  List
5.  1  \mleq{}  ||filter(eq  x;list-to-set(eq;b2))||  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  b2)
\mvdash{}  ||filter(\mlambda{}y.(eq  x  y);list-to-set(eq;b2))||  =  if  x  \mmember{}\msubb{}  b2  then  1  else  0  fi 


By

---

Latex:
TACTIC:Subst'  ||filter(\mlambda{}y.(eq  x  y);list-to-set(eq;b2))||  \msim{}  ||filter(eq  x;list-to-set(eq;b2))||  0

---

Home Index