		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-logext-ns

Signature
(aabf-logext-ns n x) → xx
Arguments: n — Guard (posp n).; x — Guard (true-listp x).

Definitions and Theorems

Function: aabf-logext-ns

(defun aabf-logext-ns (n x)
  (declare (xargs :guard (and (posp n) (true-listp x))))
  (declare (xargs :guard (and)))
  (let ((__function__ 'aabf-logext-ns))
    (declare (ignorable __function__))
    (b* ((n (lposfix n))
         ((mv head tail ?end)
          (aabf-first/rest/end x))
         ((when end) (llist-fix x))
         ((when (eql n 1)) (list head)))
      (aabf-scons head (aabf-logext-ns (1- n) tail)))))

Theorem: trivial-theorem-about-aabf-logext-ns

(defthm trivial-theorem-about-aabf-logext-ns
  (b* nil
    (b* ((?ignore (aabf-logext-ns n x))) t))
  :rule-classes nil)

Theorem: true-listp-of-aabf-logext-ns.xx

(defthm true-listp-of-aabf-logext-ns.xx
  (b* ((?xx (aabf-logext-ns n x)))
    (true-listp xx))
  :rule-classes :type-prescription)

Theorem: aabf-p-of-aabf-logext-ns

(defthm aabf-p-of-aabf-logext-ns
  (b* ((xx (aabf-logext-ns n x)))
    (implies (and (aabflist-p x man))
             (and (aabflist-p xx man)))))

Theorem: aabf-eval-of-aabf-logext-ns

(defthm aabf-eval-of-aabf-logext-ns
 (b* ((xx (aabf-logext-ns n x)))
  (implies
    (and (aabflist-p x man))
    (and (equal (bools->int (aabflist-eval xx env man))
                (logext (pos-fix n)
                        (bools->int (aabflist-eval x env man))))))))

Theorem: aabf-pred-of-aabf-logext-ns

(defthm aabf-pred-of-aabf-logext-ns
  (b* ((xx (aabf-logext-ns n x)))
    (implies (and (aabflist-p x man)
                  (aabflist-pred x man))
             (and (aabflist-pred xx man)))))