---

Step * 1 1 1 of Lemma Hofstadter_wf


1. n : ℕ
2. ∀n:ℕn. ((0 < n ⇒ (HofstadterF(n) ∈ ℕn + 1)) ∧ (HofstadterM(n) ∈ ℕn + 1))
3. 0 < n
4. ¬n < 1
5. 0 < n - 1 ⇒ (HofstadterF(n - 1) ∈ ℕ(n - 1) + 1)
6. HofstadterM(n - 1) ∈ ℕ(n - 1) + 1
7. n = 1 ∈ ℤ
⊢ 1 - HofstadterM(HofstadterF(0)) ∈ ℕ2
BY
{ (Subst' HofstadterM(HofstadterF(0)) ~ 0 0 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  \mforall{}n:\mBbbN{}n.  ((0  <  n  {}\mRightarrow{}  (HofstadterF(n)  \mmember{}  \mBbbN{}n  +  1))  \mwedge{}  (HofstadterM(n)  \mmember{}  \mBbbN{}n  +  1))
3.  0  <  n
4.  \mneg{}n  <  1
5.  0  <  n  -  1  {}\mRightarrow{}  (HofstadterF(n  -  1)  \mmember{}  \mBbbN{}(n  -  1)  +  1)
6.  HofstadterM(n  -  1)  \mmember{}  \mBbbN{}(n  -  1)  +  1
7.  n  =  1
\mvdash{}  1  -  HofstadterM(HofstadterF(0))  \mmember{}  \mBbbN{}2


By

---

Latex:
(Subst'  HofstadterM(HofstadterF(0))  \msim{}  0  0  THEN  Auto)

---

Home Index