		Search-engine friendly clone of the ACL2 documentation.

Aig-symbolic-arithmetic

Sv::aig-ite-bss-fn

Signature
(sv::aig-ite-bss-fn 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

(defun sv::aig-ite-bss-fn (c v1 v0)
  (declare (xargs :guard (and (true-listp v1) (true-listp v0))))
  (let ((__function__ 'sv::aig-ite-bss-fn))
    (declare (ignorable __function__))
    (if c (if (eq c t)
              (llist-fix v1)
            (sv::aig-ite-bss-fn-aux c v1 v0))
      (llist-fix v0))))

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

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

Theorem: aig-ite-bss-fn-correct

(defthm sv::aig-ite-bss-fn-correct
  (b* ((vv (sv::aig-ite-bss-fn 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))))))