		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-syntactically-true-p

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

Definitions and Theorems

Function: aabf-syntactically-true-p

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

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

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

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

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

Theorem: aabf-syntactically-true-p-implies

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

Theorem: aabf-syntactically-true-p-rewrite

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