Amann分析中recursion theorem的证明 (3-3)

• 当 n＝n＋1 时, 由引理 pₙ＝f〈· · ·〉n 有

f(n＋2)＝Vₙ₊₂(pₙ，f(n＋1))

＝Vₙ₊₂(f〈· · ·〉n，f(n＋1))

＝Vₙ₊₂(f〈· · ·〉(n＋1))

desired-f : desired f

desired-f = i , ii

where

i : f 0 ≡ a

i = refl

ii : ∀ n → f (suc n) ≡ V (suc n) (f ⟨⋯⟩ n)

ii zero = refl

ii (suc n) = begin

f (2+ n) ≡⟨⟩

V (2+ n) (p n , f (suc n)) ≡⟨ cong (λ x → V (2+ n) (x , f (suc n))) (eq n) ⟩

V (2+ n) (f ⟨⋯⟩ n , f (suc n)) ≡⟨⟩

V (2+ n) (f ⟨⋯⟩ (suc n)) ∎

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。