Entry	Value
Package Name	list-replicate-thm
Count	8
Theorems	APPEND_EQ_REPLICATE : !x n l1 l2. APPEND l1 l2 = REPLICATE x n <=> REPLICATE x (LENGTH l1) = l1 /\ REPLICATE x (LENGTH l2) = l2 /\ LENGTH l1 + LENGTH l2 = n LENGTH_REPLICATE : !x n. LENGTH (REPLICATE x n) = n MAP_REPLICATE : !f x n. MAP f (REPLICATE x n) = REPLICATE (f x) n MEM_REPLICATE : !x n y. MEM y (REPLICATE x n) <=> y = x /\ ~(n = 0) NULL_REPLICATE : !x n. NULL (REPLICATE x n) <=> n = 0 REPLICATE_ADD : !x m n. REPLICATE x (m + n) = APPEND (REPLICATE x m) (REPLICATE x n) SET_OF_LIST_REPLICATE : !x n. set_of_list (REPLICATE x n) = (if n = 0 then {} else {x}) nth_replicate : !x n i. i < n ==> nth (REPLICATE x n) i = x

Back to main package page