m:
, L:T List. m<||L|| 
(nth_tl(m;L) ~ [L[m] / nth_tl(1+m;L)])L:T List. 0<||L|| (L ~ [hd(L) / tl(L)])l:A List. ||l||
1 ||tl(l)|| = ||l||-1 
| Theorem | Name |
| m:, L:T List. m<||L|| (nth_tl(m;L) ~ [L[m] / nth_tl(1+m;L)]) | [nth_tl_decomp] |
| cites the following: | |
| L:T List. 0<||L|| (L ~ [hd(L) / tl(L)]) | [list_decomp] |
| l:A List. ||l||1 ||tl(l)|| = ||l||-1 | [length_tl] |