---

Step * of Lemma primrec-induction-factorial

∀n:ℕ. (∃x:ℤ [((n)! = x ∈ ℤ)])
BY
{ xxx(InstLemma `primrec-induction` [⌜λ2n.∃x:ℤ [((n)! = x ∈ ℤ)]⌝]⋅ THEN Auto)xxx }

1
.....antecedent..... 
∃x:ℤ [((0)! = x ∈ ℤ)]

2
1. n : ℕ
2. ∃x:ℤ [((n)! = x ∈ ℤ)]
⊢ ∃x:ℤ [((n + 1)! = x ∈ ℤ)]

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  (\mexists{}x:\mBbbZ{}  [((n)!  =  x)])


By

---

Latex:
xxx(InstLemma  `primrec-induction`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.\mexists{}x:\mBbbZ{}  [((n)!  =  x)]\mkleeneclose{}]\mcdot{}  THEN  Auto)xxx

---

Home Index