---

Step * of Lemma list-eo-pred

∀L:Top List. ∀i:Id. ∀n:ℕ||L||.  (0 < n ⇒ (pred(n) ~ n - 1))
BY
{ (Intros THEN RecUnfold `es-pred` 0) }

1
1. L : Top List@i
2. i : Id@i
3. n : ℕ||L||@i
4. 0 < n@i
⊢ let p = pred1(n) in
      if es-dom(list-eo(L;i)) p then p
      if es-eq(list-eo(L;i)) p n then n
      else pred(p)
      fi  ~ n - 1

---

Latex:

---

Latex:
\mforall{}L:Top  List.  \mforall{}i:Id.  \mforall{}n:\mBbbN{}||L||.    (0  <  n  {}\mRightarrow{}  (pred(n)  \msim{}  n  -  1))


By

---

Latex:
(Intros  THEN  RecUnfold  `es-pred`  0)

---

Home Index