---

Step * 1 of Lemma fibs_wf

.....wf..... 
λfibs.1.stream-zip(λx,y. (x + y);fibs;s-tl(fibs)) ∈ ⋂n:ℕ. (primrec(n;Top;λ,T. (ℕ × T)) ⟶ primrec(n;Top;λ,T. (ℕ × T)))
BY
{ (GenConcl ⌜(λx,y. (x + y)) = f ∈ (ℕ ⟶ ℕ ⟶ ℕ)⌝⋅ THENA Auto') }

1
1. f : ℕ ⟶ ℕ ⟶ ℕ
2. (λx,y. (x + y)) = f ∈ (ℕ ⟶ ℕ ⟶ ℕ)
⊢ λfibs.1.stream-zip(f;fibs;s-tl(fibs)) ∈ ⋂n:ℕ. (primrec(n;Top;λ,T. (ℕ × T)) ⟶ primrec(n;Top;λ,T. (ℕ × T)))

---

Latex:

---

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


By

---

Latex:
(GenConcl  \mkleeneopen{}(\mlambda{}x,y.  (x  +  y))  =  f\mkleeneclose{}\mcdot{}  THENA  Auto')

---

Home Index