---

Step * 1 1 of Lemma HofstadterL_wf


1. n : ℤ
2. ||[<0, 1>]|| = 1 ∈ ℤ
3. i : ℕ1@i
⊢ [<0, 1>][i] = <HofstadterM(0 - i), HofstadterF(0 - i)> ∈ (ℤ × ℤ)
BY
{ (IntSegCases (-1) THEN RepeatFor 2 ((Computation THEN EqCD))) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  ||[ɘ,  1>]||  =  1
3.  i  :  \mBbbN{}1@i
\mvdash{}  [ɘ,  1>][i]  =  <HofstadterM(0  -  i),  HofstadterF(0  -  i)>


By

---

Latex:
(IntSegCases  (-1)  THEN  RepeatFor  2  ((Computation  THEN  EqCD)))

---

Home Index