---

Step * of Lemma last_l_interval

∀[T:Type]. ∀[l:T List]. ∀[i:ℕ||l||]. ∀[j:ℕi].  (last(l_interval(l;j;i)) = l[i - 1] ∈ T)
BY
{ (Auto
   THEN Unfold `last` 0
   THEN RWO "select_l_interval" 0
   THEN Auto'
   THEN (InstLemma `length_l_interval` [⌜T⌝; ⌜l⌝; ⌜i⌝; ⌜j⌝])⋅
   THEN Auto'
   THEN (HypSubst' (-1) 0)) }

1
1. T : Type
2. l : T List
3. i : ℕ||l||
4. j : ℕi
5. ||l_interval(l;j;i)|| = (i - j) ∈ ℤ
⊢ l[j + (i - j - 1)] = l[i - 1] ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[l:T  List].  \mforall{}[i:\mBbbN{}||l||].  \mforall{}[j:\mBbbN{}i].    (last(l\_interval(l;j;i))  =  l[i  -  1])


By

---

Latex:
(Auto
  THEN  Unfold  `last`  0
  THEN  RWO  "select\_l\_interval"  0
  THEN  Auto'
  THEN  (InstLemma  `length\_l\_interval`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}l\mkleeneclose{};  \mkleeneopen{}i\mkleeneclose{};  \mkleeneopen{}j\mkleeneclose{}])\mcdot{}
  THEN  Auto'
  THEN  (HypSubst'  (-1)  0))

---

Home Index