---

Step * 1 1 1 1 1 1 1 of Lemma special-mod4-decomp-unique


1. y : ℤ
2. m : ℤ
3. k : ℤ
4. b1 : {-2..3-}
5. m = ((4 * (y + 1)) + (-2)) ∈ ℤ
6. (2 = 2 ∈ ℤ) ⇒ (↑isEven(y + 1))
7. b : {-2..3-}
8. m = ((4 * y) + 2) ∈ ℤ
9. (2 = 2 ∈ ℤ) ⇒ (↑isEven(y))
10. 4 | 4
11. 4 = 4 ∈ ℤ
12. b = 2 ∈ ℤ
13. b1 = (-2) ∈ ℤ
14. k = (y + 1) ∈ ℤ
15. (↑isEven(y + 1)) ∧ (↑isEven(y))
⊢ 2 = (-2) ∈ ℤ
BY
{ TACTIC:(D (-1) THEN (RWO "isEven-add" (-2) THENA Auto)) }

1
1. y : ℤ
2. m : ℤ
3. k : ℤ
4. b1 : {-2..3-}
5. m = ((4 * (y + 1)) + (-2)) ∈ ℤ
6. (2 = 2 ∈ ℤ) ⇒ (↑isEven(y + 1))
7. b : {-2..3-}
8. m = ((4 * y) + 2) ∈ ℤ
9. (2 = 2 ∈ ℤ) ⇒ (↑isEven(y))
10. 4 | 4
11. 4 = 4 ∈ ℤ
12. b = 2 ∈ ℤ
13. b1 = (-2) ∈ ℤ
14. k = (y + 1) ∈ ℤ
15. ↑same-parity(y;1)
16. ↑isEven(y)
⊢ 2 = (-2) ∈ ℤ

---

Latex:

---

Latex:

1.  y  :  \mBbbZ{}
2.  m  :  \mBbbZ{}
3.  k  :  \mBbbZ{}
4.  b1  :  \{-2..3\msupminus{}\}
5.  m  =  ((4  *  (y  +  1))  +  (-2))
6.  (2  =  2)  {}\mRightarrow{}  (\muparrow{}isEven(y  +  1))
7.  b  :  \{-2..3\msupminus{}\}
8.  m  =  ((4  *  y)  +  2)
9.  (2  =  2)  {}\mRightarrow{}  (\muparrow{}isEven(y))
10.  4  |  4
11.  4  =  4
12.  b  =  2
13.  b1  =  (-2)
14.  k  =  (y  +  1)
15.  (\muparrow{}isEven(y  +  1))  \mwedge{}  (\muparrow{}isEven(y))
\mvdash{}  2  =  (-2)


By

---

Latex:
TACTIC:(D  (-1)  THEN  (RWO  "isEven-add"  (-2)  THENA  Auto))

---

Home Index