---

Step * 2 of Lemma tl-lastn


1. u : Top
2. v : Top List
3. ∀[n:ℤ]. (tl(lastn(n;v)) ~ if n <z ||v|| then lastn(n - 1;v) else lastn(n;tl(v)) fi )
4. n : ℤ
⊢ tl(lastn(n;[u / v])) ~ if n <z ||[u / v]|| then lastn(n - 1;[u / v]) else lastn(n;tl([u / v])) fi 
BY
{ ((Unfold `lastn` 0 THEN RecUnfold `nth_tl` 0 THEN Reduce 0)
   THEN RepeatFor 2 ((SplitOnConclITE THENA Auto))
   THEN Try (Complete (Auto'))
   THEN (SplitOnConclITE THENA Auto)
   THEN Try (Complete (Auto'))) }

1
.....falsecase..... 
1. u : Top
2. v : Top List
3. ∀[n:ℤ]. (tl(lastn(n;v)) ~ if n <z ||v|| then lastn(n - 1;v) else lastn(n;tl(v)) fi )
4. n : ℤ
5. 0 < (||v|| + 1) - n
6. n < ||v|| + 1
7. 0 < (||v|| + 1) - n - 1
⊢ tl(nth_tl((||v|| + 1) - n - 1;v)) ~ nth_tl((||v|| + 1) - n - 1 - 1;v)

---

Latex:

---

Latex:

1.  u  :  Top
2.  v  :  Top  List
3.  \mforall{}[n:\mBbbZ{}].  (tl(lastn(n;v))  \msim{}  if  n  <z  ||v||  then  lastn(n  -  1;v)  else  lastn(n;tl(v))  fi  )
4.  n  :  \mBbbZ{}
\mvdash{}  tl(lastn(n;[u  /  v]))  \msim{}  if  n  <z  ||[u  /  v]||  then  lastn(n  -  1;[u  /  v])  else  lastn(n;tl([u  /  v]))  fi 


By

---

Latex:
((Unfold  `lastn`  0  THEN  RecUnfold  `nth\_tl`  0  THEN  Reduce  0)
  THEN  RepeatFor  2  ((SplitOnConclITE  THENA  Auto))
  THEN  Try  (Complete  (Auto'))
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Try  (Complete  (Auto')))

---

Home Index