Filtering...

acl2s-size

books/acl2s/acl2s-size

Included Books

cons-size top
other
(in-package "ACL2")
include-book
(include-book "acl2s/cons-size" :dir :system)
acl2s-sizefunction
(defun acl2s-size
  (x)
  (declare (xargs :guard t))
  (cond ((consp x) (+ 1 (acl2s-size (car x)) (acl2s-size (cdr x))))
    ((rationalp x) (integer-abs (numerator x)))
    ((stringp x) (length x))
    (t 0)))
acl2s-size-type-fctheorem
(defthm acl2s-size-type-fc
  (natp (acl2s-size x))
  :rule-classes ((:type-prescription) (:forward-chaining :trigger-terms ((acl2s-size x)))))
acons-acl2s-size-lemmatheorem
(defthm acons-acl2s-size-lemma
  (= (acl2s-size (acons x1 x2 x3))
    (+ 2 (acl2s-size x1) (acl2s-size x2) (acl2s-size x3)))
  :rule-classes ((:rewrite)))
acl2s-size-of-prod-cons1theorem
(defthm acl2s-size-of-prod-cons1
  (<= (acl2s-size y)
    (acl2s-size (prod-cons x y)))
  :rule-classes :linear)
acl2s-size-of-prod-cons2theorem
(defthm acl2s-size-of-prod-cons2
  (<= (acl2s-size x)
    (acl2s-size (prod-cons x y)))
  :rule-classes :linear)
acl2s-size-of-nth-lineartheorem
(defthm acl2s-size-of-nth-linear
  (implies (consp (double-rewrite x))
    (< (acl2s-size (nth i x)) (acl2s-size x)))
  :rule-classes ((:linear :backchain-limit-lst 0)))
acl2s-size-of-nth-linear-weaktheorem
(defthm acl2s-size-of-nth-linear-weak
  (<= (acl2s-size (nth i x)) (acl2s-size x))
  :rule-classes :linear)
acl2s-size-of-nthcdr-lineartheorem
(defthm acl2s-size-of-nthcdr-linear
  (implies (and (not (zp (double-rewrite n)))
      (consp (double-rewrite x)))
    (< (acl2s-size (nthcdr n x)) (acl2s-size x)))
  :hints (("Goal" :in-theory (enable nthcdr)))
  :rule-classes ((:linear :backchain-limit-lst 1)))
acl2s-size-of-nthcdr-linear-weaktheorem
(defthm acl2s-size-of-nthcdr-linear-weak
  (<= (acl2s-size (nthcdr n x)) (acl2s-size x))
  :hints (("Goal" :in-theory (enable nthcdr)))
  :rule-classes :linear)
acl2s-size-of-remove-duplicatesencapsulate
(encapsulate nil
  (local (include-book "arithmetic-5/top" :dir :system))
  (defthm acl2s-size-of-remove-duplicates
    (<= (acl2s-size (remove-duplicates-equal x)) (acl2s-size x))
    :rule-classes :linear))
acl2s-size-when-membertheorem
(defthm acl2s-size-when-member
  (implies (member-equal a (double-rewrite x))
    (< (acl2s-size a) (acl2s-size x)))
  :hints (("Goal" :in-theory (enable member-equal)))
  :rule-classes ((:linear :backchain-limit-lst 1 :match-free :all) (:rewrite :backchain-limit-lst 1 :match-free :all)))
acl2s-size-of-remove-assoc-equal-upper-boundtheorem
(defthm acl2s-size-of-remove-assoc-equal-upper-bound
  (<= (acl2s-size (remove-assoc-equal a x)) (acl2s-size x))
  :hints (("Goal" :in-theory (enable remove-assoc-equal)))
  :rule-classes :linear)
tail-acl2s-sizetheorem
(defthm tail-acl2s-size
  (implies (not (emptyp x))
    (< (acl2s-size (tail x)) (acl2s-size x)))
  :hints (("Goal" :in-theory (enable emptyp tail)))
  :rule-classes ((:rewrite :backchain-limit-lst 0) (:linear :backchain-limit-lst 0)))
