Step
*
2
2
1
1
1
2
2
of Lemma
HofstadterL_wf
1. n : ℤ
2. 1 < n
3. L : (ℤ × ℤ) List
4. ||L|| = ((n - 1) + 1) ∈ ℤ
5. ∀i:ℕ(n - 1) + 1. (L[i] = <HofstadterM(n - 1 - i), HofstadterF(n - 1 - i)> ∈ (ℤ × ℤ))
6. L[0] = <HofstadterM(n - 1 - 0), HofstadterF(n - 1 - 0)> ∈ (ℤ × ℤ)
⊢ eval m' = HofstadterM(n) in
eval f' = n - fst(L[n - 1 - HofstadterF(n - 1)]) in
[<m', f'> / L] ∈ {L:(ℤ × ℤ) List|
(||L|| = (n + 1) ∈ ℤ) ∧ (∀i:ℕn + 1. (L[i] = <HofstadterM(n - i), HofstadterF(n - i)> ∈ (ℤ × ℤ)))}
BY
{ Subst' n - fst(L[n - 1 - HofstadterF(n - 1)]) ~ HofstadterF(n) 0 }
1
.....equality.....
1. n : ℤ
2. 1 < n
3. L : (ℤ × ℤ) List
4. ||L|| = ((n - 1) + 1) ∈ ℤ
5. ∀i:ℕ(n - 1) + 1. (L[i] = <HofstadterM(n - 1 - i), HofstadterF(n - 1 - i)> ∈ (ℤ × ℤ))
6. L[0] = <HofstadterM(n - 1 - 0), HofstadterF(n - 1 - 0)> ∈ (ℤ × ℤ)
⊢ n - fst(L[n - 1 - HofstadterF(n - 1)]) ~ HofstadterF(n)
2
1. n : ℤ
2. 1 < n
3. L : (ℤ × ℤ) List
4. ||L|| = ((n - 1) + 1) ∈ ℤ
5. ∀i:ℕ(n - 1) + 1. (L[i] = <HofstadterM(n - 1 - i), HofstadterF(n - 1 - i)> ∈ (ℤ × ℤ))
6. L[0] = <HofstadterM(n - 1 - 0), HofstadterF(n - 1 - 0)> ∈ (ℤ × ℤ)
⊢ eval m' = HofstadterM(n) in
eval f' = HofstadterF(n) in
[<m', f'> / L] ∈ {L:(ℤ × ℤ) List|
(||L|| = (n + 1) ∈ ℤ) ∧ (∀i:ℕn + 1. (L[i] = <HofstadterM(n - i), HofstadterF(n - i)> ∈ (ℤ × ℤ)))}
Latex:
Latex:
1. n : \mBbbZ{}
2. 1 < n
3. L : (\mBbbZ{} \mtimes{} \mBbbZ{}) List
4. ||L|| = ((n - 1) + 1)
5. \mforall{}i:\mBbbN{}(n - 1) + 1. (L[i] = <HofstadterM(n - 1 - i), HofstadterF(n - 1 - i)>)
6. L[0] = <HofstadterM(n - 1 - 0), HofstadterF(n - 1 - 0)>
\mvdash{} eval m' = HofstadterM(n) in
eval f' = n - fst(L[n - 1 - HofstadterF(n - 1)]) in
[<m', f'> / L] \mmember{} \{L:(\mBbbZ{} \mtimes{} \mBbbZ{}) List|
(||L|| = (n + 1))
\mwedge{} (\mforall{}i:\mBbbN{}n + 1. (L[i] = <HofstadterM(n - i), HofstadterF(n - i)>))\}
By
Latex:
Subst' n - fst(L[n - 1 - HofstadterF(n - 1)]) \msim{} HofstadterF(n) 0
Home
Index