---

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


1. m : ℤ
2. k : ℤ
3. b1 : {-2..3-}
4. m = ((4 * k) + b1) ∈ ℤ
5. (|b1| = 2 ∈ ℤ) ⇒ (↑isEven(k))
6. y : ℤ
7. b : {-2..3-}
8. m = ((4 * y) + b) ∈ ℤ
9. (|b| = 2 ∈ ℤ) ⇒ (↑isEven(y))
10. 4 | (b - b1)
11. (b - b1) = 4 ∈ ℤ
12. (b = 2 ∈ ℤ) ∧ (b1 = (-2) ∈ ℤ) ∧ (k = (y + 1) ∈ ℤ)
⊢ b = b1 ∈ ℤ
BY
{ TACTIC:((SplitAndHyps THEN Eliminate ⌜b⌝⋅ THEN Eliminate ⌜b1⌝⋅)
          THEN All Reduce
          THEN (Assert (↑isEven(k)) ∧ (↑isEven(y)) BY
                      Auto)
          THEN Eliminate ⌜k⌝⋅) }

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. (↑isEven(y + 1)) ∧ (↑isEven(y))
⊢ 2 = (-2) ∈ ℤ

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:((SplitAndHyps  THEN  Eliminate  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THEN  Eliminate  \mkleeneopen{}b1\mkleeneclose{}\mcdot{})
                THEN  All  Reduce
                THEN  (Assert  (\muparrow{}isEven(k))  \mwedge{}  (\muparrow{}isEven(y))  BY
                                        Auto)
                THEN  Eliminate  \mkleeneopen{}k\mkleeneclose{}\mcdot{})

---

Home Index