		Search-engine friendly clone of the ACL2 documentation.

Sparseint

Sparseint-concatenate

Form the concatenation (logapp) of two sparseints

Signature
(sparseint-concatenate width lsbs msbs) → concat
Arguments: width — Guard (natp width).; lsbs — Guard (sparseint-p lsbs).; msbs — Guard (sparseint-p msbs).
Returns: concat — Type (sparseint-p concat).

Definitions and Theorems

Function: sparseint-concatenate$inline

(defun sparseint-concatenate$inline (width lsbs msbs)
  (declare (xargs :guard (and (natp width)
                              (sparseint-p lsbs)
                              (sparseint-p msbs))))
  (let ((__function__ 'sparseint-concatenate))
    (declare (ignorable __function__))
    (sparseint$-concatenate width (sparseint-fix lsbs)
                            (sparseint-fix msbs))))

Theorem: sparseint-p-of-sparseint-concatenate

(defthm sparseint-p-of-sparseint-concatenate
  (b* ((concat (sparseint-concatenate$inline width lsbs msbs)))
    (sparseint-p concat))
  :rule-classes :rewrite)

Theorem: sparseint-concatenate-correct

(defthm sparseint-concatenate-correct
  (b* ((?concat (sparseint-concatenate$inline width lsbs msbs)))
    (equal (sparseint-val concat)
           (logapp width (sparseint-val lsbs)
                   (sparseint-val msbs)))))

Theorem: sparseint-concatenate$inline-of-nfix-width

(defthm sparseint-concatenate$inline-of-nfix-width
  (equal (sparseint-concatenate$inline (nfix width)
                                       lsbs msbs)
         (sparseint-concatenate$inline width lsbs msbs)))

Theorem: sparseint-concatenate$inline-nat-equiv-congruence-on-width

(defthm sparseint-concatenate$inline-nat-equiv-congruence-on-width
  (implies
       (nat-equiv width width-equiv)
       (equal (sparseint-concatenate$inline width lsbs msbs)
              (sparseint-concatenate$inline width-equiv lsbs msbs)))
  :rule-classes :congruence)

Theorem: sparseint-concatenate$inline-of-sparseint-fix-lsbs

(defthm sparseint-concatenate$inline-of-sparseint-fix-lsbs
  (equal (sparseint-concatenate$inline width (sparseint-fix lsbs)
                                       msbs)
         (sparseint-concatenate$inline width lsbs msbs)))

Theorem: sparseint-concatenate$inline-sparseint-equiv-congruence-on-lsbs

(defthm
    sparseint-concatenate$inline-sparseint-equiv-congruence-on-lsbs
  (implies
       (sparseint-equiv lsbs lsbs-equiv)
       (equal (sparseint-concatenate$inline width lsbs msbs)
              (sparseint-concatenate$inline width lsbs-equiv msbs)))
  :rule-classes :congruence)

Theorem: sparseint-concatenate$inline-of-sparseint-fix-msbs

(defthm sparseint-concatenate$inline-of-sparseint-fix-msbs
 (equal
      (sparseint-concatenate$inline width lsbs (sparseint-fix msbs))
      (sparseint-concatenate$inline width lsbs msbs)))

Theorem: sparseint-concatenate$inline-sparseint-equiv-congruence-on-msbs

(defthm
    sparseint-concatenate$inline-sparseint-equiv-congruence-on-msbs
  (implies
       (sparseint-equiv msbs msbs-equiv)
       (equal (sparseint-concatenate$inline width lsbs msbs)
              (sparseint-concatenate$inline width lsbs msbs-equiv)))
  :rule-classes :congruence)