---

Step * of Lemma count-append

∀[A:Type]. ∀[P:A ⟶ 𝔹]. ∀[L1,L2:A List].  (count(P;L1 @ L2) ~ count(P;L1) + count(P;L2))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `count` 0
   THEN (RWO  "reduce-append" 0 THENA Auto)
   THEN ListInd (-2)
   THEN Reduce 0
   THEN Try (AutoSplit)) }

1
1. A : Type
2. P : A ⟶ 𝔹
3. L2 : A List
⊢ reduce(λa,n. (if P a then 1 else 0 fi  + n);0;L2) ~ 0 + reduce(λa,n. (if P a then 1 else 0 fi  + n);0;L2)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L1,L2:A  List].    (count(P;L1  @  L2)  \msim{}  count(P;L1)  +  count(P;L2))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `count`  0
  THEN  (RWO    "reduce-append"  0  THENA  Auto)
  THEN  ListInd  (-2)
  THEN  Reduce  0
  THEN  Try  (AutoSplit))

---

Home Index