---

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


1. L : Top List@i
2. i : Id@i
3. e : E@i
⊢ firstn(e;L) @ [if e <z ||L|| then L[e] else hd(L) fi ] ~ firstn(e + 1;L)
BY
{ ((RWO "list-eo-E-sq" (-1) THENA Auto) THEN (Assert e < ||L|| BY (D -1 THEN RW assert_pushdownC (-1) THEN Auto))) }

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

---

Latex:

---

Latex:

1.  L  :  Top  List@i
2.  i  :  Id@i
3.  e  :  E@i
\mvdash{}  firstn(e;L)  @  [if  e  <z  ||L||  then  L[e]  else  hd(L)  fi  ]  \msim{}  firstn(e  +  1;L)


By

---

Latex:
((RWO  "list-eo-E-sq"  (-1)  THENA  Auto)
  THEN  (Assert  e  <  ||L||  BY
                          (D  -1  THEN  RW  assert\_pushdownC  (-1)  THEN  Auto))
  )

---

Home Index