		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Bfr-logapp-russ

Signature
(bfr-logapp-russ n x y) → app
Arguments: n — Guard (true-listp n).; x — Guard (true-listp x).; y — Guard (true-listp y).
Returns: app — Type (true-listp app).

Definitions and Theorems

Function: bfr-logapp-russ

(defun bfr-logapp-russ (n x y)
  (declare (xargs :guard (and (true-listp n)
                              (true-listp x)
                              (true-listp y))))
  (let ((__function__ 'bfr-logapp-russ))
    (declare (ignorable __function__))
    (if (atom n)
        (llist-fix y)
      (if (b* (((mv x1 & xend) (first/rest/end x))
               ((mv y1 & yend) (first/rest/end y)))
            (and xend yend (equal x1 y1)))
          (llist-fix x)
        (bfr-ite-bss
             (car n)
             (b* ((w (ash 1 (len (cdr n)))))
               (bfr-logapp-nus w (s-take w x)
                               (bfr-logapp-russ (cdr n)
                                                (bfr-logtail-ns w x)
                                                y)))
             (bfr-logapp-russ (cdr n) x y))))))

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

(defthm true-listp-of-bfr-logapp-russ
  (b* ((app (bfr-logapp-russ n x y)))
    (true-listp app))
  :rule-classes :type-prescription)

Theorem: bfr-logapp-russ-correct

(defthm bfr-logapp-russ-correct
  (b* ((app (bfr-logapp-russ n x y)))
    (and (equal (bfr-list->s app env)
                (logapp (bfr-list->u (acl2::rev n) env)
                        (bfr-list->s x env)
                        (bfr-list->s y env))))))

Theorem: bfr-logapp-russ-deps

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