		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Bfr-ash-ss

Signature
(bfr-ash-ss place n shamt) → sh
Arguments: place — Guard (posp place).; n — Guard (true-listp n).; shamt — Guard (true-listp shamt).
Returns: sh — Type (true-listp sh).

Definitions and Theorems

Function: bfr-ash-ss

(defun bfr-ash-ss (place n shamt)
  (declare (xargs :guard (and (posp place)
                              (true-listp n)
                              (true-listp shamt))))
  (let ((__function__ 'bfr-ash-ss))
    (declare (ignorable __function__))
    (b* (((mv shdig shrst shend)
          (first/rest/end shamt))
         (place (lposfix place))
         ((when shend)
          (bfr-ite-bss shdig (bfr-logtail-ns 1 n)
                       (bfr-logapp-nss (1- place) nil n)))
         (rst (bfr-ash-ss (* 2 place) n shrst)))
      (bfr-ite-bss shdig rst (bfr-logtail-ns place rst)))))

Theorem: true-listp-of-bfr-ash-ss

(defthm true-listp-of-bfr-ash-ss
  (b* ((sh (bfr-ash-ss place n shamt)))
    (true-listp sh))
  :rule-classes :type-prescription)

Theorem: bfr-ash-ss-correct

(defthm bfr-ash-ss-correct
  (b* ((sh (bfr-ash-ss place n shamt)))
    (and (equal (bfr-list->s sh env)
                (ash (bfr-list->s n env)
                     (+ -1 (pos-fix place)
                        (* (pos-fix place)
                           (bfr-list->s shamt env))))))))

Theorem: bfr-ash-ss-deps

(defthm bfr-ash-ss-deps
  (b* ((sh (bfr-ash-ss place n shamt)))
    (implies (and (not (pbfr-list-depends-on varname param n))
                  (not (pbfr-list-depends-on varname param shamt)))
             (and (not (pbfr-list-depends-on varname param sh))))))