Flatten a pattern into a list of atoms (without an accumulator).

`(pat-flatten1 pat)` is just a simpler flattening function that
does the same thing as pat-flatten but without an accumulator. It is
generally convenient to reason about.

**Function: **

(defun pat-flatten1 (pat) (declare (xargs :guard t)) (mbe :logic (if pat (if (atom pat) (list pat) (append (pat-flatten1 (car pat)) (pat-flatten1 (cdr pat)))) nil) :exec (pat-flatten pat nil)))

**Theorem: **

(defthm pat-flatten-is-pat-flatten1 (equal (pat-flatten pat acc) (append (pat-flatten1 pat) acc)))

**Theorem: **

(defthm true-listp-of-pat-flatten1 (true-listp (pat-flatten1 x)) :rule-classes ((:type-prescription) (:rewrite)))

**Theorem: **

(defthm pat-flatten1-when-atom (implies (atom pat) (equal (pat-flatten1 pat) (if pat (list pat) nil))))

**Theorem: **

(defthm pat-flatten1-of-cons (equal (pat-flatten1 (cons x y)) (append (pat-flatten1 x) (pat-flatten1 y))))

**Theorem: **

(defthm pat-flatten1-nonnil (not (member-equal nil (pat-flatten1 x))))