---

Step * of Lemma exp-fact-as-genfact

∀[a,x:ℤ]. ∀[n:ℕ].  (a * x^n * (n)! ~ genfact(n;a;m.x * m))
BY
{ ((InductionOnNat THENA Auto)
   THENL [Computation; (RWO "fact_unroll exp_step genfact-step" 0 THEN Auto THEN AutoSplit THEN RWO "-1<" 0 THEN Auto)]
) }

1
1. a : ℤ
2. x : ℤ
3. n : ℤ
⊢ a * 1 ~ a

---

Latex:

---

Latex:
\mforall{}[a,x:\mBbbZ{}].  \mforall{}[n:\mBbbN{}].    (a  *  x\^{}n  *  (n)!  \msim{}  genfact(n;a;m.x  *  m))


By

---

Latex:
((InductionOnNat  THENA  Auto)
  THENL  [Computation
              ;  (RWO  "fact\_unroll  exp\_step  genfact-step"  0
                    THEN  Auto
                    THEN  AutoSplit
                    THEN  RWO  "-1<"  0
                    THEN  Auto)]
)

---

Home Index