---

Step * 1 1 1 1 of Lemma odd-l_sum

.....equality..... 
1. T : Type
2. L : T List
3. f : {x:T| (x ∈ L)}  ⟶ ℤ
4. l_sum(map(f;L)) = Σ(f L[i] | i < ||L||) ∈ ℤ
⊢ ||filter(λi.isOdd(f L[i]);upto(||L||))|| ~ ||filter(λx.isOdd(f x);L)||
BY
{ (Thin (-1) THEN ListInd 2 THEN Reduce 0) }

1
1. T : Type
⊢ ∀f:{x:T| (x ∈ [])}  ⟶ ℤ. (0 ~ 0)

2
1. T : Type
2. u : T
3. v : T List
4. ∀f:{x:T| (x ∈ v)}  ⟶ ℤ. (||filter(λi.isOdd(f v[i]);upto(||v||))|| ~ ||filter(λx.isOdd(f x);v)||)
⊢ ∀f:{x:T| (x ∈ [u / v])}  ⟶ ℤ
    (||filter(λi.isOdd(f [u / v][i]);upto(||v|| + 1))|| ~ ||if isOdd(f u)
    then [u / filter(λx.isOdd(f x);v)]
    else filter(λx.isOdd(f x);v)
    fi ||)

---

Latex:

---

Latex:
.....equality..... 
1.  T  :  Type
2.  L  :  T  List
3.  f  :  \{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbZ{}
4.  l\_sum(map(f;L))  =  \mSigma{}(f  L[i]  |  i  <  ||L||)
\mvdash{}  ||filter(\mlambda{}i.isOdd(f  L[i]);upto(||L||))||  \msim{}  ||filter(\mlambda{}x.isOdd(f  x);L)||


By

---

Latex:
(Thin  (-1)  THEN  ListInd  2  THEN  Reduce  0)

---

Home Index