---

Step * of Lemma lastn-0

∀[L:Top List]. ∀[n:ℤ].  lastn(n;L) ~ [] supposing n ≤ 0
BY
{ xxx((UnivCD THENA Auto)
      THEN (RWO "lastn-cases" 0 THENA Auto)
      THEN (SplitOnConclITE THENA Auto)
      THEN Try ((SplitOnConclITE THEN Auto')))xxx }

1
.....truecase..... 
1. L : Top List
2. n : ℤ
3. n ≤ 0
4. ||L|| ≤ n
⊢ L ~ []

---

Latex:

---

Latex:
\mforall{}[L:Top  List].  \mforall{}[n:\mBbbZ{}].    lastn(n;L)  \msim{}  []  supposing  n  \mleq{}  0


By

---

Latex:
xxx((UnivCD  THENA  Auto)
        THEN  (RWO  "lastn-cases"  0  THENA  Auto)
        THEN  (SplitOnConclITE  THENA  Auto)
        THEN  Try  ((SplitOnConclITE  THEN  Auto')))xxx

---

Home Index