		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-queries

Check-mbt$-call

Check if a term is a call of mbt$.

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

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

In translated terms, (mbt$ x) is (return-last 'mbe1-raw 't x).

Definitions and Theorems

Function: check-mbt$-call

(defun check-mbt$-call (term)
  (declare (xargs :guard (pseudo-termp term)))
  (let ((__function__ 'check-mbt$-call))
    (declare (ignorable __function__))
    (case-match term
      (('return-last
        ''mbe1-raw
        ''t
        ('if x ''t ''nil))
       (mv t x))
      (& (mv nil nil)))))

Theorem: booleanp-of-check-mbt$-call.yes/no

(defthm booleanp-of-check-mbt$-call.yes/no
  (b* (((mv ?yes/no ?arg)
        (check-mbt$-call term)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-check-mbt$-call.arg

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

Theorem: acl2-count-of-check-mbt$-call.arg

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