Check if all the positive integers in a given set are greater than or equal to a given positive integer.
Function:
(defun pos-set->=-pos (set x) (declare (xargs :guard (and (pos-setp set) (posp x)))) (let ((__function__ 'pos-set->=-pos)) (declare (ignorable __function__)) (or (set::emptyp set) (and (>= (set::head set) x) (pos-set->=-pos (set::tail set) x)))))
Theorem:
(defthm booleanp-of-pos-set->=-pos (b* ((yes/no (pos-set->=-pos set x))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm pos-set->=-pos-element (implies (and (pos-set->=-pos set x) (set::in elem set)) (>= elem x)))
Theorem:
(defthm pos-set->=-pos-subset (implies (and (pos-set->=-pos set x) (set::subset set1 set)) (pos-set->=-pos set1 x)))
Theorem:
(defthm pos-set->=-pos-when-emptyp (implies (set::emptyp set) (pos-set->=-pos set x)))
Theorem:
(defthm pos-set->=-pos-of-singleton (equal (pos-set->=-pos (set::insert elem nil) x) (>= elem x)))