---

Step * 1 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. 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))]
BY
{ ((RW (AddrC [1;2] (LemmaC `upto_decomp2`)) 0 THENA Auto) THEN Reduce 0 THEN EqCD) }

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
⊢ if 0 <z ||v|| + 1 then u else u fi  ~ u

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


By

---

Latex:
((RW  (AddrC  [1;2]  (LemmaC  `upto\_decomp2`))  0  THENA  Auto)  THEN  Reduce  0  THEN  EqCD)

---

Home Index