Step
*
of Lemma
HofstadterM_wf
∀n:ℤ. (HofstadterM(n) ∈ if 0 ≤z n then ℕn + 1 else ℕ1 fi )
BY
{ (InstLemma `Hofstadter_wf` [] THEN ParallelLast THEN Auto) }
Latex:
Latex:
\mforall{}n:\mBbbZ{}. (HofstadterM(n) \mmember{} if 0 \mleq{}z n then \mBbbN{}n + 1 else \mBbbN{}1 fi )
By
Latex:
(InstLemma `Hofstadter\_wf` [] THEN ParallelLast THEN Auto)
Home
Index