---

Step * of Lemma has-value-last-list

∀[l:Base]. l ∈ Top List supposing (last(l))↓
BY
{ (Auto
   THEN BLemma `list-if-has-value-length`
   THEN Auto
   THEN Unfold `last` (-1)
   THEN RecUnfold `select` (-1)
   THEN HVimplies2 (-1) [1]⋅
   THEN HasValueD 2
   THEN Auto) }

1
1. l : Base
2. (if (||<fst(l), snd(l)>|| - 1) < (1)  then fst(l)  else eval m = ||<fst(l), snd(l)>|| - 1 - 1 in snd(l)[m])↓
3. l ~ <fst(l), snd(l)>
4. ||<fst(l), snd(l)>|| - 1 ∈ ℤ
5. 1 ∈ ℤ
⊢ (||<fst(l), snd(l)>||)↓

2
1. l : Base
2. (⊥)↓
3. ∀a,b:Base.  (if l is a pair then a otherwise b ~ b)
4. ∀[F:Top]. (let x,y = l in F[x;y] ~ eval x = l in ⊥)
5. (l)↓
⊢ (||l||)↓

---

Latex:

---

Latex:
\mforall{}[l:Base].  l  \mmember{}  Top  List  supposing  (last(l))\mdownarrow{}


By

---

Latex:
(Auto
  THEN  BLemma  `list-if-has-value-length`
  THEN  Auto
  THEN  Unfold  `last`  (-1)
  THEN  RecUnfold  `select`  (-1)
  THEN  HVimplies2  (-1)  [1]\mcdot{}
  THEN  HasValueD  2
  THEN  Auto)

---

Home Index