---

Step * 1 of Lemma list-eo-before


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)
BY
{ (AutoSplit THEN RWO "list-eo-pred" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  L  :  Top  List@i
2.  i  :  Id@i
3.  e  :  \mBbbZ{}
4.  0  <  e
5.  e  -  1  <  ||L||  {}\mRightarrow{}  (before(e  -  1)  =  upto(e  -  1))
6.  e  <  ||L||@i
\mvdash{}  if  (e  =\msubz{}  0)  then  []  else  before(pred(e))  @  [pred(e)]  fi    =  upto(e)


By

---

Latex:
(AutoSplit  THEN  RWO  "list-eo-pred"  0  THEN  Auto)

---

Home Index