Theorems about integers-from-to as a finite set.
The function integers-from-to is defined, and verified, to return a list of integers in increasing order. Because of this order, this list is also a set represented according to the Std/osets library.
Thus, here we introduce some theorems about integers-from-to viewed as a set:
Theorem:
(defthm setp-of-integers-from-to (set::setp (integers-from-to min max)))
Theorem:
(defthm in-of-integers-from-to (iff (set::in x (integers-from-to min max)) (and (integerp x) (<= (ifix min) x) (<= x (ifix max)))))
Theorem:
(defthm integers-from-to-list-in-integers-from-to (implies (and (integerp min1) (integerp max1) (integerp min2) (integerp max2) (<= min1 max1)) (equal (set::list-in (integers-from-to min1 max1) (integers-from-to min2 max2)) (and (<= min2 min1) (<= max1 max2)))))