---

Step * 2 of Lemma primrec-induction-factorial


1. n : ℕ
2. ∃x:ℤ [((n)! = x ∈ ℤ)]
⊢ ∃x:ℤ [((n + 1)! = x ∈ ℤ)]
BY
{ (D (-1)
   THEN With ⌜eval x' = x in
              eval m = n + 1 in
                m * x'⌝ (D 0)⋅
   THEN Auto
   THEN RepeatFor 2 ((CallByValueReduce 0 THEN Auto))) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  \mexists{}x:\mBbbZ{}  [((n)!  =  x)]
\mvdash{}  \mexists{}x:\mBbbZ{}  [((n  +  1)!  =  x)]


By

---

Latex:
(D  (-1)
  THEN  With  \mkleeneopen{}eval  x'  =  x  in
                        eval  m  =  n  +  1  in
                            m  *  x'\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  RepeatFor  2  ((CallByValueReduce  0  THEN  Auto)))

---

Home Index