---

Step * 1 of Lemma isOdd-sum


1. n : ℤ
2. 0 < n
3. ∀[f:ℕn - 1 ⟶ ℤ]. uiff(↑isOdd(Σ(f[x] | x < n - 1));↑isOdd(||filter(λx.isOdd(f[x]);upto(n - 1))||))
4. f : ℕn ⟶ ℤ
⊢ uiff(↑isOdd(Σ(f[x] | x < n));↑isOdd(||filter(λx.isOdd(f[x]);upto(n))||))
BY
{ ((RWO "upto_decomp1" 0 THENA Auto)
   THEN (RWO "filter_append_sq" 0 THENA Auto)
   THEN Reduce 0
   THEN (InstLemma `sum_split1` [⌜n⌝;⌜f⌝]⋅ THENA Auto)
   THEN HypSubst' (-1) 0) }

1
1. n : ℤ
2. 0 < n
3. ∀[f:ℕn - 1 ⟶ ℤ]. uiff(↑isOdd(Σ(f[x] | x < n - 1));↑isOdd(||filter(λx.isOdd(f[x]);upto(n - 1))||))
4. f : ℕn ⟶ ℤ
5. Σ(f[x] | x < n) = (Σ(f[x] | x < n - 1) + f[n - 1]) ∈ ℤ
⊢ uiff(↑isOdd(Σ(f[x] | x < n - 1) + f[n - 1]);↑isOdd(||filter(λx.isOdd(f[x]);upto(n - 1))
@ if isOdd(f[n - 1]) then [n - 1] else [] fi ||))

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}[f:\mBbbN{}n  -  1  {}\mrightarrow{}  \mBbbZ{}]
          uiff(\muparrow{}isOdd(\mSigma{}(f[x]  |  x  <  n  -  1));\muparrow{}isOdd(||filter(\mlambda{}x.isOdd(f[x]);upto(n  -  1))||))
4.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}
\mvdash{}  uiff(\muparrow{}isOdd(\mSigma{}(f[x]  |  x  <  n));\muparrow{}isOdd(||filter(\mlambda{}x.isOdd(f[x]);upto(n))||))


By

---

Latex:
((RWO  "upto\_decomp1"  0  THENA  Auto)
  THEN  (RWO  "filter\_append\_sq"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (InstLemma  `sum\_split1`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-1)  0)

---

Home Index