# Subbag

Check if (every occurrence of) every value in the first obag
is also (an occurrence of) a value in the second obag.

- Signature
(subbag sub sup) → yes/no

- Arguments
`sub` — Guard (bagp sub).
`sup` — Guard (bagp sup).
- Returns
`yes/no` — Type (booleanp yes/no).

This is similar to `subset` for osets.

### Definitions and Theorems

**Function: **subbag

(defun subbag (sub sup)
(declare (xargs :guard (and (bagp sub) (bagp sup))))
(let ((__function__ 'subbag))
(declare (ignorable __function__))
(or (empty sub)
(and (in (head sub) sup)
(subbag (tail sub)
(delete (head sub) sup))))))

**Theorem: **booleanp-of-subbag

(defthm booleanp-of-subbag
(b* ((yes/no (subbag sub sup)))
(booleanp yes/no))
:rule-classes :rewrite)