---

Step * 1 1 1 of Lemma select-data-stream

.....equality..... 
1. L : Top List
2. P : Top
3. i : ℕ
4. i < ||L||
⊢ upto(||L||)[i] ~ i
BY
{ ((InstLemma `select_upto` [⌈||L||⌉;⌈i⌉]⋅ THENA Auto) THEN HypSubst' (-1) 0 THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  L  :  Top  List
2.  P  :  Top
3.  i  :  \mBbbN{}
4.  i  <  ||L||
\mvdash{}  upto(||L||)[i]  \msim{}  i


By

---

Latex:
((InstLemma  `select\_upto`  [\mkleeneopen{}||L||\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  HypSubst'  (-1)  0  THEN  Auto)

---

Home Index