		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-syntactically-signext-p

Signature
(aabf-syntactically-signext-p x b) → result
Arguments: x — Guard (true-listp x).
Returns: result — Type (booleanp result).

Definitions and Theorems

Function: aabf-syntactically-signext-p

(defun aabf-syntactically-signext-p (x b)
  (declare (xargs :guard (true-listp x)))
  (declare (xargs :guard (and)))
  (let ((__function__ 'aabf-syntactically-signext-p))
    (declare (ignorable __function__))
    (b* (((mv head tail end)
          (aabf-first/rest/end x)))
      (and (aabf-syntactically-equal head b)
           (or end
               (aabf-syntactically-signext-p tail b))))))

Theorem: booleanp-of-aabf-syntactically-signext-p

(defthm booleanp-of-aabf-syntactically-signext-p
  (b* ((result (aabf-syntactically-signext-p x b)))
    (booleanp result))
  :rule-classes :rewrite)

Theorem: trivial-theorem-about-aabf-syntactically-signext-p

(defthm trivial-theorem-about-aabf-syntactically-signext-p
  (b* nil
    (b* ((?ignore (aabf-syntactically-signext-p x b)))
      t))
  :rule-classes nil)

Theorem: aabf-syntactically-signext-p-implies

(defthm aabf-syntactically-signext-p-implies
  (b* nil
    (implies (aabf-syntactically-signext-p x b)
             (equal (bools->int (aabflist-eval x env man))
                    (endint (aabf-eval b env man))))))