---

Step * 2 1 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. 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)
BY
{ (Subst' (n + 1) - 1 ~ n 0 THENA Auto) }

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 in s-nth(m;s-tl(x1)) = eval m = n 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.  n  +  1  \mneq{}  0
10.  x1  \msim{}  s-hd(x1).s-tl(x1)
11.  y1  \msim{}  s-hd(y1).s-tl(y1)
\mvdash{}  (eval  m  =  (n  +  1)  -  1  in  s-nth(m;s-tl(x1))  =  eval  m  =  (n  +  1)  -  1  in  s-nth(m;s-tl(y1)))
{}\mRightarrow{}  (s-nth(n;s-tl(x1))  =  s-nth(n;s-tl(y1)))


By

---

Latex:
(Subst'  (n  +  1)  -  1  \msim{}  n  0  THENA  Auto)

---

Home Index