---

Step * of Lemma apply-alist-count-repeats

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[L:T List].
  (apply-alist(eq;count-repeats(L,eq);x) = if x ∈b L then inl ||filter(λy.(eq y x);L)|| else inr ⋅  fi  ∈ (ℕ+?))
BY
{ (Auto THEN MoveToConcl (-1) THEN (BLemma `last_induction` THENA Try (Complete (Auto)))) }

1
.....wf..... 
1. T : Type
2. eq : EqDecider(T)
3. x : T
⊢ λL.(apply-alist(eq;count-repeats(L,eq);x) = if x ∈b L then inl ||filter(λy.(eq y x);L)|| else inr ⋅  fi  ∈ (ℕ+?))
  ∈ (T List) ⟶ ℙ

2
1. T : Type
2. eq : EqDecider(T)
3. x : T
⊢ apply-alist(eq;count-repeats([],eq);x) = if x ∈b [] then inl ||filter(λy.(eq y x);[])|| else inr ⋅  fi  ∈ (ℕ+?)

3
1. T : Type
2. eq : EqDecider(T)
3. x : T
⊢ ∀ys:T List. ∀y:T.
    ((apply-alist(eq;count-repeats(ys,eq);x) = if x ∈b ys then inl ||filter(λy.(eq y x);ys)|| else inr ⋅  fi  ∈ (ℕ+?))
    ⇒ (apply-alist(eq;count-repeats(ys @ [y],eq);x)
       = if x ∈b ys @ [y] then inl ||filter(λy.(eq y x);ys @ [y])|| else inr ⋅  fi 
       ∈ (ℕ+?)))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[L:T  List].
    (apply-alist(eq;count-repeats(L,eq);x)
    =  if  x  \mmember{}\msubb{}  L  then  inl  ||filter(\mlambda{}y.(eq  y  x);L)||  else  inr  \mcdot{}    fi  )


By

---

Latex:
(Auto  THEN  MoveToConcl  (-1)  THEN  (BLemma  `last\_induction`  THENA  Try  (Complete  (Auto))))

---

Home Index