		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-logapp-russ

Signature
(aabf-logapp-russ n x y man) → (mv app new-man)
Arguments: n — Guard (true-listp n).; x — Guard (true-listp x).; y — Guard (true-listp y).

Definitions and Theorems

Function: aabf-logapp-russ

(defun aabf-logapp-russ (n x y man)
 (declare (xargs :guard (and (true-listp n)
                             (true-listp x)
                             (true-listp y))))
 (declare (xargs :guard (and (aabflist-p n man)
                             (aabflist-p x man)
                             (aabflist-p y man))))
 (let ((__function__ 'aabf-logapp-russ))
  (declare (ignorable __function__))
  (if (atom n)
      (mv (llist-fix y) man)
   (if (b* (((mv x1 & xend) (aabf-first/rest/end x))
            ((mv y1 & yend)
             (aabf-first/rest/end y)))
         (and xend
              yend (aabf-syntactically-equal x1 y1)))
       (mv (llist-fix x) man)
     (b* ((w (ash 1 (len (cdr n))))
          (first-n (car n))
          (rest-n (cdr n))
          ((when (aabf-syntactically-true-p first-n man))
           (aabf-nest
                (aabf-logapp-nss
                     w (aabf-loghead-ns w x)
                     (aabf-logapp-russ rest-n (aabf-logtail-ns w x)
                                       y))
                man))
          ((when (aabf-syntactically-false-p first-n man))
           (aabf-logapp-russ (cdr n) x y man)))
       (aabf-nest
            (aabf-ite-bss-fn
                 first-n
                 (aabf-logapp-nss
                      w (aabf-loghead-ns w x)
                      (aabf-logapp-russ rest-n (aabf-logtail-ns w x)
                                        y))
                 (aabf-logapp-russ (cdr n) x y))
            man))))))

Theorem: trivial-theorem-about-aabf-logapp-russ

(defthm trivial-theorem-about-aabf-logapp-russ
  (b* nil
    (b* ((?ignore (aabf-logapp-russ n x y man)))
      t))
  :rule-classes nil)

Theorem: true-listp-of-aabf-logapp-russ.app

(defthm true-listp-of-aabf-logapp-russ.app
  (b* (((mv ?app ?new-man)
        (aabf-logapp-russ n x y man)))
    (true-listp app))
  :rule-classes :type-prescription)

Theorem: aabf-extension-p-of-aabf-logapp-russ

(defthm aabf-extension-p-of-aabf-logapp-russ
  (b* (((mv ?app ?new-man)
        (aabf-logapp-russ n x y man)))
    (aabf-extension-p new-man man)))

Theorem: aabf-p-of-aabf-logapp-russ

(defthm aabf-p-of-aabf-logapp-russ
  (b* (((mv app new-man)
        (aabf-logapp-russ n x y man)))
    (implies (and (aabflist-p n man)
                  (aabflist-p x man)
                  (aabflist-p y man))
             (and (aabflist-p app new-man)))))

Theorem: aabf-eval-of-aabf-logapp-russ

(defthm aabf-eval-of-aabf-logapp-russ
 (b* (((mv app new-man)
       (aabf-logapp-russ n x y man)))
  (implies
   (and (aabflist-p n man)
        (aabflist-p x man)
        (aabflist-p y man))
   (and (equal (bools->int (aabflist-eval app env new-man))
               (logapp (bools->uint (aabflist-eval (rev n) env man))
                       (bools->int (aabflist-eval x env man))
                       (bools->int (aabflist-eval y env man))))))))

Theorem: aabf-pred-of-aabf-logapp-russ

(defthm aabf-pred-of-aabf-logapp-russ
  (b* (((mv app new-man)
        (aabf-logapp-russ n x y man)))
    (implies (and (aabflist-p n man)
                  (aabflist-p x man)
                  (aabflist-p y man)
                  (aabflist-pred n man)
                  (aabflist-pred x man)
                  (aabflist-pred y man))
             (and (aabflist-pred app new-man)))))