		Search-engine friendly clone of the ACL2 documentation.

Aig-symbolic-arithmetic

Sv::aig-logtail-ns

Signature
(sv::aig-logtail-ns place x) → xx
Arguments: place — Guard (natp place).; x — Guard (true-listp x).
Returns: xx — Type (true-listp xx).

Definitions and Theorems

Function: aig-logtail-ns

(defun sv::aig-logtail-ns (place x)
  (declare (xargs :guard (and (natp place) (true-listp x))))
  (let ((__function__ 'sv::aig-logtail-ns))
    (declare (ignorable __function__))
    (if (or (zp place) (s-endp x))
        (llist-fix x)
      (sv::aig-logtail-ns (1- place)
                          (scdr x)))))

Theorem: true-listp-of-aig-logtail-ns

(defthm sv::true-listp-of-aig-logtail-ns
  (b* ((xx (sv::aig-logtail-ns place x)))
    (true-listp xx))
  :rule-classes :type-prescription)

Theorem: aig-logtail-ns-correct

(defthm sv::aig-logtail-ns-correct
  (b* ((xx (sv::aig-logtail-ns place x)))
    (and (equal (sv::aig-list->s xx env)
                (logtail (nfix place)
                         (sv::aig-list->s x env))))))