(bfr-sign-abs-not-s x) → (mv s a n)
Function:
(defun bfr-sign-abs-not-s (x) (declare (xargs :guard (true-listp x))) (let ((__function__ 'bfr-sign-abs-not-s)) (declare (ignorable __function__)) (let ((abs (bfr-abs-s x))) (mv (bfr-sign-s x) abs (bfr-lognot-s abs)))))
Theorem:
(defthm true-listp-of-bfr-sign-abs-not-s.a (b* (((mv acl2::?s acl2::?a acl2::?n) (bfr-sign-abs-not-s x))) (true-listp a)) :rule-classes :type-prescription)
Theorem:
(defthm true-listp-of-bfr-sign-abs-not-s.n (b* (((mv acl2::?s acl2::?a acl2::?n) (bfr-sign-abs-not-s x))) (true-listp n)) :rule-classes :type-prescription)
Theorem:
(defthm bfr-sign-abs-not-s-correct (b* (((mv s a n) (bfr-sign-abs-not-s x))) (and (equal (bfr-eval s env) (< (bfr-list->s x env) 0)) (equal (bfr-list->s a env) (abs (bfr-list->s x env))) (equal (bfr-list->s n env) (lognot (abs (bfr-list->s x env)))))))
Theorem:
(defthm bfr-sign-abs-not-s-deps (b* (((mv s a n) (bfr-sign-abs-not-s x))) (implies (and (not (pbfr-list-depends-on varname param x))) (and (not (pbfr-depends-on varname param s)) (not (pbfr-list-depends-on varname param a)) (not (pbfr-list-depends-on varname param n))))))