---

Step * 1 of Lemma nth-better-fibs

.....wf..... 
1. n : ℕ
⊢ mk-stream(λp.let a,b = p 
               in eval c = a + b in
                  <b, c>;<1, 1>) ∈ stream(Top)
BY
{ (SubsumeC ⌜stream(ℕ × ℕ)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  n  :  \mBbbN{}
\mvdash{}  mk-stream(\mlambda{}p.let  a,b  =  p 
                              in  eval  c  =  a  +  b  in
                                    <b,  c>ə,  1>)  \mmember{}  stream(Top)


By

---

Latex:
(SubsumeC  \mkleeneopen{}stream(\mBbbN{}  \mtimes{}  \mBbbN{})\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index