		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod-wiresearch-pivot

Signature
(elab-mod-wiresearch-pivot wire mininst minoffset maxinst maxoffset smartp) → pivotinst
Arguments: wire — Guard (natp wire).; mininst — Guard (natp mininst).; minoffset — Guard (natp minoffset).; maxinst — Guard (natp maxinst).; maxoffset — Guard (natp maxoffset).
Returns: pivotinst — Type (natp pivotinst).

Definitions and Theorems

Function: elab-mod-wiresearch-pivot

(defun elab-mod-wiresearch-pivot
       (wire mininst
             minoffset maxinst maxoffset smartp)
  (declare (xargs :guard (and (natp wire)
                              (natp mininst)
                              (natp minoffset)
                              (natp maxinst)
                              (natp maxoffset))))
  (declare (xargs :guard (and (< (+ 1 mininst) maxinst)
                              (<= minoffset wire)
                              (< wire maxoffset))))
  (let ((__function__ 'elab-mod-wiresearch-pivot))
    (declare (ignorable __function__))
    (if smartp (elab-mod-wiresearch-smartpivot
                    wire
                    mininst minoffset maxinst maxoffset)
      (elab-mod-wiresearch-dumbpivot mininst maxinst))))

Theorem: natp-of-elab-mod-wiresearch-pivot

(defthm natp-of-elab-mod-wiresearch-pivot
 (b*
  ((pivotinst
    (elab-mod-wiresearch-pivot wire mininst
                               minoffset maxinst maxoffset smartp)))
  (natp pivotinst))
 :rule-classes :type-prescription)

Theorem: elab-mod-wiresearch-pivot-lower-bound

(defthm elab-mod-wiresearch-pivot-lower-bound
 (implies
  (< (+ 1 (nfix mininst)) (nfix maxinst))
  (<
    (nfix mininst)
    (elab-mod-wiresearch-pivot wire mininst
                               minoffset maxinst maxoffset smartp)))
 :rule-classes :linear)

Theorem: elab-mod-wiresearch-pivot-upper-bound

(defthm elab-mod-wiresearch-pivot-upper-bound
 (implies
   (< (+ 1 (nfix mininst)) (nfix maxinst))
   (< (elab-mod-wiresearch-pivot wire mininst
                                 minoffset maxinst maxoffset smartp)
      (nfix maxinst)))
 :rule-classes :linear)