L:Top List, n:{0...||L||}. (firstn(n;L) @ nth_tl(n;L)) ~ Ls:T List. 0 < ||s|| 
(s ~ (firstn(||s||-1;s) @ [s[(||s||-1)]]))
nil ; a.as' if 0 < 
n [a / firstn(n-1;as')] else nil fi (recursive)
is mentioned by
| Thm* L:Top List, n:{0...||L||}. (firstn(n;L) @ nth_tl(n;L)) ~ L | [append_firstn_lastn_sq] |
| Thm* s:T List. 0 < ||s|| (s ~ (firstn(||s||-1;s) @ [s[(||s||-1)]])) | [list-decomp-last] |
In prior sections: list 1 mb list 1
Try larger context:
Graphs