---

Step * 1 1 1 1 1 of Lemma genfact-unbounded

.....aux..... 
1. f : ℕ+ ⟶ ℤ
2. ∀m:ℕ+. 1 < f[m]
3. b : ℕ+
4. N : ℤ
5. n : ℕ
6. ∀[m:ℕn]. ∀k:ℕ. ∀x:{x:ℤ| x = genfact(k;b;m.f[m]) ∈ ℤ} .  ∃n:ℕ [(N ≤ genfact(n;b;m.f[m]))] supposing N ≤ (x + m)
7. k : ℕ
8. x : ℤ
9. x = genfact(k;b;m.f[m]) ∈ ℤ
10. N ≤ (x + n)
11. ¬(N ≤ x)
12. k' : ℤ
13. ¬k' < 1
14. k' = (k + 1) ∈ ℤ
15. z : ℤ
16. z = f[k'] ∈ ℤ
17. x' : ℤ
18. x' = (z * x) ∈ ℤ
⊢ x' = (f[k'] * genfact(k' - 1;b;m.f[m])) ∈ ℤ
BY
{ (HypSubst' (-1) 0 THEN EqCD) }

1
.....subterm..... T:t
1:n
1. f : ℕ+ ⟶ ℤ
2. ∀m:ℕ+. 1 < f[m]
3. b : ℕ+
4. N : ℤ
5. n : ℕ
6. ∀[m:ℕn]. ∀k:ℕ. ∀x:{x:ℤ| x = genfact(k;b;m.f[m]) ∈ ℤ} .  ∃n:ℕ [(N ≤ genfact(n;b;m.f[m]))] supposing N ≤ (x + m)
7. k : ℕ
8. x : ℤ
9. x = genfact(k;b;m.f[m]) ∈ ℤ
10. N ≤ (x + n)
11. ¬(N ≤ x)
12. k' : ℤ
13. ¬k' < 1
14. k' = (k + 1) ∈ ℤ
15. z : ℤ
16. z = f[k'] ∈ ℤ
17. x' : ℤ
18. x' = (z * x) ∈ ℤ
⊢ z = f[k'] ∈ ℤ

2
.....subterm..... T:t
2:n
1. f : ℕ+ ⟶ ℤ
2. ∀m:ℕ+. 1 < f[m]
3. b : ℕ+
4. N : ℤ
5. n : ℕ
6. ∀[m:ℕn]. ∀k:ℕ. ∀x:{x:ℤ| x = genfact(k;b;m.f[m]) ∈ ℤ} .  ∃n:ℕ [(N ≤ genfact(n;b;m.f[m]))] supposing N ≤ (x + m)
7. k : ℕ
8. x : ℤ
9. x = genfact(k;b;m.f[m]) ∈ ℤ
10. N ≤ (x + n)
11. ¬(N ≤ x)
12. k' : ℤ
13. ¬k' < 1
14. k' = (k + 1) ∈ ℤ
15. z : ℤ
16. z = f[k'] ∈ ℤ
17. x' : ℤ
18. x' = (z * x) ∈ ℤ
⊢ x = genfact(k' - 1;b;m.f[m]) ∈ ℤ

---

Latex:

---

Latex:
.....aux..... 
1.  f  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
2.  \mforall{}m:\mBbbN{}\msupplus{}.  1  <  f[m]
3.  b  :  \mBbbN{}\msupplus{}
4.  N  :  \mBbbZ{}
5.  n  :  \mBbbN{}
6.  \mforall{}[m:\mBbbN{}n]
          \mforall{}k:\mBbbN{}.  \mforall{}x:\{x:\mBbbZ{}|  x  =  genfact(k;b;m.f[m])\}  .
              \mexists{}n:\mBbbN{}  [(N  \mleq{}  genfact(n;b;m.f[m]))]  supposing  N  \mleq{}  (x  +  m)
7.  k  :  \mBbbN{}
8.  x  :  \mBbbZ{}
9.  x  =  genfact(k;b;m.f[m])
10.  N  \mleq{}  (x  +  n)
11.  \mneg{}(N  \mleq{}  x)
12.  k'  :  \mBbbZ{}
13.  \mneg{}k'  <  1
14.  k'  =  (k  +  1)
15.  z  :  \mBbbZ{}
16.  z  =  f[k']
17.  x'  :  \mBbbZ{}
18.  x'  =  (z  *  x)
\mvdash{}  x'  =  (f[k']  *  genfact(k'  -  1;b;m.f[m]))


By

---

Latex:
(HypSubst'  (-1)  0  THEN  EqCD)

---

Home Index