---

Step * 2 of Lemma fibs_wf


1. f : ⋂n:ℕ. (primrec(n;Top;λ,T. (ℕ × T)) ⟶ primrec(n;Top;λ,T. (ℕ × T)))
2. (λfibs.1.stream-zip(λx,y. (x + y);fibs;s-tl(fibs))) = f ∈ (⋂n:ℕ. (primrec(n;Top;λ,T. (ℕ × T)) ⟶ primrec(n;Top;λ,T. (\000Cℕ × T))))
⊢ fix((λfibs.1.f fibs)) ∈ stream(ℕ)
BY
{ Thin (-1) }

1
1. f : ⋂n:ℕ. (primrec(n;Top;λ,T. (ℕ × T)) ⟶ primrec(n;Top;λ,T. (ℕ × T)))
⊢ fix((λfibs.1.f fibs)) ∈ stream(ℕ)

---

Latex:

---

Latex:

1.  f  :  \mcap{}n:\mBbbN{}.  (primrec(n;Top;\mlambda{},T.  (\mBbbN{}  \mtimes{}  T))  {}\mrightarrow{}  primrec(n;Top;\mlambda{},T.  (\mBbbN{}  \mtimes{}  T)))
2.  (\mlambda{}fibs.1.stream-zip(\mlambda{}x,y.  (x  +  y);fibs;s-tl(fibs)))  =  f
\mvdash{}  fix((\mlambda{}fibs.1.f  fibs))  \mmember{}  stream(\mBbbN{})


By

---

Latex:
Thin  (-1)

---

Home Index