---

Step * 1 1 of Lemma fibs_wf


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)))
BY
{ ((MemTypeCD THENA Auto) THEN MemCD) }

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

2
.....eq aux..... 
1. f : ℕ ⟶ ℕ ⟶ ℕ
2. (λx,y. (x + y)) = f ∈ (ℕ ⟶ ℕ ⟶ ℕ)
3. n : ℕ
⊢ istype(primrec(n;Top;λ,T. (ℕ × T)))

---

Latex:

---

Latex:

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


By

---

Latex:
((MemTypeCD  THENA  Auto)  THEN  MemCD)

---

Home Index