---

Step * 1 1 1 1 2 1 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)||)
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 ||
BY
{ ((InstLemma `upto_decomp2` [⌜||v|| + 1⌝]⋅ THENA Auto)
   THEN RWO "-1" 0
   THEN (Subst' (||v|| + 1) - 1 ~ ||v|| 0 THENA Auto)
   THEN Reduce 0
   THEN (BoolCase ⌜isOdd(f u)⌝⋅ THENA Auto)
   THEN RWO "-3< -2<" 0
   THEN (RWO "filter-map" 0 THENA Auto)
   THEN (RWO "map-length" 0 THENA Auto)
   THEN RepUR ``compose`` 0) }

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)||
7. upto(||v|| + 1) ~ [0 / map(λi.(i + 1);upto((||v|| + 1) - 1))]
8. ↑isOdd(f u)
⊢ ||filter(λx.isOdd(f [u / v][x + 1]);upto(||v||))|| + 1 ~ ||filter(λi.isOdd(f v[i]);upto(||v||))|| + 1

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

---

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)||)
5.  f  :  \{x:T|  (x  \mmember{}  [u  /  v])\}    {}\mrightarrow{}  \mBbbZ{}
6.  ||filter(\mlambda{}i.isOdd(f  v[i]);upto(||v||))||  \msim{}  ||filter(\mlambda{}x.isOdd(f  x);v)||
\mvdash{}  ||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:
((InstLemma  `upto\_decomp2`  [\mkleeneopen{}||v||  +  1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO  "-1"  0
  THEN  (Subst'  (||v||  +  1)  -  1  \msim{}  ||v||  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (BoolCase  \mkleeneopen{}isOdd(f  u)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RWO  "-3<  -2<"  0
  THEN  (RWO  "filter-map"  0  THENA  Auto)
  THEN  (RWO  "map-length"  0  THENA  Auto)
  THEN  RepUR  ``compose``  0)

---

Home Index