		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Int->aabflist

Signature
(int->aabflist x) → v
Arguments: x — Guard (integerp x).

Definitions and Theorems

Function: int->aabflist

(defun int->aabflist (x)
  (declare (xargs :guard (integerp x)))
  (declare (xargs :guard (and)))
  (let ((__function__ 'int->aabflist))
    (declare (ignorable __function__))
    (cond ((zip x) (list (aabf-false)))
          ((eql x -1) (list (aabf-true)))
          (t (cons (if (eql (logcar x) 1)
                       (aabf-true)
                     (aabf-false))
                   (int->aabflist (logcdr x)))))))

Theorem: trivial-theorem-about-int->aabflist

(defthm trivial-theorem-about-int->aabflist
  (b* nil
    (b* ((?ignore (int->aabflist x))) t))
  :rule-classes nil)

Theorem: true-listp-of-int->aabflist.v

(defthm true-listp-of-int->aabflist.v
  (b* ((acl2::?v (int->aabflist x)))
    (true-listp v))
  :rule-classes :type-prescription)

Theorem: aabf-p-of-int->aabflist

(defthm aabf-p-of-int->aabflist
  (b* ((v (int->aabflist x)))
    (implies (and)
             (and (aabflist-p v man)))))

Theorem: aabf-eval-of-int->aabflist

(defthm aabf-eval-of-int->aabflist
  (b* ((v (int->aabflist x)))
    (implies (and)
             (and (equal (bools->int (aabflist-eval v env man))
                         (ifix x))))))

Theorem: aabf-pred-of-int->aabflist

(defthm aabf-pred-of-int->aabflist
  (b* ((v (int->aabflist x)))
    (implies (and)
             (and (aabflist-pred v man)))))