		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-+-ss

Signature
(aabf-+-ss c v1 v2 man) → (mv sum new-man)
Arguments: v1 — Guard (true-listp v1).; v2 — Guard (true-listp v2).

Definitions and Theorems

Function: aabf-+-ss

(defun aabf-+-ss (c v1 v2 man)
  (declare (xargs :guard (and (true-listp v1) (true-listp v2))))
  (declare (xargs :guard (and (aabf-p c man)
                              (aabflist-p v1 man)
                              (aabflist-p v2 man))))
  (let ((__function__ 'aabf-+-ss))
    (declare (ignorable __function__))
    (b* (((mv head1 tail1 end1)
          (aabf-first/rest/end v1))
         ((mv head2 tail2 end2)
          (aabf-first/rest/end v2))
         ((mv axorb man)
          (aabf-xor head1 head2 man))
         ((mv s man) (aabf-xor c axorb man))
         ((when (and end1 end2))
          (b* (((mv last man)
                (aabf-ite axorb (aabf-not c man)
                          head1 man)))
            (mv (aabf-scons s (list last)) man)))
         ((mv c man)
          (aabf-nest (or (and c axorb) (and head1 head2))
                     man))
         ((mv rst man)
          (aabf-+-ss c tail1 tail2 man)))
      (mv (aabf-scons s rst) man))))

Theorem: trivial-theorem-about-aabf-+-ss

(defthm trivial-theorem-about-aabf-+-ss
  (b* nil
    (b* ((?ignore (aabf-+-ss c v1 v2 man)))
      t))
  :rule-classes nil)

Theorem: true-listp-of-aabf-+-ss.sum

(defthm true-listp-of-aabf-+-ss.sum
  (b* (((mv ?sum ?new-man)
        (aabf-+-ss c v1 v2 man)))
    (true-listp sum))
  :rule-classes :type-prescription)

Theorem: aabf-extension-p-of-aabf-+-ss

(defthm aabf-extension-p-of-aabf-+-ss
  (b* (((mv ?sum ?new-man)
        (aabf-+-ss c v1 v2 man)))
    (aabf-extension-p new-man man)))

Theorem: aabf-p-of-aabf-+-ss

(defthm aabf-p-of-aabf-+-ss
  (b* (((mv sum new-man)
        (aabf-+-ss c v1 v2 man)))
    (implies (and (aabf-p c man)
                  (aabflist-p v1 man)
                  (aabflist-p v2 man))
             (and (aabflist-p sum new-man)))))

Theorem: aabf-eval-of-aabf-+-ss

(defthm aabf-eval-of-aabf-+-ss
 (b* (((mv sum new-man)
       (aabf-+-ss c v1 v2 man)))
   (implies
        (and (aabf-p c man)
             (aabflist-p v1 man)
             (aabflist-p v2 man))
        (and (equal (bools->int (aabflist-eval sum env new-man))
                    (+ (bool->bit (aabf-eval c env man))
                       (bools->int (aabflist-eval v1 env man))
                       (bools->int (aabflist-eval v2 env man))))))))

Theorem: aabf-pred-of-aabf-+-ss

(defthm aabf-pred-of-aabf-+-ss
  (b* (((mv sum new-man)
        (aabf-+-ss c v1 v2 man)))
    (implies (and (aabf-p c man)
                  (aabflist-p v1 man)
                  (aabflist-p v2 man)
                  (aabf-pred c man)
                  (aabflist-pred v1 man)
                  (aabflist-pred v2 man))
             (and (aabflist-pred sum new-man)))))