		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-ite-bss-fn-aux

Signature
(aabf-ite-bss-fn-aux c v1 v0 man) → (mv vv new-man)
Arguments: v1 — Guard (true-listp v1).; v0 — Guard (true-listp v0).

Definitions and Theorems

Function: aabf-ite-bss-fn-aux

(defun aabf-ite-bss-fn-aux (c v1 v0 man)
  (declare (xargs :guard (and (true-listp v1) (true-listp v0))))
  (declare (xargs :guard (and (aabf-p c man)
                              (aabflist-p v1 man)
                              (aabflist-p v0 man))))
  (let ((__function__ 'aabf-ite-bss-fn-aux))
    (declare (ignorable __function__))
    (b* (((mv head1 tail1 end1)
          (aabf-first/rest/end v1))
         ((mv head0 tail0 end0)
          (aabf-first/rest/end v0))
         ((when (and end1 end0))
          (b* (((mv ite man)
                (aabf-ite c head1 head0 man)))
            (mv (list ite) man)))
         ((mv rst man)
          (aabf-ite-bss-fn-aux c tail1 tail0 man))
         ((mv head man)
          (aabf-ite c head1 head0 man)))
      (mv (aabf-scons head rst) man))))

Theorem: trivial-theorem-about-aabf-ite-bss-fn-aux

(defthm trivial-theorem-about-aabf-ite-bss-fn-aux
  (b* nil
    (b* ((?ignore (aabf-ite-bss-fn-aux c v1 v0 man)))
      t))
  :rule-classes nil)

Theorem: true-listp-of-aabf-ite-bss-fn-aux.vv

(defthm true-listp-of-aabf-ite-bss-fn-aux.vv
  (b* (((mv ?vv ?new-man)
        (aabf-ite-bss-fn-aux c v1 v0 man)))
    (true-listp vv))
  :rule-classes :type-prescription)

Theorem: aabf-extension-p-of-aabf-ite-bss-fn-aux

(defthm aabf-extension-p-of-aabf-ite-bss-fn-aux
  (b* (((mv ?vv ?new-man)
        (aabf-ite-bss-fn-aux c v1 v0 man)))
    (aabf-extension-p new-man man)))

Theorem: aabf-p-of-aabf-ite-bss-fn-aux

(defthm aabf-p-of-aabf-ite-bss-fn-aux
  (b* (((mv vv new-man)
        (aabf-ite-bss-fn-aux c v1 v0 man)))
    (implies (and (aabf-p c man)
                  (aabflist-p v1 man)
                  (aabflist-p v0 man))
             (and (aabflist-p vv new-man)))))

Theorem: aabf-eval-of-aabf-ite-bss-fn-aux

(defthm aabf-eval-of-aabf-ite-bss-fn-aux
  (b* (((mv vv new-man)
        (aabf-ite-bss-fn-aux c v1 v0 man)))
    (implies
         (and (aabf-p c man)
              (aabflist-p v1 man)
              (aabflist-p v0 man))
         (and (equal (bools->int (aabflist-eval vv env new-man))
                     (if (aabf-eval c env man)
                         (bools->int (aabflist-eval v1 env man))
                       (bools->int (aabflist-eval v0 env man))))))))

Theorem: aabf-pred-of-aabf-ite-bss-fn-aux

(defthm aabf-pred-of-aabf-ite-bss-fn-aux
  (b* (((mv vv new-man)
        (aabf-ite-bss-fn-aux c v1 v0 man)))
    (implies (and (aabf-p c man)
                  (aabflist-p v1 man)
                  (aabflist-p v0 man)
                  (aabf-pred c man)
                  (aabflist-pred v1 man)
                  (aabflist-pred v0 man))
             (and (aabflist-pred vv new-man)))))