---

Step * 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|} 
⊢ ((((|m| * |x n|) * (2 * 1) * (n + m)) + ((|n| * |y m|) * (2 * 1) * (n + m)))
  + ((|m| * |m|) * |-r1|)
  + ((|n| * |n|) * |r2|)) ≤ ((|2| * |n| * |m|) * (2 * B) * (n + m))
BY
{ (((Subst' |m| ~ m 0 THENA Auto) THEN (Subst' |n| ~ n 0 THENA Auto))
   THEN (Assert |-r1| ≤ ((2 * n) - 1) BY
               (Subst' |-r1| ~ |r1| 0
                THEN Auto
                THEN DVar `r1'
                THEN Unhide
                THEN Auto
                THEN Subst' |2 * n| ~ 2 * n -2
                THEN Auto))
   THEN (Assert |r2| ≤ ((2 * m) - 1) BY
               (Subst' |-r1| ~ |r1| 0 THEN DVar `r2' THEN Unhide THEN Auto THEN Subst' |2 * m| ~ 2 * m -2 THEN Auto))) }

1
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)
⊢ ((((m * |x n|) * (2 * 1) * (n + m)) + ((n * |y m|) * (2 * 1) * (n + m))) + ((m * m) * |-r1|) + ((n * n) * |r2|)) 
  ≤ ((|2| * n * m) * (2 * B) * (n + m))

---

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|\} 
\mvdash{}  ((((|m|  *  |x  n|)  *  (2  *  1)  *  (n  +  m))  +  ((|n|  *  |y  m|)  *  (2  *  1)  *  (n  +  m)))
    +  ((|m|  *  |m|)  *  |-r1|)
    +  ((|n|  *  |n|)  *  |r2|))  \mleq{}  ((|2|  *  |n|  *  |m|)  *  (2  *  B)  *  (n  +  m))


By

---

Latex:
(((Subst'  |m|  \msim{}  m  0  THENA  Auto)  THEN  (Subst'  |n|  \msim{}  n  0  THENA  Auto))
  THEN  (Assert  |-r1|  \mleq{}  ((2  *  n)  -  1)  BY
                          (Subst'  |-r1|  \msim{}  |r1|  0
                            THEN  Auto
                            THEN  DVar  `r1'
                            THEN  Unhide
                            THEN  Auto
                            THEN  Subst'  |2  *  n|  \msim{}  2  *  n  -2
                            THEN  Auto))
  THEN  (Assert  |r2|  \mleq{}  ((2  *  m)  -  1)  BY
                          (Subst'  |-r1|  \msim{}  |r1|  0
                            THEN  DVar  `r2'
                            THEN  Unhide
                            THEN  Auto
                            THEN  Subst'  |2  *  m|  \msim{}  2  *  m  -2
                            THEN  Auto)))

---

Home Index