		Search-engine friendly clone of the ACL2 documentation.

Aig-symbolic-arithmetic

Sv::aig-logapp-nus-aux

Signature
(sv::aig-logapp-nus-aux n a b) → a-app-b
Arguments: n — Guard (natp n).; a — Guard (true-listp a).; b — Guard (true-listp b).
Returns: a-app-b — Type (true-listp a-app-b).

Definitions and Theorems

Function: aig-logapp-nus-aux

(defun sv::aig-logapp-nus-aux (n a b)
  (declare (xargs :guard (and (natp n)
                              (true-listp a)
                              (true-listp b))))
  (let ((__function__ 'sv::aig-logapp-nus-aux))
    (declare (ignorable __function__))
    (b* (((when (zp n)) (llist-fix b))
         ((mv first rest) (car/cdr a)))
      (sv::aig-scons first
                     (sv::aig-logapp-nus-aux (1- n)
                                             rest b)))))

Theorem: true-listp-of-aig-logapp-nus-aux

(defthm sv::true-listp-of-aig-logapp-nus-aux
  (b* ((a-app-b (sv::aig-logapp-nus-aux n a b)))
    (true-listp a-app-b))
  :rule-classes :type-prescription)

Theorem: aig-logapp-nus-aux-correct

(defthm sv::aig-logapp-nus-aux-correct
  (b* ((a-app-b (sv::aig-logapp-nus-aux n a b)))
    (and (equal (sv::aig-list->s a-app-b env)
                (logapp (nfix n)
                        (sv::aig-list->u a env)
                        (sv::aig-list->s b env))))))