---

Step * 1 1 1 1 1 of Lemma list-eo-info-before


1. u : Top
2. v : Top List
3. ∀e:ℕ. (e < ||v|| ⇒ (map(λe.if e <z ||v|| then v[e] else hd(v) fi ;upto(e)) ~ firstn(e;v)))
4. e : ℕ@i
5. e < ||[u / v]||@i
6. 0 < e
⊢ e - 1 < ||v||
BY
{ Auto' }

---

Latex:

---

Latex:

1.  u  :  Top
2.  v  :  Top  List
3.  \mforall{}e:\mBbbN{}.  (e  <  ||v||  {}\mRightarrow{}  (map(\mlambda{}e.if  e  <z  ||v||  then  v[e]  else  hd(v)  fi  ;upto(e))  \msim{}  firstn(e;v)))
4.  e  :  \mBbbN{}@i
5.  e  <  ||[u  /  v]||@i
6.  0  <  e
\mvdash{}  e  -  1  <  ||v||


By

---

Latex:
Auto'

---

Home Index