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