head-acl2s-sizetheorem
(defthm head-acl2s-size
  (implies (not (emptyp x))
    (< (acl2s-size (head x)) (acl2s-size x)))
  :hints (("Goal" :in-theory (enable emptyp head)))
  :rule-classes ((:rewrite :backchain-limit-lst 0) (:linear :backchain-limit-lst 0)))
split-list-1-acl2s-sizetheorem
(defthm split-list-1-acl2s-size
  (implies (consp (double-rewrite x))
    (< (acl2s-size (mv-nth 1 (split-list-1 x del)))
      (acl2s-size x)))
  :hints (("Goal" :in-theory (enable split-list-1)))
  :rule-classes ((:rewrite :backchain-limit-lst 0) (:linear :backchain-limit-lst 0)))
records-acl2s-size-linear-arith-<=theorem
(defthm records-acl2s-size-linear-arith-<=
  (<= (acl2s-size (mget k r)) (acl2s-size r))
  :hints (("goal" :in-theory (enable mget
       recordp
       no-nil-val-alistp
       ordered-unique-key-alistp)))
  :rule-classes :linear)
records-acl2s-size-linear-arith-<2theorem
(defthm records-acl2s-size-linear-arith-<2
  (implies (mget k r)
    (< (acl2s-size (mget k r)) (acl2s-size r)))
  :hints (("goal" :in-theory (enable mget
       recordp
       no-nil-val-alistp
       ordered-unique-key-alistp)))
  :rule-classes ((:linear :backchain-limit-lst 1)))
records-acl2s-sizetheorem
(defthm records-acl2s-size
  (implies (consp r)
    (< (acl2s-size (mget k r)) (acl2s-size r)))
  :hints (("goal" :in-theory (enable mget
       recordp
       no-nil-val-alistp
       ordered-unique-key-alistp)))
  :rule-classes ((:linear :backchain-limit-lst 1)))
acl2s-size-evens-weaktheorem
(defthm acl2s-size-evens-weak
  (<= (acl2s-size (evens x)) (acl2s-size x))
  :hints (("Goal" :induct (evens x)))
  :rule-classes :linear)
acl2s-size-evens-strongtheorem
(defthm acl2s-size-evens-strong
  (implies (consp (cdr (double-rewrite x)))
    (< (acl2s-size (evens x)) (acl2s-size x)))
  :rule-classes ((:linear :backchain-limit-lst 1)))
acl2-size-appendtheorem
(defthm acl2-size-append
  (<= (acl2-size (append x y))
    (+ (acl2-size x) (acl2-size y) 1))
  :rule-classes ((:linear) (:rewrite)))
acl2s-size-append-tlptheorem
(defthm acl2s-size-append-tlp
  (implies (and (true-listp x) (true-listp y))
    (= (acl2s-size (append x y))
      (+ (acl2s-size x) (acl2s-size y))))
  :hints (("goal" :in-theory (enable append)))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))
rev-acl2s-sizetheorem
(defthm rev-acl2s-size
  (<= (acl2s-size (rev x)) (acl2s-size x))
  :hints (("Goal" :in-theory (e/d (rev))))
  :rule-classes ((:linear)))
rev-acl2s-size-tlptheorem
(defthm rev-acl2s-size-tlp
  (implies (true-listp x)
    (= (acl2s-size (rev x)) (acl2s-size x)))
  :hints (("Goal" :in-theory (enable rev)))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))
acl2s-size-of-hons-remove-duplicatestheorem
(defthm acl2s-size-of-hons-remove-duplicates
  (<= (acl2s-size (hons-remove-duplicates x)) (acl2s-size x))
  :hints (("Goal" :in-theory (enable hons-remove-duplicates)))
  :rule-classes ((:linear) (:rewrite)))
