		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-ash-ss

Signature
(aabf-ash-ss place n shamt man) → (mv sh new-man)
Arguments: place — Guard (posp place).; n — Guard (true-listp n).; shamt — Guard (true-listp shamt).

Definitions and Theorems

Function: aabf-ash-ss

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

Theorem: trivial-theorem-about-aabf-ash-ss

(defthm trivial-theorem-about-aabf-ash-ss
  (b* nil
    (b* ((?ignore (aabf-ash-ss place n shamt man)))
      t))
  :rule-classes nil)

Theorem: true-listp-of-aabf-ash-ss.sh

(defthm true-listp-of-aabf-ash-ss.sh
  (b* (((mv ?sh ?new-man)
        (aabf-ash-ss place n shamt man)))
    (true-listp sh))
  :rule-classes :type-prescription)

Theorem: aabf-extension-p-of-aabf-ash-ss

(defthm aabf-extension-p-of-aabf-ash-ss
  (b* (((mv ?sh ?new-man)
        (aabf-ash-ss place n shamt man)))
    (aabf-extension-p new-man man)))

Theorem: aabf-p-of-aabf-ash-ss

(defthm aabf-p-of-aabf-ash-ss
  (b* (((mv sh new-man)
        (aabf-ash-ss place n shamt man)))
    (implies (and (aabflist-p n man)
                  (aabflist-p shamt man))
             (and (aabflist-p sh new-man)))))

Theorem: aabf-eval-of-aabf-ash-ss

(defthm aabf-eval-of-aabf-ash-ss
 (b* (((mv sh new-man)
       (aabf-ash-ss place n shamt man)))
  (implies
   (and (aabflist-p n man)
        (aabflist-p shamt man))
   (and
    (equal
       (bools->int (aabflist-eval sh env new-man))
       (ash (bools->int (aabflist-eval n env man))
            (+ -1 (pos-fix place)
               (* (pos-fix place)
                  (bools->int (aabflist-eval shamt env man))))))))))

Theorem: aabf-pred-of-aabf-ash-ss

(defthm aabf-pred-of-aabf-ash-ss
  (b* (((mv sh new-man)
        (aabf-ash-ss place n shamt man)))
    (implies (and (aabflist-p n man)
                  (aabflist-p shamt man)
                  (aabflist-pred n man)
                  (aabflist-pred shamt man))
             (and (aabflist-pred sh new-man)))))