---

Step * 1 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 ⟶ ℤ
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 ||))
BY
{ ((D 3 With ⌜f⌝  THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜Σ(f[x] | x < n - 1)⌝⋅ THENA Auto)
   THEN (GenConclTerm ⌜f[n - 1]⌝⋅ THENA Auto)
   THEN (RWO  "length-append" 0 THENA Auto)
   THEN (GenConclTerm ⌜||filter(λx.isOdd(f[x]);upto(n - 1))||⌝⋅ THENA Auto)
   THEN (RWO "isOdd-add" 0 THENA Auto)
   THEN (BoolCase ⌜same-parity(v;v1)⌝⋅ THENA Auto)
   THEN ((FLemma `same-parity-implies-even-odd` [-1] ORELSE FLemma `not-same-parity-implies-even-odd` [-4]) THENA Auto)
   THEN D -1
   THEN Auto) }

1
1. n : ℤ
2. 0 < n
3. f : ℕn ⟶ ℤ
4. Σ(f[x] | x < n) = (Σ(f[x] | x < n - 1) + f[n - 1]) ∈ ℤ
5. v : ℤ
6. Σ(f[x] | x < n - 1) = v ∈ ℤ
7. v1 : ℤ
8. f[n - 1] = v1 ∈ ℤ
9. v2 : ℕ
10. ||filter(λx.isOdd(f[x]);upto(n - 1))|| = v2 ∈ ℕ
11. ↑same-parity(v;v1)
12. ↑isEven(v)
13. ↑isEven(v1)
14. ↑isOdd(v2) supposing ↑isOdd(v)
15. ↑isOdd(v) supposing ↑isOdd(v2)
16. ¬↑same-parity(v2;||if isOdd(v1) then [n - 1] else [] fi ||)
⊢ ¬True

2
1. n : ℤ
2. 0 < n
3. f : ℕn ⟶ ℤ
4. Σ(f[x] | x < n) = (Σ(f[x] | x < n - 1) + f[n - 1]) ∈ ℤ
5. v : ℤ
6. Σ(f[x] | x < n - 1) = v ∈ ℤ
7. v1 : ℤ
8. f[n - 1] = v1 ∈ ℤ
9. v2 : ℕ
10. ||filter(λx.isOdd(f[x]);upto(n - 1))|| = v2 ∈ ℕ
11. ↑same-parity(v;v1)
12. ↑isOdd(v)
13. ↑isOdd(v1)
14. ¬↑same-parity(v2;||if isOdd(v1) then [n - 1] else [] fi ||)
15. ↑isOdd(v2)
16. ↑isOdd(v)
⊢ ¬True

3
1. n : ℤ
2. 0 < n
3. f : ℕn ⟶ ℤ
4. Σ(f[x] | x < n) = (Σ(f[x] | x < n - 1) + f[n - 1]) ∈ ℤ
5. v : ℤ
6. Σ(f[x] | x < n - 1) = v ∈ ℤ
7. v1 : ℤ
8. ¬↑same-parity(v;v1)
9. f[n - 1] = v1 ∈ ℤ
10. v2 : ℕ
11. ||filter(λx.isOdd(f[x]);upto(n - 1))|| = v2 ∈ ℕ
12. ↑isEven(v)
13. ↑isOdd(v1)
14. ↑isOdd(v2) supposing ↑isOdd(v)
15. ↑isOdd(v) supposing ↑isOdd(v2)
16. ¬False
⊢ ¬↑same-parity(v2;||if isOdd(v1) then [n - 1] else [] fi ||)

4
1. n : ℤ
2. 0 < n
3. f : ℕn ⟶ ℤ
4. Σ(f[x] | x < n) = (Σ(f[x] | x < n - 1) + f[n - 1]) ∈ ℤ
5. v : ℤ
6. Σ(f[x] | x < n - 1) = v ∈ ℤ
7. v1 : ℤ
8. ¬↑same-parity(v;v1)
9. f[n - 1] = v1 ∈ ℤ
10. v2 : ℕ
11. ||filter(λx.isOdd(f[x]);upto(n - 1))|| = v2 ∈ ℕ
12. ↑isOdd(v)
13. ↑isEven(v1)
14. ¬False
15. ↑isOdd(v2)
16. ↑isOdd(v)
⊢ ¬↑same-parity(v2;||if isOdd(v1) 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{}
5.  \mSigma{}(f[x]  |  x  <  n)  =  (\mSigma{}(f[x]  |  x  <  n  -  1)  +  f[n  -  1])
\mvdash{}  uiff(\muparrow{}isOdd(\mSigma{}(f[x]  |  x  <  n  -  1)  +  f[n  -  1]);\muparrow{}isOdd(||filter(\mlambda{}x.isOdd(f[x]);upto(n  -  1))
@  if  isOdd(f[n  -  1])  then  [n  -  1]  else  []  fi  ||))


By

---

Latex:
((D  3  With  \mkleeneopen{}f\mkleeneclose{}    THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}\mSigma{}(f[x]  |  x  <  n  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}f[n  -  1]\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (RWO    "length-append"  0  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}||filter(\mlambda{}x.isOdd(f[x]);upto(n  -  1))||\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (RWO  "isOdd-add"  0  THENA  Auto)
  THEN  (BoolCase  \mkleeneopen{}same-parity(v;v1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ((FLemma  `same-parity-implies-even-odd`  [-1]
              ORELSE  FLemma  `not-same-parity-implies-even-odd`  [-4]
              )
              THENA  Auto
              )
  THEN  D  -1
  THEN  Auto)

---

Home Index