---

Step * 2 of Lemma data-stream-cons


1. L : Top List
2. a : Top
3. P : Top
⊢ map(λi.(snd(P*(firstn(i;[a / L]))([a / L][i])));[0 / map(λi.(i + 1);upto(||L||))]) 
~ [snd(P(a)) / map(λi.(snd(fst(P(a))*(firstn(i;L))(L[i])));upto(||L||))]
BY
{ (Reduce 0
   THEN EqCD
   THEN Try (((RWO "first0" 0 THENA Auto) THEN Reduce 0 THEN Trivial))
   THEN ((RWO "map-map" 0 THENM RepUR ``compose`` 0) THENA Auto)
   THEN GenConclAtAddr [2;2]
   THEN Thin (-1)
   THEN ListInd (-1)
   THEN Reduce 0
   THEN RepeatFor 3 ((EqCD THEN Try (Trivial)))
   THEN Try (((RWO "select-cons" 0 THENM AutoSplit) THEN Auto))) }

1
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)
⊢ P*(firstn(u + 1;[a / L])) ~ fst(P(a))*(firstn(u;L))

---

Latex:

---

Latex:

1.  L  :  Top  List
2.  a  :  Top
3.  P  :  Top
\mvdash{}  map(\mlambda{}i.(snd(P*(firstn(i;[a  /  L]))([a  /  L][i])));[0  /  map(\mlambda{}i.(i  +  1);upto(||L||))]) 
\msim{}  [snd(P(a))  /  map(\mlambda{}i.(snd(fst(P(a))*(firstn(i;L))(L[i])));upto(||L||))]


By

---

Latex:
(Reduce  0
  THEN  EqCD
  THEN  Try  (((RWO  "first0"  0  THENA  Auto)  THEN  Reduce  0  THEN  Trivial))
  THEN  ((RWO  "map-map"  0  THENM  RepUR  ``compose``  0)  THENA  Auto)
  THEN  GenConclAtAddr  [2;2]
  THEN  Thin  (-1)
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  RepeatFor  3  ((EqCD  THEN  Try  (Trivial)))
  THEN  Try  (((RWO  "select-cons"  0  THENM  AutoSplit)  THEN  Auto)))

---

Home Index