		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Within-1

Signature
(within-1 x y) → *
Arguments: x — Guard (natp x).; y — Guard (natp y).

Definitions and Theorems

Function: within-1

(defun within-1 (x y)
  (declare (xargs :guard (and (natp x) (natp y))))
  (let ((__function__ 'within-1))
    (declare (ignorable __function__))
    (<= (abs (- (lnfix x) (lnfix y))) 1)))

Theorem: within-1-when-equal

(defthm within-1-when-equal
  (within-1 x x))

Theorem: within-1-when-y-greater

(defthm within-1-when-y-greater
  (implies (equal (+ 1 (nfix x)) (nfix y))
           (within-1 x y)))

Theorem: within-1-when-x-greater

(defthm within-1-when-x-greater
  (implies (equal (+ 1 (nfix y)) (nfix x))
           (within-1 x y)))

Theorem: within-1-commutative

(defthm within-1-commutative
  (implies (within-1 y x) (within-1 x y)))

Theorem: <-when-within-1

(defthm <-when-within-1
  (implies (and (within-1 x y) (natp x) (natp y))
           (equal (< x y) (equal (+ 1 x) y))))

Theorem: >-when-within-1

(defthm >-when-within-1
  (implies (and (within-1 x y) (natp x) (natp y))
           (equal (< y x) (equal (+ 1 y) x))))

Theorem: within-1-when-<

(defthm within-1-when-<
  (implies (< (nfix x) (nfix y))
           (equal (within-1 x y)
                  (equal (nfix y) (+ 1 (nfix x))))))

Theorem: within-1-when->

(defthm within-1-when->
  (implies (> (nfix x) (nfix y))
           (equal (within-1 x y)
                  (equal (nfix x) (+ 1 (nfix y))))))

Theorem: within-1-of-nfix-x

(defthm within-1-of-nfix-x
  (equal (within-1 (nfix x) y)
         (within-1 x y)))

Theorem: within-1-nat-equiv-congruence-on-x

(defthm within-1-nat-equiv-congruence-on-x
  (implies (nat-equiv x x-equiv)
           (equal (within-1 x y)
                  (within-1 x-equiv y)))
  :rule-classes :congruence)

Theorem: within-1-of-nfix-y

(defthm within-1-of-nfix-y
  (equal (within-1 x (nfix y))
         (within-1 x y)))

Theorem: within-1-nat-equiv-congruence-on-y

(defthm within-1-nat-equiv-congruence-on-y
  (implies (nat-equiv y y-equiv)
           (equal (within-1 x y)
                  (within-1 x y-equiv)))
  :rule-classes :congruence)