---

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


1. L : Top List@i
2. i : Id@i
3. e : E@i
⊢ map(λe.info(e);before(e)) ~ firstn(e;L)
BY
{ ((RWO "list-eo-before" 0 THENA Auto)
   THEN (RWO "list-eo-info" 0 THENA Auto)
   THEN ((RWO "list-eo-E-sq" (-1) THENM D -1) THENA Auto)
   THEN (RW assert_pushdownC (-1) THENA Auto)) }

1
1. L : Top List@i
2. i : Id@i
3. e : ℕ@i
4. e < ||L||
⊢ map(λe.if e <z ||L|| then L[e] else hd(L) fi ;upto(e)) ~ firstn(e;L)

---

Latex:

---

Latex:

1.  L  :  Top  List@i
2.  i  :  Id@i
3.  e  :  E@i
\mvdash{}  map(\mlambda{}e.info(e);before(e))  \msim{}  firstn(e;L)


By

---

Latex:
((RWO  "list-eo-before"  0  THENA  Auto)
  THEN  (RWO  "list-eo-info"  0  THENA  Auto)
  THEN  ((RWO  "list-eo-E-sq"  (-1)  THENM  D  -1)  THENA  Auto)
  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto))

---

Home Index