		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Regex-disjunct2

Signature
(regex-disjunct2 x y) → res
Arguments: x — Guard (regex-p x).; y — Guard (regex-p y).
Returns: res — Type (regex-p res).

Definitions and Theorems

Function: regex-disjunct2

(defun regex-disjunct2 (x y)
  (declare (xargs :guard (and (regex-p x) (regex-p y))))
  (let ((__function__ 'regex-disjunct2))
    (declare (ignorable __function__))
    (regex-case y
                :disjunct (regex-disjunct (cons x y.lst))
                :otherwise (regex-disjunct (list x y)))))

Theorem: regex-p-of-regex-disjunct2

(defthm regex-p-of-regex-disjunct2
  (b* ((res (regex-disjunct2 x y)))
    (regex-p res))
  :rule-classes :rewrite)