---

Step * 1 2 of Lemma Hofstadter_wf


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
BY
{ (((CallByValueReduce 0 THENA Auto) THEN (InstHyp [⌜HofstadterM(n - 1)⌝] 2⋅ THENA Auto))
   THEN (GenConcl ⌜HofstadterM(n - 1) = m ∈ ℕn⌝⋅ THENA Auto)
   THEN (CallByValueReduce 0 THENA Auto)) }

1
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
7. (0 < HofstadterM(n - 1) ⇒ (HofstadterF(HofstadterM(n - 1)) ∈ ℕHofstadterM(n - 1) + 1))
∧ (HofstadterM(HofstadterM(n - 1)) ∈ ℕHofstadterM(n - 1) + 1)
8. m : ℕn
9. HofstadterM(n - 1) = m ∈ ℕn
⊢ eval f = HofstadterF(m) in
  n - f ∈ ℕn + 1

---

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  {}\mRightarrow{}  (HofstadterF(n)  \mmember{}  \mBbbN{}n  +  1)
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
\mvdash{}  eval  p  =  n  -  1  in
    eval  m  =  HofstadterM(p)  in
    eval  f  =  HofstadterF(m)  in
        n  -  f  \mmember{}  \mBbbN{}n  +  1


By

---

Latex:
(((CallByValueReduce  0  THENA  Auto)  THEN  (InstHyp  [\mkleeneopen{}HofstadterM(n  -  1)\mkleeneclose{}]  2\mcdot{}  THENA  Auto))
  THEN  (GenConcl  \mkleeneopen{}HofstadterM(n  -  1)  =  m\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto))

---

Home Index