---

Step * 2 1 of Lemma stream-extensionality


1. A : Type
2. x : stream(A)
3. y : stream(A)
4. ∀n:ℕ. (s-nth(n;x) = s-nth(n;y) ∈ A)
5. x1 : stream(A)
6. y1 : stream(A)
7. ∀n:ℕ. (s-nth(n;x1) = s-nth(n;y1) ∈ A)
8. n : ℕ
9. x1 ~ s-hd(x1).s-tl(x1)
10. y1 ~ s-hd(y1).s-tl(y1)
⊢ (s-nth(n + 1;s-hd(x1).s-tl(x1)) = s-nth(n + 1;s-hd(y1).s-tl(y1)) ∈ A) ⇒ (s-nth(n;s-tl(x1)) = s-nth(n;s-tl(y1)) ∈ A)
BY
{ (RW (AddrC [1] (RecUnfoldC `s-nth`)) 0 THEN Unfold `s-cons` 0 THEN Reduce 0 THEN AutoSplit)⋅ }

1
1. A : Type
2. x : stream(A)
3. y : stream(A)
4. ∀n:ℕ. (s-nth(n;x) = s-nth(n;y) ∈ A)
5. x1 : stream(A)
6. y1 : stream(A)
7. ∀n:ℕ. (s-nth(n;x1) = s-nth(n;y1) ∈ A)
8. n : ℕ
9. n + 1 ≠ 0
10. x1 ~ s-hd(x1).s-tl(x1)
11. y1 ~ s-hd(y1).s-tl(y1)
⊢ (eval m = (n + 1) - 1 in s-nth(m;s-tl(x1)) = eval m = (n + 1) - 1 in s-nth(m;s-tl(y1)) ∈ A)
⇒ (s-nth(n;s-tl(x1)) = s-nth(n;s-tl(y1)) ∈ A)

---

Latex:

---

Latex:

1.  A  :  Type
2.  x  :  stream(A)
3.  y  :  stream(A)
4.  \mforall{}n:\mBbbN{}.  (s-nth(n;x)  =  s-nth(n;y))
5.  x1  :  stream(A)
6.  y1  :  stream(A)
7.  \mforall{}n:\mBbbN{}.  (s-nth(n;x1)  =  s-nth(n;y1))
8.  n  :  \mBbbN{}
9.  x1  \msim{}  s-hd(x1).s-tl(x1)
10.  y1  \msim{}  s-hd(y1).s-tl(y1)
\mvdash{}  (s-nth(n  +  1;s-hd(x1).s-tl(x1))  =  s-nth(n  +  1;s-hd(y1).s-tl(y1)))
{}\mRightarrow{}  (s-nth(n;s-tl(x1))  =  s-nth(n;s-tl(y1)))


By

---

Latex:
(RW  (AddrC  [1]  (RecUnfoldC  `s-nth`))  0  THEN  Unfold  `s-cons`  0  THEN  Reduce  0  THEN  AutoSplit)\mcdot{}

---

Home Index