---

Step * 2 of Lemma mul-initial-seg-step

.....upcase..... 
1. f : ℕ ⟶ ℕ
2. m : ℤ
3. 0 < m
4. (mul-initial-seg(f) m) = ((mul-initial-seg(f) (m - 1)) * (f (m - 1))) ∈ ℤ
⊢ (mul-initial-seg(f) (m + 1)) = ((mul-initial-seg(f) ((m + 1) - 1)) * (f ((m + 1) - 1))) ∈ ℤ
BY
{ xxx((Subst' (m + 1) - 1 ~ m 0 THENA Auto)
      THEN RepUR ``mul-initial-seg`` 0⋅
      THEN (RW (AddrC [2;3;2] (LemmaC `upto_decomp1`)) 0 THENA Auto)
      THEN (Subst' (m + 1) - 1 ~ m 0 THENA Auto)
      THEN (RWO "map_append_sq" 0⋅ THENA Auto)
      THEN Reduce 0
      THEN (GenConcl ⌜map(f;upto(m)) = L ∈ (ℕ List)⌝⋅ THENA Auto)
      THEN (GenConcl ⌜(f m) = x ∈ ℕ⌝⋅ THENA Auto)
      THEN All Thin)xxx }

1
1. L : ℕ List
2. x : ℕ
⊢ reduce(λx,y. (x * y);1;L @ [x]) = (reduce(λx,y. (x * y);1;L) * x) ∈ ℤ

---

Latex:

---

Latex:
.....upcase..... 
1.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  m  :  \mBbbZ{}
3.  0  <  m
4.  (mul-initial-seg(f)  m)  =  ((mul-initial-seg(f)  (m  -  1))  *  (f  (m  -  1)))
\mvdash{}  (mul-initial-seg(f)  (m  +  1))  =  ((mul-initial-seg(f)  ((m  +  1)  -  1))  *  (f  ((m  +  1)  -  1)))


By

---

Latex:
xxx((Subst'  (m  +  1)  -  1  \msim{}  m  0  THENA  Auto)
        THEN  RepUR  ``mul-initial-seg``  0\mcdot{}
        THEN  (RW  (AddrC  [2;3;2]  (LemmaC  `upto\_decomp1`))  0  THENA  Auto)
        THEN  (Subst'  (m  +  1)  -  1  \msim{}  m  0  THENA  Auto)
        THEN  (RWO  "map\_append\_sq"  0\mcdot{}  THENA  Auto)
        THEN  Reduce  0
        THEN  (GenConcl  \mkleeneopen{}map(f;upto(m))  =  L\mkleeneclose{}\mcdot{}  THENA  Auto)
        THEN  (GenConcl  \mkleeneopen{}(f  m)  =  x\mkleeneclose{}\mcdot{}  THENA  Auto)
        THEN  All  Thin)xxx

---

Home Index