		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svex-is-const-concat

Signature
(svex-is-const-concat x) → is-concat
Arguments: x — Guard (svex-p x).

Definitions and Theorems

Function: svex-is-const-concat

(defun svex-is-const-concat (x)
  (declare (xargs :guard (svex-p x)))
  (let ((__function__ 'svex-is-const-concat))
    (declare (ignorable __function__))
    (svex-case x
               :call (and (eq x.fn 'concat)
                          (eql (len x.args) 3)
                          (let ((arg1 (mbe :logic (nth 0 x.args)
                                           :exec (car x.args))))
                            (svex-case arg1 :quote)))
               :otherwise nil)))

Theorem: svex-is-const-concat-of-svex-fix-x

(defthm svex-is-const-concat-of-svex-fix-x
  (equal (svex-is-const-concat (svex-fix x))
         (svex-is-const-concat x)))

Theorem: svex-is-const-concat-svex-equiv-congruence-on-x

(defthm svex-is-const-concat-svex-equiv-congruence-on-x
  (implies (svex-equiv x x-equiv)
           (equal (svex-is-const-concat x)
                  (svex-is-const-concat x-equiv)))
  :rule-classes :congruence)