		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Bfr-logapp-nus

Signature
(bfr-logapp-nus n a b) → a-app-b
Arguments: n — Guard (natp n).; a — Guard (true-listp a).; b — Guard (true-listp b).
Returns: a-app-b — Type (true-listp a-app-b).

Definitions and Theorems

Function: bfr-logapp-nus

(defun bfr-logapp-nus (n a b)
  (declare (xargs :guard (and (natp n)
                              (true-listp a)
                              (true-listp b))))
  (let ((__function__ 'bfr-logapp-nus))
    (declare (ignorable __function__))
    (b* (((when (syntactically-zero-p b))
          (bfr-loghead-nu n a)))
      (bfr-logapp-nus-aux n a b))))

Theorem: true-listp-of-bfr-logapp-nus

(defthm true-listp-of-bfr-logapp-nus
  (b* ((a-app-b (bfr-logapp-nus n a b)))
    (true-listp a-app-b))
  :rule-classes :type-prescription)

Theorem: bfr-logapp-nus-correct

(defthm bfr-logapp-nus-correct
  (b* ((a-app-b (bfr-logapp-nus n a b)))
    (and (equal (bfr-list->s a-app-b env)
                (logapp (nfix n)
                        (bfr-list->u a env)
                        (bfr-list->s b env))))))

Theorem: bfr-logapp-nus-deps

(defthm bfr-logapp-nus-deps
  (b* ((a-app-b (bfr-logapp-nus n a b)))
    (implies
         (and (not (pbfr-list-depends-on varname param a))
              (not (pbfr-list-depends-on varname param b)))
         (and (not (pbfr-list-depends-on varname param a-app-b))))))