---

Step * 1 of Lemma primrec-induction-factorial

.....antecedent..... 
∃x:ℤ [((0)! = x ∈ ℤ)]
BY
{ (With ⌜1⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
\mexists{}x:\mBbbZ{}  [((0)!  =  x)]


By

---

Latex:
(With  \mkleeneopen{}1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index