s:T List. 0 < ||s|| 
(s ~ (firstn(||s||-1;s) @ [s[(||s||-1)]]))i,j:
, k:(j-i). upto(i;j)[k] = i+kL:T List, P:(T
). (
x
L.P(x)) 
(i:||L||. P(L[i]))L:T List, P:(T). (xL.P(x)) (i:||L||. P(L[i]))is mentioned by
| Thm* s:T List. 0 < ||s|| (s ~ (firstn(||s||-1;s) @ [s[(||s||-1)]])) | [list-decomp-last] |
| Thm* i,j:, k:(j-i). upto(i;j)[k] = i+k | [select_upto] |
| Thm* L:T List, P:(T). (xL.P(x)) (i:||L||. P(L[i])) | [assert_l_bexists] |
| Thm* L:T List, P:(T). (xL.P(x)) (i:||L||. P(L[i])) | [assert_l_ball] |
In prior sections: list 1 mb basic mb list 1 mb list 2
Try larger context:
Graphs