		Search-engine friendly clone of the ACL2 documentation.

Aig-symbolic-arithmetic

Sv::aig-loghead-nu

Signature
(sv::aig-loghead-nu n a) → head
Arguments: n — Guard (natp n).; a — Guard (true-listp a).
Returns: head — Type (true-listp head).

Definitions and Theorems

Function: aig-loghead-nu

(defun sv::aig-loghead-nu (n a)
  (declare (xargs :guard (and (natp n) (true-listp a))))
  (let ((__function__ 'sv::aig-loghead-nu))
    (declare (ignorable __function__))
    (b* (((when (or (zp n) (atom a))) '(nil))
         ((mv first rest) (car/cdr a)))
      (sv::aig-scons first
                     (sv::aig-loghead-nu (1- n) rest)))))

Theorem: true-listp-of-aig-loghead-nu

(defthm sv::true-listp-of-aig-loghead-nu
  (b* ((head (sv::aig-loghead-nu n a)))
    (true-listp head))
  :rule-classes :type-prescription)

Theorem: aig-loghead-nu-correct

(defthm sv::aig-loghead-nu-correct
  (b* ((head (sv::aig-loghead-nu n a)))
    (and (equal (sv::aig-list->s head env)
                (loghead (nfix n)
                         (sv::aig-list->u a env))))))