Step
*
2
1
2
of Lemma
HofstadterL_wf
1. n : ℤ
2. 0 < n
3. HofstadterL(n - 1) ∈ {L:(ℤ × ℤ) List|
(||L|| = ((n - 1) + 1) ∈ ℤ)
∧ (∀i:ℕ(n - 1) + 1. (L[i] = <HofstadterM(n - 1 - i), HofstadterF(n - 1 - i)> ∈ (ℤ × ℤ)))}
4. n = 1 ∈ ℤ
⊢ [<0, 1>; <0, 1>] ∈ {L:(ℤ × ℤ) List|
(||L|| = (1 + 1) ∈ ℤ) ∧ (∀i:ℕ1 + 1. (L[i] = <HofstadterM(1 - i), HofstadterF(1 - i)> ∈ (ℤ × ℤ)))}
BY
{ ((MemTypeCD THEN Reduce 0 THEN Auto) THEN IntSegCases (-1) THEN Computation THEN EqCD THEN Auto) }
Latex:
Latex:
1. n : \mBbbZ{}
2. 0 < n
3. HofstadterL(n - 1) \mmember{} \{L:(\mBbbZ{} \mtimes{} \mBbbZ{}) List|
(||L|| = ((n - 1) + 1))
\mwedge{} (\mforall{}i:\mBbbN{}(n - 1) + 1
(L[i] = <HofstadterM(n - 1 - i), HofstadterF(n - 1 - i)>))\}
4. n = 1
\mvdash{} [ɘ, 1> ɘ, 1>] \mmember{} \{L:(\mBbbZ{} \mtimes{} \mBbbZ{}) List|
(||L|| = (1 + 1)) \mwedge{} (\mforall{}i:\mBbbN{}1 + 1. (L[i] = <HofstadterM(1 - i), HofstadterF(1 - i)>))\}
By
Latex:
((MemTypeCD THEN Reduce 0 THEN Auto) THEN IntSegCases (-1) THEN Computation THEN EqCD THEN Auto)
Home
Index