predicate - ACL2 Book

other

(in-package "ACL2")

predicatepfunction

(defun predicatep
  (term)
  (and (consp term)
    (member (car term)
      '(< integerp power2p complex-rationalp rationalp bvecp))))

equal-of-preds-rewritetheorem

(defthm equal-of-preds-rewrite
  (implies (and (syntaxp (and (predicatep a) (predicatep b)))
      (case-split (booleanp a))
      (case-split (booleanp b)))
    (equal (equal a b) (and (implies a b) (implies b a)))))