---

Step * 1 of Lemma tl-lastn


1. n : ℤ
⊢ tl(lastn(n;[])) ~ if n <z ||[]|| then lastn(n - 1;[]) else lastn(n;tl([])) fi 
BY
{ ((Reduce 0 THEN (RWO "lastn-nil" 0 THENM Reduce 0 THENM SplitOnConclITE)) THEN Auto)⋅ }

---

Latex:

---

Latex:

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


By

---

Latex:
((Reduce  0  THEN  (RWO  "lastn-nil"  0  THENM  Reduce  0  THENM  SplitOnConclITE))  THEN  Auto)\mcdot{}

---

Home Index