(aabf-syntactically-neg1-p x) → result
Function:
(defun aabf-syntactically-neg1-p (x) (declare (xargs :guard (true-listp x))) (declare (xargs :guard (and))) (let ((__function__ 'aabf-syntactically-neg1-p)) (declare (ignorable __function__)) (b* (((mv head tail end) (aabf-first/rest/end x))) (and (aabf-syntactically-equal head (aabf-true)) (or end (aabf-syntactically-neg1-p tail))))))
Theorem:
(defthm booleanp-of-aabf-syntactically-neg1-p (b* ((result (aabf-syntactically-neg1-p x))) (booleanp result)) :rule-classes :rewrite)
Theorem:
(defthm trivial-theorem-about-aabf-syntactically-neg1-p (b* nil (b* ((?ignore (aabf-syntactically-neg1-p x))) t)) :rule-classes nil)
Theorem:
(defthm aabf-syntactically-neg1-p-implies (b* nil (implies (aabf-syntactically-neg1-p x) (equal (bools->int (aabflist-eval x env man)) -1))))