		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svex-svstmt-or

Signature
(svex-svstmt-or a b) → or
Arguments: a — Guard (svex-p a).; b — Guard (svex-p b).
Returns: or — Type (svex-p or).

Definitions and Theorems

Function: svex-svstmt-or

(defun svex-svstmt-or (a b)
  (declare (xargs :guard (and (svex-p a) (svex-p b))))
  (let ((__function__ 'svex-svstmt-or))
    (declare (ignorable __function__))
    (b* ((a (svex-fix a))
         (b (svex-fix b))
         ((when (svex-case a
                           :quote (2vec-p a.val)
                           :otherwise nil))
          (b* ((a (2vec->val (svex-quote->val a))))
            (if (eql a 0) b -1)))
         ((when (svex-case b
                           :quote (2vec-p b.val)
                           :otherwise nil))
          (b* ((b (2vec->val (svex-quote->val b))))
            (if (eql b 0) a -1))))
      (svex-call 'bitor
                 (list (svex-call 'uor (list a))
                       (svex-call 'uor (list b)))))))

Theorem: svex-p-of-svex-svstmt-or

(defthm svex-p-of-svex-svstmt-or
  (b* ((or (svex-svstmt-or a b)))
    (svex-p or))
  :rule-classes :rewrite)

Theorem: svex-svstmt-or-correct

(defthm svex-svstmt-or-correct
  (b* ((common-lisp::?or (svex-svstmt-or a b)))
    (equal (4vec-reduction-or (svex-eval or env))
           (4vec-reduction-or (4vec-bitor (svex-eval a env)
                                          (svex-eval b env))))))

Theorem: vars-of-svex-svstmt-or

(defthm vars-of-svex-svstmt-or
  (b* ((common-lisp::?or (svex-svstmt-or a b)))
    (implies (and (not (member v (svex-vars a)))
                  (not (member v (svex-vars b))))
             (not (member v (svex-vars or))))))

Theorem: svex-svstmt-or-of-svex-fix-a

(defthm svex-svstmt-or-of-svex-fix-a
  (equal (svex-svstmt-or (svex-fix a) b)
         (svex-svstmt-or a b)))

Theorem: svex-svstmt-or-svex-equiv-congruence-on-a

(defthm svex-svstmt-or-svex-equiv-congruence-on-a
  (implies (svex-equiv a a-equiv)
           (equal (svex-svstmt-or a b)
                  (svex-svstmt-or a-equiv b)))
  :rule-classes :congruence)

Theorem: svex-svstmt-or-of-svex-fix-b

(defthm svex-svstmt-or-of-svex-fix-b
  (equal (svex-svstmt-or a (svex-fix b))
         (svex-svstmt-or a b)))

Theorem: svex-svstmt-or-svex-equiv-congruence-on-b

(defthm svex-svstmt-or-svex-equiv-congruence-on-b
  (implies (svex-equiv b b-equiv)
           (equal (svex-svstmt-or a b)
                  (svex-svstmt-or a b-equiv)))
  :rule-classes :congruence)