---

Step * 1 of Lemma HofstadterL_wf

.....basecase..... 
1. n : ℤ
⊢ HofstadterL(0) ∈ {L:(ℤ × ℤ) List| 
                    (||L|| = (0 + 1) ∈ ℤ) ∧ (∀i:ℕ0 + 1. (L[i] = <HofstadterM(0 - i), HofstadterF(0 - i)> ∈ (ℤ × ℤ)))} 
BY
{ ((Unfold `HofstadterL` 0 THEN Reduce 0) THEN MemTypeCD THEN Auto) }

1
1. n : ℤ
2. ||[<0, 1>]|| = 1 ∈ ℤ
3. i : ℕ1@i
⊢ [<0, 1>][i] = <HofstadterM(0 - i), HofstadterF(0 - i)> ∈ (ℤ × ℤ)

---

Latex:

---

Latex:
.....basecase..... 
1.  n  :  \mBbbZ{}
\mvdash{}  HofstadterL(0)  \mmember{}  \{L:(\mBbbZ{}  \mtimes{}  \mBbbZ{})  List| 
                                        (||L||  =  (0  +  1))
                                        \mwedge{}  (\mforall{}i:\mBbbN{}0  +  1.  (L[i]  =  <HofstadterM(0  -  i),  HofstadterF(0  -  i)>))\} 


By

---

Latex:
((Unfold  `HofstadterL`  0  THEN  Reduce  0)  THEN  MemTypeCD  THEN  Auto)

---

Home Index