		Search-engine friendly clone of the ACL2 documentation.

Patterns

Subsetp-of-pat-flatten

(subsetp-of-pat-flatten x pat) is an optimized way to ask if x is a subset of (pat-flatten1 pat).

This just avoids flattening the pattern. Don't expect it to be super fast; it's still O(n^2).

Definitions and Theorems

Function: subsetp-of-pat-flatten

(defun subsetp-of-pat-flatten (x pat)
  (declare (xargs :guard t))
  (mbe :logic
       (subsetp-equal x (pat-flatten1 pat))
       :exec
       (if (atom x)
           t
         (and (member-of-pat-flatten (car x) pat)
              (subsetp-of-pat-flatten (cdr x) pat)))))