		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-truncate-height

Signature
(sparseint$-truncate-height width x height) → (mv new-x new-height)
Arguments: width — Guard (posp width).; x — Guard (sparseint$-p x).
Returns: new-x — Type (equal new-x (sparseint$-truncate width x)).; new-height — Type (equal new-height (sparseint$-height (sparseint$-truncate width x))).

Definitions and Theorems

Function: sparseint$-truncate-height

(defun sparseint$-truncate-height (width x height)
 (declare (xargs :guard (and (posp width) (sparseint$-p x))))
 (declare (xargs :guard (and (sparseint$-height-correctp x)
                             (equal height (sparseint$-height x)))))
 (let ((__function__ 'sparseint$-truncate-height))
   (declare (ignorable __function__))
   (b* ((height (mbe :logic (sparseint$-height x)
                     :exec height)))
     (sparseint$-case x :leaf (mv (sparseint$-fix x) height)
                      :concat
                      (if (< x.width (lposfix width))
                          (mv (sparseint$-fix x) height)
                        (sparseint$-truncate-height
                             width x.lsbs
                             (- height (if x.msbs-taller 2 1))))))))

Theorem: return-type-of-sparseint$-truncate-height.new-x

(defthm return-type-of-sparseint$-truncate-height.new-x
  (b* (((mv ?new-x ?new-height)
        (sparseint$-truncate-height width x height)))
    (equal new-x (sparseint$-truncate width x)))
  :rule-classes :rewrite)

Theorem: return-type-of-sparseint$-truncate-height.new-height

(defthm return-type-of-sparseint$-truncate-height.new-height
  (b* (((mv ?new-x ?new-height)
        (sparseint$-truncate-height width x height)))
    (equal new-height
           (sparseint$-height (sparseint$-truncate width x))))
  :rule-classes :rewrite)

Theorem: sparseint$-truncate-height-of-pos-fix-width

(defthm sparseint$-truncate-height-of-pos-fix-width
  (equal (sparseint$-truncate-height (pos-fix width)
                                     x height)
         (sparseint$-truncate-height width x height)))

Theorem: sparseint$-truncate-height-pos-equiv-congruence-on-width

(defthm sparseint$-truncate-height-pos-equiv-congruence-on-width
 (implies (pos-equiv width width-equiv)
          (equal (sparseint$-truncate-height width x height)
                 (sparseint$-truncate-height width-equiv x height)))
 :rule-classes :congruence)

Theorem: sparseint$-truncate-height-of-sparseint$-fix-x

(defthm sparseint$-truncate-height-of-sparseint$-fix-x
  (equal (sparseint$-truncate-height width (sparseint$-fix x)
                                     height)
         (sparseint$-truncate-height width x height)))

Theorem: sparseint$-truncate-height-sparseint$-equiv-congruence-on-x

(defthm sparseint$-truncate-height-sparseint$-equiv-congruence-on-x
 (implies (sparseint$-equiv x x-equiv)
          (equal (sparseint$-truncate-height width x height)
                 (sparseint$-truncate-height width x-equiv height)))
 :rule-classes :congruence)