---

Step * of Lemma doublefact_wf

∀[n:ℤ]. (doublefact(n) ∈ ℕ+)
BY
{ ((Assert ∀n:ℕ. (doublefact(n) ∈ ℕ+) BY
          (CompleteInductionOnNat THEN Unfold `doublefact` 0 THEN Auto))
   THEN ProveWfLemma
   ) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  (doublefact(n)  \mmember{}  \mBbbN{}\msupplus{})


By

---

Latex:
((Assert  \mforall{}n:\mBbbN{}.  (doublefact(n)  \mmember{}  \mBbbN{}\msupplus{})  BY
                (CompleteInductionOnNat  THEN  Unfold  `doublefact`  0  THEN  Auto))
  THEN  ProveWfLemma
  )

---

Home Index