---

Step * 1 1 1 2 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. ¬0 < e
6. e < ||[u / v]||@i
⊢ map(λe.if e <z ||v|| + 1 then [u / v][e] else u fi ;upto(e)) ~ []
BY
{ (Subst' e ~ 0 0 THEN Reduce 0 THEN 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.  \mneg{}0  <  e
6.  e  <  ||[u  /  v]||@i
\mvdash{}  map(\mlambda{}e.if  e  <z  ||v||  +  1  then  [u  /  v][e]  else  u  fi  ;upto(e))  \msim{}  []


By

---

Latex:
(Subst'  e  \msim{}  0  0  THEN  Reduce  0  THEN  Auto)

---

Home Index