Step
*
of Lemma
genfact-base-linear
∀[n:ℤ]. ∀[f:ℕ+ ⟶ ℤ]. ∀[b:ℤ]. (genfact(n;b;m.f[m]) = (b * genfact(n;1;m.f[m])) ∈ ℤ)
BY
{ (Assert ∀[n:ℕ]. ∀[f:ℕ+ ⟶ ℤ]. ∀[b:ℤ]. (genfact(n;b;m.f[m]) = (b * genfact(n;1;m.f[m])) ∈ ℤ) BY
(InductionOnNat
THEN Auto
THEN (Unfold `genfact` 0 THEN AutoSplit)
THEN RepeatFor 3 ((CallByValueReduce 0 THENA Auto))
THEN RWO "-3" 0
THEN Auto)) }
1
1. ∀[n:ℕ]. ∀[f:ℕ+ ⟶ ℤ]. ∀[b:ℤ]. (genfact(n;b;m.f[m]) = (b * genfact(n;1;m.f[m])) ∈ ℤ)
⊢ ∀[n:ℤ]. ∀[f:ℕ+ ⟶ ℤ]. ∀[b:ℤ]. (genfact(n;b;m.f[m]) = (b * genfact(n;1;m.f[m])) ∈ ℤ)
Latex:
Latex:
\mforall{}[n:\mBbbZ{}]. \mforall{}[f:\mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbZ{}]. \mforall{}[b:\mBbbZ{}]. (genfact(n;b;m.f[m]) = (b * genfact(n;1;m.f[m])))
By
Latex:
(Assert \mforall{}[n:\mBbbN{}]. \mforall{}[f:\mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbZ{}]. \mforall{}[b:\mBbbZ{}]. (genfact(n;b;m.f[m]) = (b * genfact(n;1;m.f[m]))) BY
(InductionOnNat
THEN Auto
THEN (Unfold `genfact` 0 THEN AutoSplit)
THEN RepeatFor 3 ((CallByValueReduce 0 THENA Auto))
THEN RWO "-3" 0
THEN Auto))
Home
Index