Step * 1 2 1 1 1 of Lemma Hofstadter_wf


1. : ℕ
2. ∀n:ℕn. ((0 <  (HofstadterF(n) ∈ ℕ1)) ∧ (HofstadterM(n) ∈ ℕ1))
3. 0 <  (HofstadterF(n) ∈ ℕ1)
4. ¬n < 1
5. 0 <  (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. : ℕn
9. HofstadterM(n 1) m ∈ ℕn
10. 0 < m
11. (0 <  (HofstadterF(m) ∈ ℕ1)) ∧ (HofstadterM(m) ∈ ℕ1)
⊢ eval HofstadterF(m) in
  f ∈ ℕ1
BY
(D -1 THEN (D -2 THENA Auto)) }

1
1. : ℕ
2. ∀n:ℕn. ((0 <  (HofstadterF(n) ∈ ℕ1)) ∧ (HofstadterM(n) ∈ ℕ1))
3. 0 <  (HofstadterF(n) ∈ ℕ1)
4. ¬n < 1
5. 0 <  (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. : ℕn
9. HofstadterM(n 1) m ∈ ℕn
10. 0 < m
11. HofstadterM(m) ∈ ℕ1
12. HofstadterF(m) ∈ ℕ1
⊢ eval HofstadterF(m) in
  f ∈ ℕ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
7.  (0  <  HofstadterM(n  -  1)  {}\mRightarrow{}  (HofstadterF(HofstadterM(n  -  1))  \mmember{}  \mBbbN{}HofstadterM(n  -  1)  +  1))
\mwedge{}  (HofstadterM(HofstadterM(n  -  1))  \mmember{}  \mBbbN{}HofstadterM(n  -  1)  +  1)
8.  m  :  \mBbbN{}n
9.  HofstadterM(n  -  1)  =  m
10.  0  <  m
11.  (0  <  m  {}\mRightarrow{}  (HofstadterF(m)  \mmember{}  \mBbbN{}m  +  1))  \mwedge{}  (HofstadterM(m)  \mmember{}  \mBbbN{}m  +  1)
\mvdash{}  eval  f  =  HofstadterF(m)  in
    n  -  f  \mmember{}  \mBbbN{}n  +  1


By


Latex:
(D  -1  THEN  (D  -2  THENA  Auto))




Home Index