---

Step * 1 1 1 1 1 1 1 of Lemma reg-seq-mul-regular-eventually


1. x : ℕ+ ⟶ ℤ
2. y : ℕ+ ⟶ ℤ
3. B : ℕ+
4. b : ℕ+
5. ∀n,m:{b...}.  ((2 * ((m * |x n|) + (n * |y m|))) ≤ ((n * m) * ((4 * B) - 2)))
6. n : {b...}
7. m : {b...}
8. r1 : {r:ℤ| |r| < |2 * n|} 
9. r2 : {r:ℤ| |r| < |2 * m|} 
10. |-r1| ≤ ((2 * n) - 1)
11. |r2| ≤ ((2 * m) - 1)
12. (((m * m) * |-r1|) + ((n * n) * |r2|)) ≤ (((2 * n * m) * (n + m)) - (n * n) + (m * m))
⊢ ((((m * |x n|) * 2 * (n + m)) + ((n * |y m|) * 2 * (n + m))) + (((2 * n * m) * (n + m)) - (n * n) + (m * m))) ≤ ((2
                                                                                                                   * n
                                                                                                                   * m)
  * (2 * B)
  * (n + m))
BY
{ ((Assert 0 ≤ ((n * n) + (m * m)) BY
          Auto)
   THEN (Assert (2 * ((m * |x n|) + (n * |y m|))) ≤ ((n * m) * ((4 * B) - 2)) BY
               (BHyp 5 THEN Auto))
   THEN Mul ⌜n + m⌝ (-1)⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
2.  y  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  B  :  \mBbbN{}\msupplus{}
4.  b  :  \mBbbN{}\msupplus{}
5.  \mforall{}n,m:\{b...\}.    ((2  *  ((m  *  |x  n|)  +  (n  *  |y  m|)))  \mleq{}  ((n  *  m)  *  ((4  *  B)  -  2)))
6.  n  :  \{b...\}
7.  m  :  \{b...\}
8.  r1  :  \{r:\mBbbZ{}|  |r|  <  |2  *  n|\} 
9.  r2  :  \{r:\mBbbZ{}|  |r|  <  |2  *  m|\} 
10.  |-r1|  \mleq{}  ((2  *  n)  -  1)
11.  |r2|  \mleq{}  ((2  *  m)  -  1)
12.  (((m  *  m)  *  |-r1|)  +  ((n  *  n)  *  |r2|))  \mleq{}  (((2  *  n  *  m)  *  (n  +  m))  -  (n  *  n)  +  (m  *  m))
\mvdash{}  ((((m  *  |x  n|)  *  2  *  (n  +  m))  +  ((n  *  |y  m|)  *  2  *  (n  +  m)))
    +  (((2  *  n  *  m)  *  (n  +  m))  -  (n  *  n)  +  (m  *  m)))  \mleq{}  ((2  *  n  *  m)  *  (2  *  B)  *  (n  +  m))


By

---

Latex:
((Assert  0  \mleq{}  ((n  *  n)  +  (m  *  m))  BY
                Auto)
  THEN  (Assert  (2  *  ((m  *  |x  n|)  +  (n  *  |y  m|)))  \mleq{}  ((n  *  m)  *  ((4  *  B)  -  2))  BY
                          (BHyp  5  THEN  Auto))
  THEN  Mul  \mkleeneopen{}n  +  m\mkleeneclose{}  (-1)\mcdot{}
  THEN  Auto)

---

Home Index