---

Step * 2 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. s-hd(x1) = s-hd(y1) ∈ A
9. n : ℕ
⊢ s-nth(n;s-tl(x1)) = s-nth(n;s-tl(y1)) ∈ A
BY
{ (Thin (-2)
   THEN (InstHyp [⌜n + 1⌝] (-2)⋅ THEN Auto)
   THEN MoveToConcl (-1)
   THEN ((InstLemma `stream-decomp` [⌜x1⌝]⋅ THENM HypSubst'(-1) 0) THENA (DoSubsume THEN Auto))
   THEN ((InstLemma `stream-decomp` [⌜y1⌝]⋅ THENM HypSubst'(-1) 0) THENA (DoSubsume THEN Auto))
   THEN Reduce 0) }

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. 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)

---

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.  s-hd(x1)  =  s-hd(y1)
9.  n  :  \mBbbN{}
\mvdash{}  s-nth(n;s-tl(x1))  =  s-nth(n;s-tl(y1))


By

---

Latex:
(Thin  (-2)
  THEN  (InstHyp  [\mkleeneopen{}n  +  1\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)
  THEN  MoveToConcl  (-1)
  THEN  ((InstLemma  `stream-decomp`  [\mkleeneopen{}x1\mkleeneclose{}]\mcdot{}  THENM  HypSubst'(-1)  0)  THENA  (DoSubsume  THEN  Auto))
  THEN  ((InstLemma  `stream-decomp`  [\mkleeneopen{}y1\mkleeneclose{}]\mcdot{}  THENM  HypSubst'(-1)  0)  THENA  (DoSubsume  THEN  Auto))
  THEN  Reduce  0)

---

Home Index