		Search-engine friendly clone of the ACL2 documentation.

Aig-symbolic-arithmetic

Sv::aig-ite-bss-fn-aux

Signature
(sv::aig-ite-bss-fn-aux c v1 v0) → vv
Arguments: v1 — Guard (true-listp v1).; v0 — Guard (true-listp v0).
Returns: vv — Type (true-listp vv).

Definitions and Theorems

Function: aig-ite-bss-fn-aux

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

Theorem: true-listp-of-aig-ite-bss-fn-aux

(defthm sv::true-listp-of-aig-ite-bss-fn-aux
  (b* ((vv (sv::aig-ite-bss-fn-aux c v1 v0)))
    (true-listp vv))
  :rule-classes :type-prescription)

Theorem: aig-ite-bss-fn-aux-correct

(defthm sv::aig-ite-bss-fn-aux-correct
  (b* ((vv (sv::aig-ite-bss-fn-aux c v1 v0)))
    (and (equal (sv::aig-list->s vv env)
                (if (acl2::aig-eval c env)
                    (sv::aig-list->s v1 env)
                  (sv::aig-list->s v0 env))))))