---

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


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

1
1. l : Base@i
2. u : Base@i
3. v : Base@i
4. j : ℕ
5. exception(u; v) ≤ λlist_ind,L. eval v = L in
                                  if v is a pair then let h,t = v 
                                                      in λx.(list_ind t h) otherwise if v = Ax then λx.x otherwise ⊥^j 
                     ⊥ 
                     l 
                     ⊥
⊢ exception(u; v) ≤ last(l)

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:(RepUR  ``l-last  l-last-default  list\_ind``  -1  THEN  ExceptionCompactness  (-1)  THEN  Thin  (-3))

---

Home Index