bounded-integer-alistp

other

(in-package "ACL2")

in-theory

(in-theory (disable bounded-integer-alistp))

bounded-integer-alistp-of-appendtheorem

(defthm bounded-integer-alistp-of-append
  (implies (true-listp x)
    (equal (bounded-integer-alistp (append x y) n)
      (and (bounded-integer-alistp x n)
        (bounded-integer-alistp y n))))
  :hints (("Goal" :in-theory (enable bounded-integer-alistp append))))

bounded-integer-alistp-of-revappendtheorem

(defthm bounded-integer-alistp-of-revappend
  (implies (and (bounded-integer-alistp x n)
      (bounded-integer-alistp y n))
    (bounded-integer-alistp (revappend x y) n))
  :hints (("Goal" :in-theory (enable bounded-integer-alistp revappend))))

integerp-of-car-of-assoc-equal-when-bounded-integer-alistptheorem

(defthm integerp-of-car-of-assoc-equal-when-bounded-integer-alistp
  (implies (and (bounded-integer-alistp array n) (assoc-equal i array))
    (equal (integerp (car (assoc-equal i array)))
      (not (eq :header (car (assoc-equal i array))))))
  :hints (("Goal" :in-theory (enable bounded-integer-alistp assoc-equal))))

bound-of-car-of-assoc-equal-when-bounded-integer-alistptheorem

(defthm bound-of-car-of-assoc-equal-when-bounded-integer-alistp
  (implies (and (bounded-integer-alistp array n)
      (natp n)
      (assoc-equal i array))
    (equal (< (car (assoc-equal i array)) n)
      (if (eq :header (car (assoc-equal i array)))
        (not (equal n 0))
        t)))
  :hints (("Goal" :in-theory (enable bounded-integer-alistp assoc-equal))))

not-assoc-equal-when-bounded-integer-alistp-out-of-boundstheorem

(defthmd not-assoc-equal-when-bounded-integer-alistp-out-of-bounds
  (implies (and (bounded-integer-alistp array bound)
      (<= bound index)
      (natp index))
    (equal (assoc-equal index array) nil))
  :hints (("Goal" :in-theory (enable bounded-integer-alistp assoc-equal))))

bound2-of-car-of-assoc-equal-when-bounded-integer-alistptheorem

(defthm bound2-of-car-of-assoc-equal-when-bounded-integer-alistp
  (implies (and (bounded-integer-alistp array n) (assoc-equal i array))
    (not (< (car (assoc-equal i array)) 0)))
  :hints (("Goal" :in-theory (enable bounded-integer-alistp assoc-equal))))

bounded-integer-alistp-of-constheorem

(defthm bounded-integer-alistp-of-cons
  (equal (bounded-integer-alistp (cons item array) n)
    (and (bounded-integer-alistp array n)
      (or (eq :header (car item))
        (and (natp (car item)) (< (car item) n)))))
  :hints (("Goal" :in-theory (enable bounded-integer-alistp))))

bounded-integer-alistp-of-niltheorem

(defthm bounded-integer-alistp-of-nil
  (equal (bounded-integer-alistp 'nil n) t)
  :hints (("Goal" :in-theory (enable bounded-integer-alistp))))

assoc-equal-forward-when-bounded-integer-alistptheorem

(defthmd assoc-equal-forward-when-bounded-integer-alistp
  (implies (and (assoc-equal i array)
      (bounded-integer-alistp array n)
      (not (equal :header i)))
    (and (natp i) (< i n)))
  :rule-classes :forward-chaining)