---

Step * 2 1 1 of Lemma data-stream-cons

.....equality..... 
1. L : Top List
2. a : Top
3. P : Top
4. u : ℕ||L||
5. v : ℕ||L|| List
6. map(λx.(snd(P*(firstn(x + 1;[a / L]))([a / L][x + 1])));v) ~ map(λi.(snd(fst(P(a))*(firstn(i;L))(L[i])));v)
⊢ firstn(u + 1;[a / L]) ~ [a / firstn(u;L)]
BY
{ (RW (AddrC [1] RecUnfoldTopAbC) 0 THEN Reduce 0 THEN AutoSplit THEN RepeatFor 2 (EqCD) THEN DVar `u' THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  L  :  Top  List
2.  a  :  Top
3.  P  :  Top
4.  u  :  \mBbbN{}||L||
5.  v  :  \mBbbN{}||L||  List
6.  map(\mlambda{}x.(snd(P*(firstn(x  +  1;[a  /  L]))([a  /  L][x  +  1])));v) 
\msim{}  map(\mlambda{}i.(snd(fst(P(a))*(firstn(i;L))(L[i])));v)
\mvdash{}  firstn(u  +  1;[a  /  L])  \msim{}  [a  /  firstn(u;L)]


By

---

Latex:
(RW  (AddrC  [1]  RecUnfoldTopAbC)  0
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  RepeatFor  2  (EqCD)
  THEN  DVar  `u'
  THEN  Auto)

---

Home Index