		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-syntactically-false-p

Signature
(aabf-syntactically-false-p x man) → false-p
Returns: false-p — Type (booleanp false-p).

Definitions and Theorems

Function: aabf-syntactically-false-p

(defun aabf-syntactically-false-p (x man)
  (declare (xargs :guard (and (aabf-p x man))))
  (let ((__function__ 'aabf-syntactically-false-p))
    (declare (ignorable __function__))
    (aabf-syntactically-equal x (aabf-false))))

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

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

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

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

Theorem: aabf-syntactically-false-p-implies

(defthm aabf-syntactically-false-p-implies
  (b* nil
    (implies (aabf-syntactically-false-p x man)
             (equal (aabf-eval x env man) nil))))

Theorem: aabf-syntactically-false-p-rewrite

(defthm aabf-syntactically-false-p-rewrite
 (b* nil
   (implies (and (acl2::rewriting-negative-literal
                      (cons 'aabf-syntactically-false-p
                            (cons x (cons man 'nil))))
                 (bind-free '((env . env)) (env)))
            (iff (aabf-syntactically-false-p x man)
                 (and (equal (aabf-eval x env man) nil)
                      (hide (aabf-syntactically-false-p x man)))))))