---

Step * 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
⊢ map(λe.if e <z ||v|| + 1 then [u / v][e] else u fi ;upto(e)) ~ [u / firstn(e - 1;v)]
BY
{ (RWO "3<" 0 THENA Auto) }

1
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||

2
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
⊢ map(λe.if e <z ||v|| + 1 then [u / v][e] else u fi ;upto(e)) ~ [u / 
                                                                  map(λe.if e <z ||v|| then v[e] else hd(v) fi ;upto(e 
                                                                      - 1))]

---

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{}  map(\mlambda{}e.if  e  <z  ||v||  +  1  then  [u  /  v][e]  else  u  fi  ;upto(e))  \msim{}  [u  /  firstn(e  -  1;v)]


By

---

Latex:
(RWO  "3<"  0  THENA  Auto)

---

Home Index