Entry	Value
Package Name	list-take-drop-thm
Count	16
Theorems	drop_add : !m n l. m + n <= LENGTH l ==> drop (m + n) l = drop m (drop n l) drop_append : !l1 l2. drop (LENGTH l1) (APPEND l1 l2) = l2 drop_length : !l. drop (LENGTH l) l = [] drop_replicate : !m n x. m <= n ==> drop m (REPLICATE x n) = REPLICATE x (n - m) length_drop : !n l. n <= LENGTH l ==> LENGTH (drop n l) = LENGTH l - n length_drop_add : !n l. n <= LENGTH l ==> n + LENGTH (drop n l) = LENGTH l length_take : !n l. n <= LENGTH l ==> LENGTH (take n l) = n nth_drop : !n l i. n + i < LENGTH l ==> nth (drop n l) i = nth l (n + i) nth_take : !n l i. n <= LENGTH l /\ i < n ==> nth (take n l) i = nth l i nth_take_drop : !n l i. n <= LENGTH l /\ i < LENGTH l ==> nth l i = (if i < n then nth (take n l) i else nth (drop n l) (i - n)) take_add : !m n l. m + n <= LENGTH l ==> take (m + n) l = APPEND (take m l) (take n (drop m l)) take_append : !l1 l2. take (LENGTH l1) (APPEND l1 l2) = l1 take_drop : !n l. n <= LENGTH l ==> APPEND (take n l) (drop n l) = l take_length : !l. take (LENGTH l) l = l take_one : !h t. take 1 (CONS h t) = [h] take_replicate : !m n x. m <= n ==> take m (REPLICATE x n) = REPLICATE x m

Back to main package page