---

Step * of Lemma nth-nats

No Annotations
∀n:ℕ. (s-nth(n;nats()) ~ n)
BY
{ ((Unfold `nats` 0 THEN Auto)
   THEN Assert ⌜∀i:ℤ. (s-nth(n;mk-stream(λx.(x + 1);i)) = (n + i) ∈ ℤ)⌝⋅
   THEN Try (TACTIC:(RWO "-1" 0 THEN Auto))) }

1
.....assertion..... 
1. n : ℕ
⊢ ∀i:ℤ. (s-nth(n;mk-stream(λx.(x + 1);i)) = (n + i) ∈ ℤ)

---

Latex:

---

Latex:
No  Annotations
\mforall{}n:\mBbbN{}.  (s-nth(n;nats())  \msim{}  n)


By

---

Latex:
((Unfold  `nats`  0  THEN  Auto)
  THEN  Assert  \mkleeneopen{}\mforall{}i:\mBbbZ{}.  (s-nth(n;mk-stream(\mlambda{}x.(x  +  1);i))  =  (n  +  i))\mkleeneclose{}\mcdot{}
  THEN  Try  (TACTIC:(RWO  "-1"  0  THEN  Auto)))

---

Home Index