---

Step * of Lemma tl-lastn

∀[L:Top List]. ∀[n:ℤ].  (tl(lastn(n;L)) ~ if n <z ||L|| then lastn(n - 1;L) else lastn(n;tl(L)) fi )
BY
{ xxx(InductionOnList THEN (D 0 THENA Auto))xxx }

1
1. n : ℤ
⊢ tl(lastn(n;[])) ~ if n <z ||[]|| then lastn(n - 1;[]) else lastn(n;tl([])) fi 

2
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 

---

Latex:

---

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


By

---

Latex:
xxx(InductionOnList  THEN  (D  0  THENA  Auto))xxx

---

Home Index