acl2s-size-<=-acl2-countencapsulate
(encapsulate nil
  (local (include-book "arithmetic-5/top" :dir :system))
  (defthm acl2s-size-<=-acl2-count
    (<= (acl2s-size x) (acl2-count x))
    :rule-classes :linear))
len-<=-acl2s-sizetheorem
(defthm len-<=-acl2s-size
  (<= (len x) (acl2s-size x))
  :rule-classes :linear)
acl2-count-removetheorem
(defthm acl2-count-remove
  (<= (acl2-count (remove a x)) (acl2-count x))
  :rule-classes :linear)
acl2-count-remove2theorem
(defthm acl2-count-remove2
  (<= (acl2-count (remove-equal a x)) (acl2-count x))
  :rule-classes :linear)
acl2s-size-built-in-1theorem
(defthm acl2s-size-built-in-1
  (o-p (acl2s-size x))
  :rule-classes :built-in-clause)
acl2s-size-built-inttheorem
(defthm acl2s-size-built-int
  (integerp (acl2s-size x))
  :rule-classes :built-in-clause)
acl2s-size-built-nattheorem
(defthm acl2s-size-built-nat
  (<= 0 (acl2s-size x))
  :rule-classes :built-in-clause)
acl2s-size-o<-<theorem
(defthm acl2s-size-o<-<
  (equal (o< (acl2s-size x) (acl2s-size y))
    (< (acl2s-size x) (acl2s-size y))))
acl2s-size-built-in-2theorem
(defthm acl2s-size-built-in-2
  (implies (consp x)
    (and (< (acl2s-size (car x)) (acl2s-size x))
      (o< (acl2s-size (car x)) (acl2s-size x))))
  :rule-classes ((:built-in-clause)))
acl2s-size-built-in-3theorem
(defthm acl2s-size-built-in-3
  (implies (consp x)
    (and (< (acl2s-size (cdr x)) (acl2s-size x))
      (o< (acl2s-size (cdr x)) (acl2s-size x))))
  :rule-classes ((:built-in-clause)))
acl2s-size-built-in-4theorem
(defthm acl2s-size-built-in-4
  (implies (not (atom x))
    (and (< (acl2s-size (car x)) (acl2s-size x))
      (o< (acl2s-size (car x)) (acl2s-size x))))
  :rule-classes :built-in-clause)
acl2s-size-built-in-5theorem
(defthm acl2s-size-built-in-5
  (implies (not (atom x))
    (and (< (acl2s-size (cdr x)) (acl2s-size x))
      (o< (acl2s-size (cdr x)) (acl2s-size x))))
  :rule-classes :built-in-clause)
acl2s-size-built-in-6theorem
(defthm acl2s-size-built-in-6
  (implies (not (endp x))
    (and (< (acl2s-size (car x)) (acl2s-size x))
      (o< (acl2s-size (car x)) (acl2s-size x))))
  :rule-classes :built-in-clause)
acl2s-size-built-in-7theorem
(defthm acl2s-size-built-in-7
  (implies (not (endp x))
    (and (< (acl2s-size (cdr x)) (acl2s-size x))
      (o< (acl2s-size (cdr x)) (acl2s-size x))))
  :rule-classes :built-in-clause)
