---

Step * 1 of Lemma nth-nats

.....assertion..... 
1. n : ℕ
⊢ ∀i:ℤ. (s-nth(n;mk-stream(λx.(x + 1);i)) = (n + i) ∈ ℤ)
BY
{ (NatInd (-1)
   THEN Auto
   THEN RecUnfold `s-nth` 0
   THEN RecUnfold `mk-stream` 0
   THEN Reduce 0
   THEN Auto
   THEN OldAutoSplit
   THEN RepeatFor 2 ((CallByValueReduce 0 THEN Auto))) }

---

Latex:

---

Latex:
.....assertion..... 
1.  n  :  \mBbbN{}
\mvdash{}  \mforall{}i:\mBbbZ{}.  (s-nth(n;mk-stream(\mlambda{}x.(x  +  1);i))  =  (n  +  i))


By

---

Latex:
(NatInd  (-1)
  THEN  Auto
  THEN  RecUnfold  `s-nth`  0
  THEN  RecUnfold  `mk-stream`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  OldAutoSplit
  THEN  RepeatFor  2  ((CallByValueReduce  0  THEN  Auto)))

---

Home Index