---

Step * 1 1 1 1 1 1 of Lemma fibs_wf

.....falsecase..... 
1. f : ℕ ⟶ ℕ ⟶ ℕ
2. (λx,y. (x + y)) = f ∈ (ℕ ⟶ ℕ ⟶ ℕ)
3. n : ℕ
4. fibs : (λ,T. (ℕ × T)) (n - 1) primrec(n - 1;Top;λ,T. (ℕ × T))
5. 1 ≤ n
6. ¬n < 1
⊢ stream-zip(f;fibs;s-tl(fibs)) ∈ primrec(n - 1;Top;λ,T. (ℕ × T))
BY
{ (Thin (-1) THEN Reduce (-2) THEN D -2 THEN RepUR ``s-tl`` 0)⋅ }

1
1. f : ℕ ⟶ ℕ ⟶ ℕ
2. (λx,y. (x + y)) = f ∈ (ℕ ⟶ ℕ ⟶ ℕ)
3. n : ℕ
4. f1 : ℕ
5. f2 : primrec(n - 1;Top;λ,T. (ℕ × T))
6. 1 ≤ n
⊢ stream-zip(f;<f1, f2>;f2) ∈ primrec(n - 1;Top;λ,T. (ℕ × T))

---

Latex:

---

Latex:
.....falsecase..... 
1.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  (\mlambda{}x,y.  (x  +  y))  =  f
3.  n  :  \mBbbN{}
4.  fibs  :  (\mlambda{},T.  (\mBbbN{}  \mtimes{}  T))  (n  -  1)  primrec(n  -  1;Top;\mlambda{},T.  (\mBbbN{}  \mtimes{}  T))
5.  1  \mleq{}  n
6.  \mneg{}n  <  1
\mvdash{}  stream-zip(f;fibs;s-tl(fibs))  \mmember{}  primrec(n  -  1;Top;\mlambda{},T.  (\mBbbN{}  \mtimes{}  T))


By

---

Latex:
(Thin  (-1)  THEN  Reduce  (-2)  THEN  D  -2  THEN  RepUR  ``s-tl``  0)\mcdot{}

---

Home Index