---

Step * 1 of Lemma Hofstadter_wf

.....assertion..... 
∀n:ℕ. ((0 < n ⇒ (HofstadterF(n) ∈ ℕn + 1)) ∧ (HofstadterM(n) ∈ ℕn + 1))
BY
{ (CompleteInductionOnNat
   THEN Auto
   THEN (Decide ⌜n < 1⌝⋅ THEN Auto)
   THEN Try ((Subst' n ~ 0 0 THENA Complete (Auto)))
   THEN RW (AddrC [2] UnfoldTopAbC) 0
   THEN (Reduce 0 THENA Auto)
   THEN (((InstHyp [⌜n - 1⌝] 2⋅ THENA Complete (Auto)) THEN D -1) ORELSE Auto)) }

1
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
⊢ eval p = n - 1 in
  eval f = HofstadterF(p) in
  eval m = HofstadterM(f) in
    n - m ∈ ℕn + 1

2
1. n : ℕ
2. ∀n:ℕn. ((0 < n ⇒ (HofstadterF(n) ∈ ℕn + 1)) ∧ (HofstadterM(n) ∈ ℕn + 1))
3. 0 < n ⇒ (HofstadterF(n) ∈ ℕn + 1)
4. ¬n < 1
5. 0 < n - 1 ⇒ (HofstadterF(n - 1) ∈ ℕ(n - 1) + 1)
6. HofstadterM(n - 1) ∈ ℕ(n - 1) + 1
⊢ eval p = n - 1 in
  eval m = HofstadterM(p) in
  eval f = HofstadterF(m) in
    n - f ∈ ℕn + 1

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}n:\mBbbN{}.  ((0  <  n  {}\mRightarrow{}  (HofstadterF(n)  \mmember{}  \mBbbN{}n  +  1))  \mwedge{}  (HofstadterM(n)  \mmember{}  \mBbbN{}n  +  1))


By

---

Latex:
(CompleteInductionOnNat
  THEN  Auto
  THEN  (Decide  \mkleeneopen{}n  <  1\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  Try  ((Subst'  n  \msim{}  0  0  THENA  Complete  (Auto)))
  THEN  RW  (AddrC  [2]  UnfoldTopAbC)  0
  THEN  (Reduce  0  THENA  Auto)
  THEN  (((InstHyp  [\mkleeneopen{}n  -  1\mkleeneclose{}]  2\mcdot{}  THENA  Complete  (Auto))  THEN  D  -1)  ORELSE  Auto))

---

Home Index