Step * 1 1 2 1 of Lemma Hofstadter_wf


1. : ℕ
2. ∀n:ℕn. ((0 <  (HofstadterF(n) ∈ ℕ1)) ∧ (HofstadterM(n) ∈ ℕ1))
3. 0 < n
4. ¬n < 1
5. HofstadterM(n 1) ∈ ℕ(n 1) 1
6. ¬(n 1 ∈ ℤ)
7. HofstadterF(n 1) ∈ ℕ(n 1) 1
⊢ eval in
  eval HofstadterF(p) in
  eval HofstadterM(f) in
    m ∈ ℕ1
BY
(InstHyp [⌜HofstadterF(n 1)⌝2⋅ 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.  HofstadterM(n  -  1)  \mmember{}  \mBbbN{}(n  -  1)  +  1
6.  \mneg{}(n  =  1)
7.  HofstadterF(n  -  1)  \mmember{}  \mBbbN{}(n  -  1)  +  1
\mvdash{}  eval  p  =  n  -  1  in
    eval  f  =  HofstadterF(p)  in
    eval  m  =  HofstadterM(f)  in
        n  -  m  \mmember{}  \mBbbN{}n  +  1


By


Latex:
(InstHyp  [\mkleeneopen{}HofstadterF(n  -  1)\mkleeneclose{}]  2\mcdot{}  THEN  Auto)




Home Index