---

Step * 2 1 of Lemma l-last-is-last


1. l : Base
2. u : Base
3. v : Base
4. exception(u; v) ≤ last(l)
⊢ exception(u; v) ≤ l-last(l)
BY
{ TACTIC:(RepUR ``last select`` -1 THEN ExceptionCompactness (-1) THEN Thin (-3)) }

1
1. l : Base
2. u : Base
3. v : Base
4. j : ℕ
5. exception(u; v) ≤ λselect,n,L. let x,y = L in if (n) < (1)  then x  else eval m = n - 1 in select m y^j ⊥ (||l|| - 1)\000C l
⊢ exception(u; v) ≤ l-last(l)

---

Latex:

---

Latex:

1.  l  :  Base
2.  u  :  Base
3.  v  :  Base
4.  exception(u;  v)  \mleq{}  last(l)
\mvdash{}  exception(u;  v)  \mleq{}  l-last(l)


By

---

Latex:
TACTIC:(RepUR  ``last  select``  -1  THEN  ExceptionCompactness  (-1)  THEN  Thin  (-3))

---

Home Index