		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod-wiresearch-dumbpivot

Signature
(elab-mod-wiresearch-dumbpivot mininst maxinst) → pivotinst
Arguments: mininst — Guard (natp mininst).; maxinst — Guard (natp maxinst).
Returns: pivotinst — Type (natp pivotinst).

Definitions and Theorems

Function: elab-mod-wiresearch-dumbpivot

(defun elab-mod-wiresearch-dumbpivot (mininst maxinst)
  (declare (xargs :guard (and (natp mininst) (natp maxinst))))
  (declare (xargs :guard (< (+ 1 mininst) maxinst)))
  (let ((__function__ 'elab-mod-wiresearch-dumbpivot))
    (declare (ignorable __function__))
    (b* ((maxinst (mbe :logic (pos-fix maxinst)
                       :exec maxinst))
         (mininst (lnfix mininst))
         (guess (ash (- maxinst mininst) -1)))
      (min (+ -1 maxinst)
           (max (+ 1 mininst) guess)))))

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

(defthm natp-of-elab-mod-wiresearch-dumbpivot
  (b* ((pivotinst (elab-mod-wiresearch-dumbpivot mininst maxinst)))
    (natp pivotinst))
  :rule-classes :type-prescription)

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

(defthm elab-mod-wiresearch-dumbpivot-lower-bound
  (implies (< (+ 1 (nfix mininst)) (nfix maxinst))
           (< (nfix mininst)
              (elab-mod-wiresearch-dumbpivot mininst maxinst)))
  :rule-classes :linear)

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

(defthm elab-mod-wiresearch-dumbpivot-upper-bound
  (implies (< (+ 1 (nfix mininst)) (nfix maxinst))
           (< (elab-mod-wiresearch-dumbpivot mininst maxinst)
              (nfix maxinst)))
  :rule-classes :linear)