---

Step * 2 1 of Lemma tl-lastn

.....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)
BY
{ ((InstHyp [⌜n⌝] 3⋅ THENA Auto)
   THEN NthHypSq (-1)
   THEN EqCD
   THEN Unfold `lastn` 0
   THEN Try ((SplitOnConclITE THENA Auto))) }

1
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
8. tl(lastn(n;v)) ~ if n <z ||v|| then lastn(n - 1;v) else lastn(n;tl(v)) fi 
⊢ tl(nth_tl((||v|| + 1) - n - 1;v)) ~ tl(nth_tl(||v|| - n;v))

2
.....truecase..... 
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
8. tl(lastn(n;v)) ~ if n <z ||v|| then lastn(n - 1;v) else lastn(n;tl(v)) fi 
9. n < ||v||
⊢ nth_tl((||v|| + 1) - n - 1 - 1;v) ~ nth_tl(||v|| - n - 1;v)

3
.....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
8. tl(lastn(n;v)) ~ if n <z ||v|| then lastn(n - 1;v) else lastn(n;tl(v)) fi 
9. ||v|| ≤ n
⊢ nth_tl((||v|| + 1) - n - 1 - 1;v) ~ nth_tl(||tl(v)|| - n;tl(v))

---

Latex:

---

Latex:
.....falsecase..... 
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{}
5.  0  <  (||v||  +  1)  -  n
6.  n  <  ||v||  +  1
7.  0  <  (||v||  +  1)  -  n  -  1
\mvdash{}  tl(nth\_tl((||v||  +  1)  -  n  -  1;v))  \msim{}  nth\_tl((||v||  +  1)  -  n  -  1  -  1;v)


By

---

Latex:
((InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
  THEN  NthHypSq  (-1)
  THEN  EqCD
  THEN  Unfold  `lastn`  0
  THEN  Try  ((SplitOnConclITE  THENA  Auto)))

---

Home Index