		Search-engine friendly clone of the ACL2 documentation.

Balance

Lit-in-bounds

Signature
(lit-in-bounds x var-bound) → *
Arguments: x — Guard (litp x).; var-bound — Guard (natp var-bound).

Definitions and Theorems

Function: lit-in-bounds

(defun lit-in-bounds (x var-bound)
  (declare (xargs :guard (and (litp x) (natp var-bound))))
  (let ((__function__ 'lit-in-bounds))
    (declare (ignorable __function__))
    (< (lit-id x) (lnfix var-bound))))

Theorem: lit-in-bounds-of-lit-fix-x

(defthm lit-in-bounds-of-lit-fix-x
  (equal (lit-in-bounds (lit-fix x) var-bound)
         (lit-in-bounds x var-bound)))

Theorem: lit-in-bounds-lit-equiv-congruence-on-x

(defthm lit-in-bounds-lit-equiv-congruence-on-x
  (implies (lit-equiv x x-equiv)
           (equal (lit-in-bounds x var-bound)
                  (lit-in-bounds x-equiv var-bound)))
  :rule-classes :congruence)

Theorem: lit-in-bounds-of-nfix-var-bound

(defthm lit-in-bounds-of-nfix-var-bound
  (equal (lit-in-bounds x (nfix var-bound))
         (lit-in-bounds x var-bound)))

Theorem: lit-in-bounds-nat-equiv-congruence-on-var-bound

(defthm lit-in-bounds-nat-equiv-congruence-on-var-bound
  (implies (nat-equiv var-bound var-bound-equiv)
           (equal (lit-in-bounds x var-bound)
                  (lit-in-bounds x var-bound-equiv)))
  :rule-classes :congruence)