---

Step * 1 of Lemma data-stream-cons

.....equality..... 
1. L : Top List
2. a : Top
3. P : Top
⊢ upto(||[a / L]||) ~ [0 / map(λi.(i + 1);upto(||L||))]
BY
{ RW (AddrC [1] (LemmaC `upto_decomp2`)) 0 }

1
.....wf..... 
1. L : Top List
2. a : Top
3. P : Top
⊢ ||[a / L]|| ∈ ℕ+

2
1. L : Top List
2. a : Top
3. P : Top
⊢ [0 / map(λi.(i + 1);upto(||[a / L]|| - 1))] ~ [0 / map(λi.(i + 1);upto(||L||))]

---

Latex:

---

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


By

---

Latex:
RW  (AddrC  [1]  (LemmaC  `upto\_decomp2`))  0

---

Home Index