---

Step * 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
⊢ map(λe.if e <z ||[u / v]|| then [u / v][e] else hd([u / v]) fi ;upto(e)) ~ firstn(e;[u / v])
BY
{ ((RecUnfold `firstn` 0 THEN Reduce 0) THEN AutoSplit) }

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
⊢ map(λe.if e <z ||v|| + 1 then [u / v][e] else u fi ;upto(e)) ~ [u / firstn(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. ¬0 < e
6. e < ||[u / v]||@i
⊢ map(λe.if e <z ||v|| + 1 then [u / v][e] else u fi ;upto(e)) ~ []

---

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


By

---

Latex:
((RecUnfold  `firstn`  0  THEN  Reduce  0)  THEN  AutoSplit)

---

Home Index