(bagp x) → yes/no
This is similar to the definition of setp, but each element of the list is checked to be either equal or smaller than the next.
Since a strictly ordered list is also non-strictly ordered, an oset is an obag.
(defun bagp (x) (declare (xargs :guard t)) (let ((__function__ 'bagp)) (declare (ignorable __function__)) (if (atom x) (null x) (or (null (cdr x)) (and (consp (cdr x)) (or (equal (car x) (cadr x)) (fast-<< (car x) (cadr x))) (bagp (cdr x)))))))
(defthm booleanp-of-bagp (b* ((yes/no (bagp x))) (booleanp yes/no)) :rule-classes :rewrite)
(defthm bagp-when-setp (implies (setp x) (bagp x)) :rule-classes (:rewrite :forward-chaining))