---

Step * 1 of Lemma genfact-step


1. ∀[n:ℕ]. ∀[f:ℕ+ ⟶ ℤ]. ∀[b:ℤ].  (genfact(n;b;m.f[m]) = if n <z 1 then b else f[n] * genfact(n - 1;b;m.f[m]) fi  ∈ ℤ)
2. n : ℤ
3. f : ℕ+ ⟶ ℤ
4. b : ℤ
5. ¬(0 ≤ n)
⊢ genfact(n;b;m.f[m]) = if n <z 1 then b else f[n] * genfact(n - 1;b;m.f[m]) fi  ∈ ℤ
BY
{ ((OReduce 0 THEN Auto) THEN Unfold `genfact` 0 THEN AutoSplit) }

---

Latex:

---

Latex:

1.  \mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[b:\mBbbZ{}].
          (genfact(n;b;m.f[m])  =  if  n  <z  1  then  b  else  f[n]  *  genfact(n  -  1;b;m.f[m])  fi  )
2.  n  :  \mBbbZ{}
3.  f  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
4.  b  :  \mBbbZ{}
5.  \mneg{}(0  \mleq{}  n)
\mvdash{}  genfact(n;b;m.f[m])  =  if  n  <z  1  then  b  else  f[n]  *  genfact(n  -  1;b;m.f[m])  fi 


By

---

Latex:
((OReduce  0  THEN  Auto)  THEN  Unfold  `genfact`  0  THEN  AutoSplit)

---

Home Index