Entry	Value
Package Name	list-nth-thm
Count	8
Theorems	all_nth : !p l. ALL p l <=> (!i. i < LENGTH l ==> p (nth l i)) ex_nth : !p l. EX p l <=> (?i. i < LENGTH l /\ p (nth l i)) last_nth : !l. ~NULL l ==> nth l (LENGTH l - 1) = LAST l mem_nth : !l x. MEM x l <=> (?i. i < LENGTH l /\ x = nth l i) nth_append : !l1 l2 k. k < LENGTH l1 + LENGTH l2 ==> nth (APPEND l1 l2) k = (if k < LENGTH l1 then nth l1 k else nth l2 (k - LENGTH l1)) nth_eq : !l1 l2. LENGTH l1 = LENGTH l2 /\ (!i. i < LENGTH l1 ==> nth l1 i = nth l2 i) ==> l1 = l2 nth_map : !f l i. i < LENGTH l ==> nth (MAP f l) i = f (nth l i) set_of_list_nth : !l. set_of_list l = IMAGE (nth l) {i | i < LENGTH l}

Back to main package page