---

Step * of Lemma list-eo-before

∀L:Top List. ∀i:Id. ∀e:E.  (before(e) ~ upto(e))
BY
{ (RWO "list-eo-E-sq" 0
   THEN Auto
   THEN D -1
   THEN (RW assert_pushdownC (-1) THENA Auto)
   THEN NatInd (-2)
   THEN Auto
   THEN RecUnfold `es-before` 0
   THEN (RWO "list-eo-first" 0 THENA Auto)
   THEN Reduce 0
   THEN Auto) }

1
1. L : Top List@i
2. i : Id@i
3. e : ℤ
4. 0 < e
5. e - 1 < ||L|| ⇒ (before(e - 1) = upto(e - 1) ∈ (ℕe - 1 List))
6. e < ||L||@i
⊢ if (e =z 0) then [] else before(pred(e)) @ [pred(e)] fi  = upto(e) ∈ (ℕe List)

---

Latex:

---

Latex:
\mforall{}L:Top  List.  \mforall{}i:Id.  \mforall{}e:E.    (before(e)  \msim{}  upto(e))


By

---

Latex:
(RWO  "list-eo-E-sq"  0
  THEN  Auto
  THEN  D  -1
  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
  THEN  NatInd  (-2)
  THEN  Auto
  THEN  RecUnfold  `es-before`  0
  THEN  (RWO  "list-eo-first"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index