		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-signext-nss

Signature
(aabf-signext-nss n a sign) → a-app-b
Arguments: n — Guard (natp n).; a — Guard (true-listp a).

Definitions and Theorems

Function: aabf-signext-nss

(defun aabf-signext-nss (n a sign)
  (declare (xargs :guard (and (natp n) (true-listp a))))
  (declare (xargs :guard (and)))
  (let ((__function__ 'aabf-signext-nss))
    (declare (ignorable __function__))
    (b* (((when (or (zp n)
                    (aabf-syntactically-signext-p a sign)))
          (list sign))
         ((mv first rest &)
          (aabf-first/rest/end a)))
      (aabf-scons first
                  (aabf-signext-nss (1- n) rest sign)))))

Theorem: trivial-theorem-about-aabf-signext-nss

(defthm trivial-theorem-about-aabf-signext-nss
  (b* nil
    (b* ((?ignore (aabf-signext-nss n a sign)))
      t))
  :rule-classes nil)

Theorem: true-listp-of-aabf-signext-nss.a-app-b

(defthm true-listp-of-aabf-signext-nss.a-app-b
  (b* ((?a-app-b (aabf-signext-nss n a sign)))
    (true-listp a-app-b))
  :rule-classes :type-prescription)

Theorem: aabf-p-of-aabf-signext-nss

(defthm aabf-p-of-aabf-signext-nss
  (b* ((a-app-b (aabf-signext-nss n a sign)))
    (implies (and (aabflist-p a man)
                  (aabf-p sign man))
             (and (aabflist-p a-app-b man)))))

Theorem: aabf-eval-of-aabf-signext-nss

(defthm aabf-eval-of-aabf-signext-nss
  (b* ((a-app-b (aabf-signext-nss n a sign)))
    (implies
         (and (aabflist-p a man)
              (aabf-p sign man))
         (and (equal (bools->int (aabflist-eval a-app-b env man))
                     (logapp (nfix n)
                             (bools->int (aabflist-eval a env man))
                             (endint (aabf-eval sign env man))))))))

Theorem: aabf-pred-of-aabf-signext-nss

(defthm aabf-pred-of-aabf-signext-nss
  (b* ((a-app-b (aabf-signext-nss n a sign)))
    (implies (and (aabflist-p a man)
                  (aabf-p sign man)
                  (aabflist-pred a man)
                  (aabf-pred sign man))
             (and (aabflist-pred a-app-b man)))))