acl2s-size-built-in-8encapsulate
(encapsulate nil
  (local (include-book "arithmetic-5/top" :dir :system))
  (defthm acl2s-size-built-in-8
    (implies (not (zp x))
      (and (< (acl2s-size (binary-+ x -1)) (acl2s-size x))
        (o< (acl2s-size (binary-+ x -1)) (acl2s-size x))))
    :rule-classes :built-in-clause)
  (defthm acl2s-size-built-in-9
    (implies (not (zp x))
      (and (< (acl2s-size (binary-+ -1 x)) (acl2s-size x))
        (o< (acl2s-size (binary-+ -1 x)) (acl2s-size x))))
    :rule-classes :built-in-clause)
  (defthm acl2s-size-built-in-10
    (implies (and (integerp x) (< 0 x))
      (and (< (acl2s-size (binary-+ x -1)) (acl2s-size x))
        (o< (acl2s-size (binary-+ x -1)) (acl2s-size x))))
    :rule-classes :built-in-clause)
  (defthm acl2s-size-built-in-11
    (implies (and (integerp x) (not (< x 0)) (not (= x 0)))
      (and (< (acl2s-size (binary-+ x -1)) (acl2s-size x))
        (o< (acl2s-size (binary-+ x -1)) (acl2s-size x))))
    :rule-classes :built-in-clause)
  (defthm acl2s-size-built-in-12
    (implies (and (integerp x) (not (< x 0)) (not (= x 0)))
      (and (< (acl2s-size (binary-+ x -1)) (acl2s-size x))
        (o< (acl2s-size (binary-+ x -1)) (acl2s-size x))))
    :rule-classes :built-in-clause)
  (defthm acl2s-size-built-in-13
    (implies (and (integerp x) (not (< x 0)) (not (equal x 0)))
      (and (< (acl2s-size (binary-+ x -1)) (acl2s-size x))
        (o< (acl2s-size (binary-+ x -1)) (acl2s-size x))))
    :rule-classes :built-in-clause)
  (defthm acl2s-size-built-in-14
    (implies (and (integerp x) (< 0 x))
      (and (< (acl2s-size (binary-+ -1 x)) (acl2s-size x))
        (o< (acl2s-size (binary-+ -1 x)) (acl2s-size x))))
    :rule-classes :built-in-clause)
  (defthm acl2s-size-built-in-15
    (implies (and (integerp x) (not (< x 0)) (not (= x 0)))
      (and (< (acl2s-size (binary-+ -1 x)) (acl2s-size x))
        (o< (acl2s-size (binary-+ -1 x)) (acl2s-size x))))
    :rule-classes :built-in-clause)
  (defthm acl2s-size-built-in-16
    (implies (and (integerp x) (not (< x 0)) (not (= 0 x)))
      (and (< (acl2s-size (binary-+ -1 x)) (acl2s-size x))
        (o< (acl2s-size (binary-+ -1 x)) (acl2s-size x))))
    :rule-classes :built-in-clause)
  (defthm acl2s-size-built-in-17
    (implies (and (integerp x) (not (< x 0)) (not (equal 0 x)))
      (and (< (acl2s-size (binary-+ -1 x)) (acl2s-size x))
        (o< (acl2s-size (binary-+ -1 x)) (acl2s-size x))))
    :rule-classes :built-in-clause)
  (defthm acl2s-size-built-in-18
    (implies (and (true-listp x) (not (eq x nil)))
      (and (< (acl2s-size (cdr x)) (acl2s-size x))
        (o< (acl2s-size (cdr x)) (acl2s-size x))))
    :rule-classes :built-in-clause)
  (defthm acl2s-size-built-in-19
    (implies (and (true-listp x) (not (null x)))
      (and (< (acl2s-size (cdr x)) (acl2s-size x))
        (o< (acl2s-size (cdr x)) (acl2s-size x))))
    :rule-classes :built-in-clause)
  (defthm acl2s-size-built-in-20
    (implies (and (true-listp x) (not (eq nil x)))
      (and (< (acl2s-size (cdr x)) (acl2s-size x))
        (o< (acl2s-size (cdr x)) (acl2s-size x))))
    :rule-classes :built-in-clause)
  (defthm acl2s-size-built-in-21
    (implies (and (true-listp x) (not (equal x nil)))
      (and (< (acl2s-size (cdr x)) (acl2s-size x))
        (o< (acl2s-size (cdr x)) (acl2s-size x))))
    :rule-classes :built-in-clause))
acl2s-size-car-cdr-lineartheorem
(defthm acl2s-size-car-cdr-linear
  (implies (consp x)
    (equal (acl2s-size x)
      (+ 1 (acl2s-size (car x)) (acl2s-size (cdr x)))))
  :rule-classes :linear)