---

Step * 1 of Lemma apply-alist-count-repeats

.....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) ⟶ ℙ
BY
{ (RepeatFor 2 ((MemCD THENA Auto)) THEN Try (AutoSplit) THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. L : T List
5. (x ∈ L)
⊢ ||filter(λy.(eq y x);L)|| ∈ ℕ+

---

Latex:

---

Latex:
.....wf..... 
1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  T
\mvdash{}  \mlambda{}L.(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  )  \mmember{}  (T  List)  {}\mrightarrow{}  \mBbbP{}


By

---

Latex:
(RepeatFor  2  ((MemCD  THENA  Auto))  THEN  Try  (AutoSplit)  THEN  Auto)

---

Home Index