		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-queries

Check-and-call

Check if a term is a (translated) call of and.

Signature
(check-and-call term) → (mv yes/no left right)
Arguments: term — Guard (pseudo-termp term).
Returns: yes/no — Type (booleanp yes/no).; left — Type (pseudo-termp left), given the guard.; right — Type (pseudo-termp right), given the guard.

If it is, return its conjuncts. If it is not, all results are nil.

Definitions and Theorems

Function: check-and-call

(defun check-and-call (term)
  (declare (xargs :guard (pseudo-termp term)))
  (let ((__function__ 'check-and-call))
    (declare (ignorable __function__))
    (b* (((mv ifp test then else)
          (check-if-call term))
         ((when (not ifp)) (mv nil nil nil)))
      (if (equal else *nil*)
          (mv t test then)
        (mv nil nil nil)))))

Theorem: booleanp-of-check-and-call.yes/no

(defthm booleanp-of-check-and-call.yes/no
  (b* (((mv ?yes/no ?left ?right)
        (check-and-call term)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-check-and-call.left

(defthm pseudo-termp-of-check-and-call.left
  (implies (and (pseudo-termp term))
           (b* (((mv ?yes/no ?left ?right)
                 (check-and-call term)))
             (pseudo-termp left)))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-check-and-call.right

(defthm pseudo-termp-of-check-and-call.right
  (implies (and (pseudo-termp term))
           (b* (((mv ?yes/no ?left ?right)
                 (check-and-call term)))
             (pseudo-termp right)))
  :rule-classes :rewrite)

Theorem: acl2-count-of-check-and-call.left

(defthm acl2-count-of-check-and-call.left
  (b* (((mv ?yes/no ?left ?right)
        (check-and-call term)))
    (implies yes/no
             (< (acl2-count left)
                (acl2-count term))))
  :rule-classes :linear)

Theorem: acl2-count-of-check-and-call.right

(defthm acl2-count-of-check-and-call.right
  (b* (((mv ?yes/no ?left ?right)
        (check-and-call term)))
    (implies yes/no
             (< (acl2-count right)
                (acl2-count term))))
  :rule-classes :linear)