(int->aabflist x) → v
Function:
(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:
(defthm trivial-theorem-about-int->aabflist (b* nil (b* ((?ignore (int->aabflist x))) t)) :rule-classes nil)
Theorem:
(defthm true-listp-of-int->aabflist.v (b* ((acl2::?v (int->aabflist x))) (true-listp v)) :rule-classes :type-prescription)
Theorem:
(defthm aabf-p-of-int->aabflist (b* ((v (int->aabflist x))) (implies (and) (and (aabflist-p v man)))))
Theorem:
(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:
(defthm aabf-pred-of-int->aabflist (b* ((v (int->aabflist x))) (implies (and) (and (aabflist-pred v man)))))