---

Step * 1 1 1 1 2 of Lemma odd-l_sum


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 ||)
BY
{ ParallelLast }

1
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)||)
5. f : {x:T| (x ∈ [u / v])}  ⟶ ℤ
6. ||filter(λi.isOdd(f v[i]);upto(||v||))|| ~ ||filter(λx.isOdd(f x);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:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}f:\{x:T|  (x  \mmember{}  v)\}    {}\mrightarrow{}  \mBbbZ{}.  (||filter(\mlambda{}i.isOdd(f  v[i]);upto(||v||))||  \msim{}  ||filter(\mlambda{}x.isOdd(f  x);v)||)
\mvdash{}  \mforall{}f:\{x:T|  (x  \mmember{}  [u  /  v])\}    {}\mrightarrow{}  \mBbbZ{}
        (||filter(\mlambda{}i.isOdd(f  [u  /  v][i]);upto(||v||  +  1))||  \msim{}  ||if  isOdd(f  u)
        then  [u  /  filter(\mlambda{}x.isOdd(f  x);v)]
        else  filter(\mlambda{}x.isOdd(f  x);v)
        fi  ||)


By

---

Latex:
ParallelLast

---

Home Index