---

Step * of Lemma add-one-mod-2

∀[x:ℤ]. (((x + 1) mod 2) = (1 - x mod 2) ∈ ℤ)
BY
{ (Auto
   THEN ((InstLemma `mod_bounds` [⌜x⌝; ⌜2⌝])⋅ THENA Auto)
   THEN ((InstLemma `mod_bounds` [⌜x + 1⌝; ⌜2⌝])⋅ THENA Auto)
   THEN ((InstLemma `modulus-equal` [⌜x + 1⌝; ⌜x⌝; ⌜2⌝])⋅ THENA Auto)
   THEN RepeatFor 3 ((MoveToConcl (-1)))
   THEN (GenConclAtAddr [1; 1; 2])
   THEN (Thin (-1))
   THEN (GenConclAtAddr [2; 1; 1; 2])
   THEN RW IntNormC 0
   THEN Auto) }

1
1. x : ℤ
2. v : ℕ
3. v1 : ℕ
4. ((x + 1) mod 2) = v1 ∈ ℕ
5. 0 ≤ v
6. v < 2
7. 0 ≤ v1
8. v1 < 2
9. (v1 = v ∈ ℤ) ⇒ (2 | 1)
10. (v1 = v ∈ ℤ) ⇐ 2 | 1
⊢ v1 = (1 + ((-1) * v)) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  (((x  +  1)  mod  2)  =  (1  -  x  mod  2))


By

---

Latex:
(Auto
  THEN  ((InstLemma  `mod\_bounds`  [\mkleeneopen{}x\mkleeneclose{};  \mkleeneopen{}2\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `mod\_bounds`  [\mkleeneopen{}x  +  1\mkleeneclose{};  \mkleeneopen{}2\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `modulus-equal`  [\mkleeneopen{}x  +  1\mkleeneclose{};  \mkleeneopen{}x\mkleeneclose{};  \mkleeneopen{}2\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  RepeatFor  3  ((MoveToConcl  (-1)))
  THEN  (GenConclAtAddr  [1;  1;  2])
  THEN  (Thin  (-1))
  THEN  (GenConclAtAddr  [2;  1;  1;  2])
  THEN  RW  IntNormC  0
  THEN  Auto)

---

Home Index