---

Step * of Lemma lastn-cases

∀[L:Top List]. ∀[n:ℤ].  (lastn(n;L) ~ if ||L|| ≤z n then L if n ≤z 0 then [] else lastn(n;tl(L)) fi )
BY
{ xxx((UnivCD THENA Auto)
      THEN (SplitOnConclITE THENA Auto)
      THEN RW (AddrC [1] (UnfoldC `lastn`)) 0
      THEN RecUnfold `nth_tl` 0
      THEN RepeatFor 2 ((SplitOnConclITE THEN Try (Complete (Auto')))))xxx }

1
.....truecase..... 
1. L : Top List
2. n : ℤ
3. n < ||L||
4. 0 < ||L|| - n
5. n ≤ 0
⊢ nth_tl(||L|| - n - 1;tl(L)) ~ []

2
.....falsecase..... 
1. L : Top List
2. n : ℤ
3. n < ||L||
4. 0 < ||L|| - n
5. 0 < n
⊢ nth_tl(||L|| - n - 1;tl(L)) ~ lastn(n;tl(L))

---

Latex:

---

Latex:
\mforall{}[L:Top  List].  \mforall{}[n:\mBbbZ{}].
    (lastn(n;L)  \msim{}  if  ||L||  \mleq{}z  n  then  L
    if  n  \mleq{}z  0  then  []
    else  lastn(n;tl(L))
    fi  )


By

---

Latex:
xxx((UnivCD  THENA  Auto)
        THEN  (SplitOnConclITE  THENA  Auto)
        THEN  RW  (AddrC  [1]  (UnfoldC  `lastn`))  0
        THEN  RecUnfold  `nth\_tl`  0
        THEN  RepeatFor  2  ((SplitOnConclITE  THEN  Try  (Complete  (Auto')))))xxx

---

Home Index