		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Bfr-logext-ns

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

Definitions and Theorems

Function: bfr-logext-ns

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

Theorem: true-listp-of-bfr-logext-ns

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

Theorem: bfr-logext-ns-correct

(defthm bfr-logext-ns-correct
  (b* ((xx (bfr-logext-ns n x)))
    (and (equal (bfr-list->s xx env)
                (logext (pos-fix n)
                        (bfr-list->s x env))))))

Theorem: bfr-logext-ns-deps

(defthm bfr-logext-ns-deps
  (b* ((xx (bfr-logext-ns n x)))
    (implies (and (not (pbfr-list-depends-on varname param x)))
             (and (not (pbfr-list-depends-on varname param xx))))))