Filtering...

base

books/acl2s/defdata/base
other
(in-package "ACL2S")
other
(include-book "splitnat")
other
(include-book "switchnat")
other
(include-book "number-enums-sampling")
other
(include-book "defdata-core")
other
(include-book "random-state")
other
(include-book "enumerators-gen")
other
(include-book "library-support")
other
(include-book "register-data-constructor")
other
(include-book "register-type")
other
(include-book "register-combinator")
other
(include-book "listof")
other
(include-book "alistof")
other
(include-book "record")
other
(include-book "map")
other
(include-book "tau-characterization")
other
(include-book "tools/rulesets" :dir :system)
other
(include-book "var-book" :ttags :all)
allpfunction
(defun allp
  (x)
  (declare (xargs :mode :logic :guard t)
    (ignore x))
  t)
other
(in-theory (disable allp))
other
(table allp-aliases-table nil)
other
(table allp-aliases-table
  'allp
  'all
  :put)
allp-aliases-tablefunction
(defun allp-aliases-table
  (wrld)
  "api to get the alist representing alias table allp-aliases"
  (declare (xargs :guard (plist-worldp wrld)))
  (table-alist 'allp-aliases-table
    wrld))
other
(set-override-hints nil)
other
(local (include-book "std/system/non-parallel-book" :dir :system))
other
(local (non-parallel-book))
other
(register-data-constructor (consp cons)
  ((allp car) (allp cdr))
  :rule-classes nil
  :verbose t)
other
(register-data-constructor (symbolp intern$)
  ((stringp symbol-name) (stringp symbol-package-name))
  :rule-classes nil
  :proper nil)
other
(register-data-constructor (rationalp /)
  ((integerp numerator) (posp denominator))
  :rule-classes nil
  :proper nil)
other
(register-data-constructor (acl2-numberp complex)
  ((rationalp realpart) (rationalp imagpart))
  :rule-classes nil)
other
(def-const *character-values*
  *standard-chars*)
other
(def-const *len-character-values*
  (len *character-values*))
other
(def-const *alpha-chars*
  '(#\A #\B
    #\C
    #\D
    #\E
    #\F
    #\G
    #\H
    #\I
    #\J
    #\K
    #\L
    #\M
    #\N
    #\O
    #\P
    #\Q
    #\R
    #\S
    #\T
    #\U
    #\V
    #\W
    #\X
    #\Y
    #\Z
    #\a
    #\b
    #\c
    #\d
    #\e
    #\f
    #\g
    #\h
    #\i
    #\j
    #\k
    #\l
    #\m
    #\n
    #\o
    #\p
    #\q
    #\r
    #\s
    #\t
    #\u
    #\v
    #\w
    #\x
    #\y
    #\z))
other
(def-const *len-alpha-chars*
  (len *alpha-chars*))
other
(def-const *alpha-low-chars*
  '(#\a #\b
    #\c
    #\d
    #\e
    #\f
    #\g
    #\h
    #\i
    #\j
    #\k
    #\l
    #\m
    #\n
    #\o
    #\p
    #\q
    #\r
    #\s
    #\t
    #\u
    #\v
    #\w
    #\x
    #\y
    #\z))
other
(def-const *len-alpha-low-chars*
  (len *alpha-low-chars*))
other
(def-const *alpha-up-chars*
  '(#\A #\B
    #\C
    #\D
    #\E
    #\F
    #\G
    #\H
    #\I
    #\J
    #\K
    #\L
    #\M
    #\N
    #\O
    #\P
    #\Q
    #\R
    #\S
    #\T
    #\U
    #\V
    #\W
    #\X
    #\Y
    #\Z))
other
(def-const *len-alpha-up-chars*
  (len *alpha-up-chars*))
other
(def-const *alpha-num-chars*
  '(#\A #\B
    #\C
    #\D
    #\E
    #\F
    #\G
    #\H
    #\I
    #\J
    #\K
    #\L
    #\M
    #\N
    #\O
    #\P
    #\Q
    #\R
    #\S
    #\T
    #\U
    #\V
    #\W
    #\X
    #\Y
    #\Z
    #\0
    #\1
    #\2
    #\3
    #\4
    #\5
    #\6
    #\7
    #\8
    #\9
    #\a
    #\b
    #\c
    #\d
    #\e
    #\f
    #\g
    #\h
    #\i
    #\j
    #\k
    #\l
    #\m
    #\n
    #\o
    #\p
    #\q
    #\r
    #\s
    #\t
    #\u
    #\v
    #\w
    #\x
    #\y
    #\z))
other
(def-const *len-alpha-num-chars*
  (len *alpha-num-chars*))
other
(defthm integerp-mod
  (implies (and (integerp m) (integerp n))
    (integerp (mod m n)))
  :rule-classes (:rewrite :type-prescription))
other
(encapsulate nil
  (local (include-book "arithmetic-5/top" :dir :system))
  (defthm mod-nonnegative-integer-args
    (implies (and (integerp x) (integerp y) (< 0 y))
      (<= 0 (mod x y)))
    :rule-classes ((:rewrite :backchain-limit-lst 1) (:type-prescription)))
  (defun get-character-list-from-positions
    (l)
    (declare (xargs :guard (nat-listp l)))
    (if (endp l)
      nil
      (let* ((pos (mod (car l) (len *alpha-num-chars*))) (char (nth pos *alpha-num-chars*)))
        (cons char
          (get-character-list-from-positions (cdr l))))))
  (defun get-standard-char-list-from-positions
    (l)
    (declare (xargs :guard (nat-listp l)))
    (if (endp l)
      nil
      (let* ((pos (mod (car l) (len *standard-chars*))) (char (nth pos *standard-chars*)))
        (cons char
          (get-standard-char-list-from-positions (cdr l))))))
  (defthm get-character-list-from-positions--character-listp
    (implies (nat-listp l)
      (and (character-listp (get-character-list-from-positions l))
        (character-listp (get-standard-char-list-from-positions l))))
    :hints (("goal" :in-theory (enable standard-char-listp)))))
other
(local (in-theory (disable mod)))
other
(def-const *boolean-values* '(t nil))
nth-boolean-builtinfunction
(defun nth-boolean-builtin
  (n)
  (declare (xargs :guard (natp n)))
  (nth (mod n 2) *boolean-values*))
nth-string-builtinfunction
(defun nth-string-builtin
  (n)
  (declare (xargs :guard (natp n)))
  (let* ((str-len (1+ (mod n 7))) (char-pos-list (split-nat str-len n))
      (charlist (get-character-list-from-positions char-pos-list)))
    (coerce charlist 'string)))
other
(defthm nth-string-is-stringp
  (implies (natp n)
    (stringp (nth-string-builtin n)))
  :rule-classes (:rewrite :type-prescription))
standard-stringpfunction
(defun standard-stringp
  (x)
  (declare (xargs :guard t))
  (and (stringp x)
    (standard-char-listp (coerce x 'list))))
nth-standard-string-builtinfunction
(defun nth-standard-string-builtin
  (n)
  (declare (xargs :guard (natp n)))
  (let* ((str-len (1+ (mod n 7))) (char-pos-list (split-nat str-len n))
      (charlist (get-standard-char-list-from-positions char-pos-list)))
    (coerce charlist 'string)))
nth-symbol-builtinfunction
(defun nth-symbol-builtin
  (n)
  (declare (xargs :guard (natp n)))
  (intern$ (nth-string-builtin n)
    "ACL2S"))
nth-character-builtinfunction
(defun nth-character-builtin
  (n)
  (declare (xargs :guard (natp n)))
  (nth (mod n *len-character-values*)
    *character-values*))
nth-alpha-num-characterfunction
(defun nth-alpha-num-character
  (n)
  (declare (xargs :guard (natp n)))
  (nth (mod n *len-alpha-num-chars*)
    *alpha-num-chars*))
nth-character-list-builtinfunction
(defun nth-character-list-builtin
  (n)
  (declare (xargs :guard (natp n)))
  (let* ((str-len (1+ (mod n 7))) (char-pos-list (split-nat str-len n))
      (charlist (get-character-list-from-positions char-pos-list)))
    charlist))
nth-standard-char-list-builtinfunction
(defun nth-standard-char-list-builtin
  (n)
  (declare (xargs :guard (natp n)))
  (let* ((str-len (1+ (mod n 7))) (char-pos-list (split-nat str-len n))
      (charlist (get-standard-char-list-from-positions char-pos-list)))
    charlist))
register-custom-typemacro
(defmacro register-custom-type
  (typename typesize
    enum
    pred
    &key
    verbose)
  `(register-type ,ACL2S::TYPENAME
    :domain-size ,ACL2S::TYPESIZE
    :predicate ,ACL2S::PRED
    :enumerator ,ACL2S::ENUM
    :verbose ,ACL2S::VERBOSE))
other
(register-custom-type neg
  t
  nth-neg-builtin
  negp)
other
(register-custom-type pos
  t
  nth-pos-builtin
  posp)
other
(register-custom-type nat
  t
  nth-nat-builtin
  natp)
other
(register-custom-type non-pos-integer
  t
  nth-non-pos-integer-builtin
  non-pos-integerp)
other
(register-custom-type non-0-integer
  t
  nth-non-0-integer-builtin
  non-0-integerp)
other
(register-custom-type integer
  t
  nth-integer-builtin
  integerp)
other
(register-custom-type neg-ratio
  t
  nth-neg-ratio-builtin
  neg-ratiop)
other
(register-custom-type pos-ratio
  t
  nth-pos-ratio-builtin
  pos-ratiop)
other
(defdata ratio
  (oneof pos-ratio neg-ratio))
other
(defthm ratiop-compound-recognizer
  (equal (ratiop x)
    (and (rationalp x) (not (integerp x))))
  :rule-classes :compound-recognizer)
other
(register-custom-type neg-rational
  t
  nth-neg-rational-builtin
  neg-rationalp)
other
(register-custom-type pos-rational
  t
  nth-pos-rational-builtin
  pos-rationalp)
other
(register-custom-type non-neg-rational
  t
  nth-non-neg-rational-builtin
  non-neg-rationalp)
other
(register-custom-type non-pos-rational
  t
  nth-non-pos-rational-builtin
  non-pos-rationalp)
other
(register-custom-type non-0-rational
  t
  nth-non-0-rational-builtin
  non-0-rationalp)
other
(register-custom-type rational
  t
  nth-rational-builtin
  rationalp)
other
(register-custom-type complex-rational
  t
  nth-complex-rational-builtin
  complex-rationalp)
other
(register-custom-type acl2-number
  t
  nth-acl2-number-builtin
  acl2-numberp)
other
(def-const *number-testing-limit* 1000)
nth-neg-testingfunction
(defun nth-neg-testing
  (n)
  (declare (xargs :guard (natp n)))
  (let ((n-small (mod n *number-testing-limit*)))
    (nth-neg-builtin n-small)))
nth-pos-testingfunction
(defun nth-pos-testing
  (n)
  (declare (xargs :guard (natp n)))
  (let ((n-small (mod n *number-testing-limit*)))
    (nth-pos-builtin n-small)))
nth-nat-testingfunction
(defun nth-nat-testing
  (n)
  (declare (xargs :guard (natp n)))
  (let ((n-small (mod n *number-testing-limit*)))
    (nth-nat-builtin n-small)))
nth-non-pos-integer-testingfunction
(defun nth-non-pos-integer-testing
  (n)
  (declare (xargs :guard (natp n)))
  (let ((n-small (mod n *number-testing-limit*)))
    (nth-non-pos-integer-builtin n-small)))
nth-non-0-integer-testingfunction
(defun nth-non-0-integer-testing
  (n)
  (declare (xargs :guard (natp n)))
  (let ((n-small (mod n *number-testing-limit*)))
    (nth-non-0-integer-builtin n-small)))
nth-integer-testingfunction
(defun nth-integer-testing
  (n)
  (declare (xargs :guard (natp n)))
  (let ((n-small (mod n *number-testing-limit*)))
    (nth-integer-builtin n-small)))
nth-neg-ratio-testingfunction
(defun nth-neg-ratio-testing
  (n)
  (declare (xargs :guard (natp n)
      :verify-guards nil))
  (let ((n-small (mod n *number-testing-limit*)))
    (nth-neg-ratio-builtin n-small)))
nth-pos-ratio-testingfunction
(defun nth-pos-ratio-testing
  (n)
  (declare (xargs :guard (natp n)
      :verify-guards nil))
  (let ((n-small (mod n *number-testing-limit*)))
    (nth-pos-ratio-builtin n-small)))
nth-ratio-testingfunction
(defun nth-ratio-testing
  (n)
  (declare (xargs :guard (natp n)
      :verify-guards nil
      :mode :program))
  (let ((n-small (mod n *number-testing-limit*)))
    (nth-ratio-builtin n-small)))
nth-neg-rational-testingfunction
(defun nth-neg-rational-testing
  (n)
  (declare (xargs :guard (natp n)))
  (let ((n-small (mod n *number-testing-limit*)))
    (nth-neg-rational-builtin n-small)))
nth-pos-rational-testingfunction
(defun nth-pos-rational-testing
  (n)
  (declare (xargs :guard (natp n)))
  (let ((n-small (mod n *number-testing-limit*)))
    (nth-pos-rational-builtin n-small)))
nth-non-neg-rational-testingfunction
(defun nth-non-neg-rational-testing
  (n)
  (declare (xargs :guard (natp n)))
  (let ((n-small (mod n *number-testing-limit*)))
    (nth-non-neg-rational-builtin n-small)))
nth-non-pos-rational-testingfunction
(defun nth-non-pos-rational-testing
  (n)
  (declare (xargs :guard (natp n)))
  (let ((n-small (mod n *number-testing-limit*)))
    (nth-non-pos-rational-builtin n-small)))
nth-non-0-rational-testingfunction
(defun nth-non-0-rational-testing
  (n)
  (declare (xargs :guard (natp n)))
  (let ((n-small (mod n *number-testing-limit*)))
    (nth-non-0-rational-builtin n-small)))
nth-rational-testingfunction
(defun nth-rational-testing
  (n)
  (declare (xargs :guard (natp n)))
  (let ((n-small (mod n *number-testing-limit*)))
    (nth-rational-builtin n-small)))
nth-complex-rational-testingfunction
(defun nth-complex-rational-testing
  (n)
  (declare (xargs :guard (natp n)))
  (let ((n-small (mod n *number-testing-limit*)))
    (nth-complex-rational-builtin n-small)))
nth-acl2-number-testingfunction
(defun nth-acl2-number-testing
  (n)
  (declare (xargs :guard (natp n)))
  (let ((n-small (mod n *number-testing-limit*)))
    (nth-acl2-number-builtin n-small)))
other
(register-custom-type boolean
  2
  nth-boolean-builtin
  booleanp)
other
(register-custom-type symbol
  t
  nth-symbol-builtin
  symbolp)
other
(verify-termination legal-constantp)
other
(verify-guards legal-constantp)
proper-symbolpfunction
(defun proper-symbolp
  (x)
  (declare (xargs :guard t))
  (and (symbolp x)
    (not (or (keywordp x)
        (booleanp x)
        (legal-constantp x)))))
other
(local (in-theory (disable legal-constantp)))
other
(def-const *nice-symbol-names*
  '(x y
    z
    a
    b
    c
    i
    j
    k
    p
    q
    r
    s
    u
    v
    w
    l
    d
    e
    f
    g
    h
    m
    n))
nth-proper-symbol-builtinfunction
(defun nth-proper-symbol-builtin
  (n)
  (declare (xargs :guard (natp n)))
  (let ((psym (nth-symbol-builtin n)))
    (if (proper-symbolp psym)
      psym
      (nth (mod n (len *nice-symbol-names*))
        *nice-symbol-names*))))
other
(register-custom-type proper-symbol
  t
  nth-proper-symbol-builtin
  proper-symbolp)
other
(local (defthm symbolp-helper
    (implies (and (symbol-listp l)
        (< n (len l)))
      (symbolp (nth n l)))))
other
(local (include-book "arithmetic-5/top" :dir :system))
other
(local (defthm mod-helper
    (implies (and (posp m) (natp n))
      (< (mod n m) m))))
other
(defthm nth-proper-symbol-builtin-type
  (implies (natp n)
    (symbolp (nth-proper-symbol-builtin n))))
nth-keyword-builtinfunction
(defun nth-keyword-builtin
  (n)
  (declare (xargs :guard (natp n)))
  (let ((psym (nth-proper-symbol-builtin n)))
    (intern (symbol-name psym) "KEYWORD")))
other
(register-custom-type keyword
  t
  nth-keyword-builtin
  keywordp)
non-keyword-symbolpfunction
(defun non-keyword-symbolp
  (x)
  (declare (xargs :guard t))
  (and (symbolp x) (not (keywordp x))))
nth-non-keyword-symbol-builtinfunction
(defun nth-non-keyword-symbol-builtin
  (n)
  (declare (xargs :guard (natp n)))
  (nth-proper-symbol-builtin n))
other
(register-custom-type non-keyword-symbol
  t
  nth-non-keyword-symbol-builtin
  non-keyword-symbolp)
nth-character-uniform-builtinfunction
(defun nth-character-uniform-builtin
  (m seed)
  (declare (ignorable m))
  (declare (type (unsigned-byte 63) seed))
  (declare (xargs :guard (and (natp m)
        (unsigned-byte-p 63 seed))))
  (mv-let (n seed)
    (random-natural-seed seed)
    (mv (nth-character-builtin n)
      (the (unsigned-byte 63) seed))))
other
(register-type character
  :domain-size 62
  :enumerator nth-character-builtin
  :predicate characterp
  :enum/acc nth-character-uniform-builtin)
nth-standard-char-builtinfunction
(defun nth-standard-char-builtin
  (n)
  (declare (xargs :guard (natp n)))
  (nth (mod n 96) *standard-chars*))
other
(register-custom-type standard-char
  96
  nth-standard-char-builtin
  standard-char-p)
other
(register-custom-type string
  t
  nth-string-builtin
  stringp)
other
(register-custom-type standard-string
  t
  nth-standard-string-builtin
  standard-stringp)
nth-atom-builtinfunction
(defun nth-atom-builtin
  (n)
  (declare (xargs :guard (natp n)))
  (b* (((mv choice seed) (weighted-switch-nat '(1 1 3 1 1 2 2 10 10 20 30)
         n)))
    (case choice
      (0 'nil)
      (1 't)
      (2 (nth-nat seed))
      (3 (nth-symbol seed))
      (4 (nth-string seed))
      (5 (nth-alpha-num-character seed))
      (6 (nth-acl2-number seed))
      (7 (nth-rational seed))
      (8 (nth-pos seed))
      (9 0)
      (t (nth-integer seed)))))
other
(register-custom-type atom
  t
  nth-atom-builtin
  atom)
other
(def-const *z-values* '(0 -1 "a" 1/3 :a))
nth-z-builtinfunction
(defun nth-z-builtin
  (n)
  (declare (xargs :guard (natp n)))
  (nth (mod n 5) *z-values*))
nth-z-uniform-builtinfunction
(defun nth-z-uniform-builtin
  (m seed)
  (declare (ignorable m))
  (declare (type (unsigned-byte 63) seed))
  (declare (xargs :guard (and (natp m)
        (unsigned-byte-p 63 seed))))
  (mv-let (n seed)
    (random-natural-seed seed)
    (mv (nth-z-builtin n)
      (the (unsigned-byte 63) seed))))
other
(register-type z
  :domain-size t
  :enumerator nth-z-builtin
  :predicate zp
  :enum/acc nth-z-uniform-builtin)
other
(defdata-subtype-strict neg
  non-pos-integer)
other
(defdata-subtype-strict neg
  non-0-integer)
other
(defdata-subtype-strict neg
  neg-rational)
other
(defdata-subtype-strict pos nat)
other
(defdata-subtype-strict pos
  non-0-integer)
other
(defdata-subtype-strict pos
  pos-rational)
other
(defdata-subtype-strict non-pos-integer
  integer)
other
(defdata-subtype-strict non-0-integer integer)
other
(defdata-subtype-strict nat integer)
other
(defdata-subtype-strict integer rational)
other
(defdata-subtype-strict neg-ratio
  non-pos-rational)
other
(defdata-subtype-strict pos-ratio
  non-neg-rational)
other
(defdata-subtype-strict ratio rational)
other
(defdata-subtype-strict neg-rational
  non-pos-rational)
other
(defdata-subtype-strict neg-rational
  non-0-rational)
other
(defdata-subtype-strict pos-rational
  non-neg-rational)
other
(defdata-subtype-strict pos-rational
  non-0-rational)
other
(defdata-subtype-strict non-neg-rational
  rational)
other
(defdata-subtype-strict non-pos-rational
  rational)
other
(defdata-subtype-strict non-0-rational
  rational)
other
(defdata-subtype-strict rational acl2-number)
other
(defdata-subtype-strict complex-rational
  acl2-number)
other
(defdata-subtype-strict acl2-number atom)
other
(defdata-subtype-strict non-pos-rational
  z)
other
(defdata-subtype-strict ratio z)
other
(defdata-subtype-strict complex-rational
  z)
other
(defdata-subtype-strict symbol z)
other
(defdata-subtype-strict character z)
other
(defdata-subtype-strict string z)
other
(defdata-disjoint-strict neg nat)
other
(defdata-disjoint-strict pos
  non-pos-integer)
other
(defdata-disjoint-strict integer ratio)
other
(defdata-disjoint-strict neg-ratio
  non-neg-rational)
other
(defdata-disjoint-strict pos-ratio
  non-pos-rational)
other
(defdata-disjoint-strict neg-rational
  non-neg-rational)
other
(defdata-disjoint-strict pos-rational
  non-pos-rational)
other
(defdata-disjoint-strict rational
  complex-rational)
other
(defdata-disjoint-strict pos z)
other
(defdata-subtype-strict boolean symbol)
other
(defdata-subtype-strict proper-symbol symbol)
other
(defdata-subtype-strict standard-char
  character
  :hints (("Goal" :in-theory (enable standard-char-p))))
other
(defdata-subtype-strict character atom)
other
(defdata-subtype-strict string atom)
other
(defdata-subtype-strict symbol atom)
other
(defdata-subtype-strict standard-string
  string)
other
(defdata-disjoint-strict acl2-number
  character)
other
(defdata-disjoint-strict acl2-number symbol)
other
(defdata-disjoint-strict character string)
other
(defdata-disjoint-strict character symbol)
other
(defdata-disjoint-strict string symbol)
other
(defdata-disjoint-strict boolean
  proper-symbol)
other
(defthm termination-tree-enum-cdr
  (implies (consp x)
    (and (< (acl2-count (cdr x))
        (acl2-count x))
      (< (acl2-count (car x))
        (acl2-count x)))))
other
(defthm termination-tree-enum-dec
  (implies (< (acl2-count x1)
      (acl2-count x2))
    (and (< (acl2-count (car x1))
        (acl2-count x2))
      (< (acl2-count (cdr x1))
        (acl2-count x2)))))
other
(defthm terminination-tree-enum-nth
  (<= (acl2-count (nth i x))
    (acl2-count x))
  :rule-classes (:rewrite :linear))
other
(defthm termination-tree-enum-dec2
  (implies (< (acl2-count x1)
      (acl2-count x2))
    (< (acl2-count (nth i x1))
      (acl2-count x2)))
  :hints (("Goal" :in-theory (disable nth))))
other
(defdata cons-atom (cons atom atom))
other
(defdata-disjoint-strict cons-atom atom)
other
(defdata cons-ca-ca
  (cons cons-atom cons-atom))
other
(defdata cons-cca-cca
  (cons cons-ca-ca cons-ca-ca))
nth-proper-cons-builtinfunction
(defun nth-proper-cons-builtin
  (n)
  (declare (xargs :mode :program))
  (b* (((mv choice seed) (weighted-switch-nat '(1 1 1 1 1 1 1 1 1) n)))
    (case choice
      (0 (list (nth-atom seed)))
      (1 (b* (((list i1 i2) (split-nat 2 seed)))
          (list (nth-atom i1)
            (nth-atom i2))))
      (2 (b* (((list i1 i2 i3) (split-nat 3 seed)))
          (list (nth-atom i1)
            (nth-atom i2)
            (nth-atom i3))))
      (3 (b* (((list i1 i2 i3) (split-nat 3 seed)))
          (list (nth-atom i1)
            (cons (nth-atom i2)
              (nth-atom i3)))))
      (4 (b* (((list i1 i2 i3 i4 i5) (split-nat 5 seed)))
          (list (nth-atom i1)
            (nth-atom i2)
            (nth-atom i3)
            (cons (nth-atom i4)
              (nth-atom i5)))))
      (5 (b* (((list i1
              i2
              i3
              i4
              i5
              i6) (split-nat 6 seed)))
          (list (nth-atom i1)
            (nth-atom i2)
            (cons (cons (nth-atom i3)
                (nth-atom i4))
              (cons (nth-atom i5)
                (nth-atom i6))))))
      (6 (b* (((list i1 i2 i3 i4 i5) (split-nat 5 seed)))
          (list (nth-cons-atom i1)
            (cons (cons (nth-cons-atom i2)
                (nth-cons-atom i3))
              (cons (nth-cons-atom i4)
                (nth-cons-atom i5))))))
      (7 (b* (((list i1 i2 i3 i4 i5) (split-nat 5 seed)))
          (list (nth-cons-atom i1)
            (cons (cons (nth-atom i2)
                (nth-atom i3))
              (cons (nth-atom i4)
                (nth-atom i5))))))
      (8 (b* (((list i1 i2 i3 i4 i5) (split-nat 5 seed)))
          (list (nth-atom i1)
            (nth-atom i2)
            (nth-atom i3)
            (nth-atom i4)
            (nth-atom i5))))
      (t '(1 2)))))
nth-proper-cons-uniform-builtinfunction
(defun nth-proper-cons-uniform-builtin
  (m seed.)
  (declare (xargs :mode :program))
  (declare (ignorable m)
    (type (unsigned-byte 63) seed.))
  (declare (xargs :guard (and (natp m)
        (unsigned-byte-p 63 seed.))))
  (b* (((mv n seed.) (random-natural-seed seed.)) ((mv choice n) (weighted-switch-nat '(1 1 1 1 1 1 1 1 1) n))
      ((mv (list i1
           i2
           i3
           i4
           i5
           i6)
         seed.) (random-natural-list-seed 6 seed.)))
    (case choice
      (0 (mv (list (nth-atom n)) seed.))
      (1 (mv (list (nth-atom i1)
            (nth-atom i2))
          seed.))
      (2 (mv (list (nth-atom i1)
            (nth-atom i2)
            (nth-atom i3))
          seed.))
      (3 (mv (list (nth-atom i1)
            (cons (nth-atom i2)
              (nth-atom i3)))
          seed.))
      (4 (mv (list (nth-atom i1)
            (nth-atom i2)
            (nth-atom i3)
            (cons (nth-atom i4)
              (nth-atom i5)))
          seed.))
      (5 (mv (list (nth-atom i1)
            (nth-atom i2)
            (cons (cons (nth-atom i3)
                (nth-atom i4))
              (cons (nth-atom i5)
                (nth-atom i6))))
          seed.))
      (6 (mv (list (nth-cons-atom i1)
            (cons (cons (nth-cons-atom i2)
                (nth-cons-atom i3))
              (cons (nth-cons-atom i4)
                (nth-cons-atom i5))))
          seed.))
      (7 (mv (list (nth-cons-atom i1)
            (cons (cons (nth-atom i2)
                (nth-atom i3))
              (cons (nth-atom i4)
                (nth-atom i5))))
          seed.))
      (8 (mv (list (nth-atom i1)
            (nth-atom i2)
            (nth-atom i3)
            (nth-atom i4)
            (nth-atom i5))
          seed.))
      (t (mv '(1 2) seed.)))))
other
(register-type proper-cons
  :domain-size t
  :enumerator nth-proper-cons-builtin
  :enum/acc nth-proper-cons-uniform-builtin
  :predicate proper-consp)
other
(defdata nat-list (listof nat))
other
(defdata non-empty-nat-list
  (cons nat nat-list))
other
(local (defthm non-empty-nat-list-thm
    (equal (non-empty-nat-listp x)
      (and (consp x) (nat-listp x)))
    :rule-classes ((:forward-chaining :trigger-terms ((non-empty-nat-listp x))))))
other
(defdata lex
  (oneof nat non-empty-nat-list))
other
(defdata pos-list (listof pos))
other
(defdata integer-list (listof integer))
other
(defdata rational-list
  (listof rational))
other
(defdata complex-rational-list
  (listof complex-rational))
other
(defdata acl2-number-list
  (listof acl2-number))
other
(defdata boolean-list (listof boolean))
other
(defdata symbol-list (listof symbol))
other
(defdata keyword-list (listof keyword))
other
(defdata proper-symbol-list
  (listof proper-symbol))
other
(register-type character-list
  :domain-size t
  :predicate character-listp
  :enumerator nth-character-list-builtin
  :prettyified-def (listof character))
other
(register-type standard-char-list
  :domain-size t
  :predicate standard-char-listp
  :enumerator nth-standard-char-list-builtin
  :prettyified-def (listof standard-char))
other
(defthm def=>standard-char-list
  (and (implies (and (equal v1 'nil))
      (standard-char-listp v1))
    (implies (and (standard-char-p v11)
        (standard-char-listp v12))
      (standard-char-listp (cons v11 v12))))
  :hints (("goal" :in-theory (e/d (standard-char-listp) (standard-char-p))))
  :rule-classes (:tau-system :rewrite))
other
(defthm standard-char-list=>def
  (and (implies (and (standard-char-listp v1)
        (endp v1))
      (equal v1 'nil))
    (implies (and (standard-char-listp v1)
        (consp v1))
      (and (standard-char-p (car v1))
        (standard-char-listp (cdr v1)))))
  :hints (("goal" :in-theory (e/d (standard-char-listp) (standard-char-p))))
  :rule-classes (:tau-system (:forward-chaining :trigger-terms ((standard-char-listp v1)))))
other
(defdata string-list (listof string))
other
(defdata atom-list (listof atom))
other
(defdata-subtype-strict pos-list
  nat-list)
other
(defdata-subtype-strict nat-list
  integer-list)
other
(defdata-subtype-strict integer-list
  rational-list)
other
(defdata-subtype-strict complex-rational-list
  acl2-number-list)
other
(defdata-subtype-strict rational-list
  acl2-number-list)
other
(defdata-subtype-strict acl2-number-list
  atom-list)
other
(defdata-subtype-strict boolean-list
  symbol-list)
other
(defdata-subtype-strict keyword-list
  symbol-list)
other
(defdata-subtype-strict standard-char-list
  character-list)
other
(defdata-subtype-strict character-list
  atom-list)
other
(defdata-subtype-strict string-list
  atom-list)
other
(defdata-subtype-strict symbol-list
  atom-list)
nth-all-builtinfunction
(defun nth-all-builtin
  (n)
  (declare (xargs :mode :program))
  (declare (xargs :guard (natp n)))
  (b* (((mv choice seed) (weighted-switch-nat '(1 1 1 1 1 1 1 1 2 1 1 5 5 5 2 20 5 10 1 10 5)
         n)))
    (case choice
      (0 'nil)
      (1 0)
      (2 't)
      (3 (nth-integer seed))
      (4 (nth-rational seed))
      (5 (nth-nat-list seed))
      (6 (nth-symbol seed))
      (7 (nth-string seed))
      (8 (nth-alpha-num-character seed))
      (9 (nth-acl2-number seed))
      (10 (nth-atom seed))
      (11 (b* (((list i1 i2) (split-nat 2 seed)))
          (list (nth-atom i1)
            (nth-atom i2))))
      (12 (nth-integer-list seed))
      (13 (nth-rational-list seed))
      (14 (nth-symbol-list seed))
      (15 (nth-cons-atom seed))
      (16 (nth-character-list seed))
      (17 (b* (((list i1 i2) (split-nat 2 seed)))
          (cons (nth-cons-atom i1)
            (nth-cons-atom i2))))
      (18 (nth-string-list seed))
      (19 (nth-atom-list seed))
      (20 (b* (((list i1 i2 i3 i4) (split-nat 4 seed)))
          (list (list (nth-atom i1)
              (nth-atom i2))
            (list (nth-atom i3)
              (nth-atom i4)))))
      (t 'nil))))
nth-all-uniform-builtinfunction
(defun nth-all-uniform-builtin
  (m seed)
  (declare (xargs :mode :program))
  (declare (type (unsigned-byte 63) seed))
  (declare (xargs :guard (and (natp m)
        (unsigned-byte-p 63 seed))))
  (b* (((mv n seed) (random-natural-seed seed)) ((mv choice ?rest) (weighted-switch-nat '(1 1 1 1 1 1 1 1 2 1 1 5 5 5 2 20 5 10 1 10)
          n)))
    (case choice
      (0 (mv 'nil seed))
      (1 (mv 0 seed))
      (2 (mv 't seed))
      (3 (nth-integer/acc m seed))
      (4 (nth-rational/acc m seed))
      (5 (nth-nat-list/acc m seed))
      (6 (nth-symbol/acc m seed))
      (7 (nth-string/acc m seed))
      (8 (mv (nth-alpha-num-character rest)
          seed))
      (9 (nth-acl2-number/acc m seed))
      (10 (mv (nth (mod rest 2) *boolean-values*)
          seed))
      (11 (nth-nat/acc m seed))
      (12 (nth-pos/acc m seed))
      (13 (nth-rational-list/acc m seed))
      (14 (nth-symbol-list/acc m seed))
      (15 (nth-cons-atom/acc m seed))
      (16 (nth-character-list/acc m seed))
      (17 (nth-cons-ca-ca/acc m seed))
      (18 (nth-string-list/acc m seed))
      (19 (nth-atom-list/acc m seed))
      (t (mv 'nil seed)))))
other
(register-type all
  :predicate allp
  :domain-size t
  :enumerator nth-all-builtin
  :enum/acc nth-all-uniform-builtin)
nth-quote-builtinfunction
(defun nth-quote-builtin
  (n)
  (declare (xargs :mode :program))
  (declare (xargs :guard (natp n)))
  `',(ACL2S::NTH-ALL-BUILTIN ACL2S::N))
nth-quote-uniform-builtinfunction
(defun nth-quote-uniform-builtin
  (m seed)
  (declare (xargs :mode :program))
  (declare (type (unsigned-byte 63) seed))
  (declare (xargs :guard (and (natp m)
        (unsigned-byte-p 63 seed))))
  (b* (((mv val seed) (nth-all-uniform-builtin m seed)))
    (mv `',ACL2S::VAL seed)))
other
(register-type quote
  :predicate rquotep
  :domain-size t
  :enumerator nth-quote-builtin
  :enum/acc nth-quote-uniform-builtin)
other
(def-const *empty-values* 'nil)
nth-emptyfunction
(defun nth-empty
  (x)
  (declare (ignore x)
    (xargs :guard (natp x)))
  (er hard?
    'nth-empty
    "~| Empty enumerator~%"))
nth-empty/accfunction
(defun nth-empty/acc
  (m seed)
  (declare (ignorable m seed))
  (mv (er hard?
      'nth-empty
      "~| Empty enumerator~%")
    seed))
emptypfunction
(defun emptyp
  (x)
  (declare (ignore x)
    (xargs :guard t))
  nil)
other
(defthm emptyp-is-tau-predicate
  (booleanp (emptyp x))
  :rule-classes :tau-system)
other
(table type-metadata-table
  'empty
  '((:predicate . emptyp) (:enumerator . nth-empty)
    (:domain-size . 0)
    (:enum/acc . nth-empty/acc)))
other
(defdata cons (cons all all))
other
(defdata acons
  (cons (cons all all) all))
acons-caarfunction
(defun acons-caar
  (x)
  (declare (xargs :guard (aconsp x)))
  (caar x))
acons-cdarfunction
(defun acons-cdar
  (x)
  (declare (xargs :guard (aconsp x)))
  (cdar x))
acons-cdrfunction
(defun acons-cdr
  (x)
  (declare (xargs :guard (aconsp x)))
  (cdr x))
other
(defthm acons-acl2-count-lemma
  (equal (acl2-count (acons x1 x2 x3))
    (+ 2
      (acl2-count x1)
      (acl2-count x2)
      (acl2-count x3))))
other
(in-theory (enable aconsp))
other
(register-data-constructor (aconsp acons)
  ((allp acons-caar) (allp acons-cdar)
    (allp acons-cdr))
  :rule-classes (:rewrite)
  :verbose t)
other
(defthm acons-alist-lemma
  (implies (alistp x)
    (alistp (acons x1 x2 x)))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))
other
(defdata list (oneof cons nil))
other
(defuns (nth-tl-builtin (x)
    (declare (xargs :mode :program))
    (declare (xargs :guard (natp x)
        :verify-guards nil
        :measure (nfix x)))
    (if (or (not (integerp x)) (< x 1))
      'nil
      (let ((x (- x 1)))
        (let ((infxlst (split-nat 2 x)))
          (cons (let ((x (nth 0 infxlst)))
              (nth-all x))
            (let ((x (nth 1 infxlst)))
              (nth-tl-builtin x))))))))
nth-tl/acc-builtinfunction
(defun nth-tl/acc-builtin
  (i1 seed.)
  (declare (type (unsigned-byte 63) seed.))
  (declare (xargs :mode :program :guard (and (natp i1)
        (unsigned-byte-p 63 seed.))))
  (b* (((mv _choice i1) (switch 2 i1)))
    (case _choice
      (0 (mv 'nil seed.))
      (1 (b* (((mv (list i1 i2) seed.) (random-index-list-seed 2 i1 seed.)) ((mv _v1 seed.) (nth-all/acc i1 seed.))
            ((mv _v2 seed.) (nth-tl/acc-builtin i2 seed.)))
          (mv (cons _v1 _v2) seed.)))
      (otherwise (mv nil seed.)))))
nth-true-list-builtinfunction
(defun nth-true-list-builtin
  (n)
  (declare (xargs :mode :program))
  (declare (xargs :guard (natp n)))
  (b* (((mv choice seed) (weighted-switch-nat '(10 2 20 1 10 1 1 5 10 5)
         n)))
    (case choice
      (0 (nth-integer-list seed))
      (1 (nth-rational-list seed))
      (2 (nth-nat-list seed))
      (3 'nil)
      (4 (nth-symbol-list seed))
      (5 (nth-string-list seed))
      (6 (nth-character-list seed))
      (7 (nth-acl2-number-list seed))
      (8 (nth-atom-list seed))
      (9 (nth-tl-builtin seed))
      (t 'nil))))
nth-true-list-uniform-builtinfunction
(defun nth-true-list-uniform-builtin
  (m seed)
  (declare (xargs :mode :program))
  (declare (type (unsigned-byte 63) seed))
  (declare (xargs :guard (and (natp m)
        (unsigned-byte-p 63 seed))))
  (b* (((mv n seed) (random-natural-seed seed)) ((mv choice ?rest) (weighted-switch-nat '(10 2 20 1 10 1 1 5 10 5)
          n)))
    (case choice
      (0 (nth-integer-list/acc m seed))
      (1 (nth-rational-list/acc m seed))
      (2 (nth-nat-list/acc m seed))
      (3 (mv 'nil seed))
      (4 (nth-symbol-list/acc m seed))
      (5 (nth-string-list/acc m seed))
      (6 (nth-character-list/acc m seed))
      (7 (nth-acl2-number-list/acc m seed))
      (8 (nth-atom-list/acc m seed))
      (9 (nth-tl/acc-builtin m seed))
      (t (mv 'nil seed)))))
other
(register-type true-list
  :domain-size t
  :predicate true-listp
  :enumerator nth-true-list-builtin
  :enum/acc nth-true-list-uniform-builtin
  :prettyified-def (listof all))
other
(defdata alist
  (listof (cons all all)))
other
(defdata symbol-alist
  (alistof symbol all))
other
(verify-termination character-alistp)
other
(defdata character-alist
  (alistof character all))
other
(defdata r-symbol-alist
  (alistof all symbol))
other
(defdata-subtype-strict symbol-alist
  alist)
other
(defdata-subtype-strict character-alist
  alist)
other
(defdata-subtype-strict r-symbol-alist
  alist)
other
(defdata true-list-list
  (listof true-list))
other
(defdata-subtype-strict true-list-list
  true-list)
other
(defdata-subtype-strict cons z)
other
(defdata-subtype-strict list z)
all-but-zero-nil-tpfunction
(defun all-but-zero-nil-tp
  (x)
  (declare (xargs :guard t))
  (and (not (equal x 0))
    (not (equal x 't))
    (not (equal x 'nil))))
nth-all-but-zero-nil-t-builtinfunction
(defun nth-all-but-zero-nil-t-builtin
  (n)
  (declare (xargs :mode :program))
  (declare (xargs :guard (natp n)))
  (b* (((mv choice seed) (weighted-switch-nat '(1 1 1 1 2 1 5 5 5 5 2 20 5 10 1 10)
         n)) (val (case choice
          (0 (nth-integer seed))
          (1 (nth-character-list seed))
          (2 (nth-symbol seed))
          (3 (nth-string seed))
          (4 (nth-character seed))
          (5 (nth-pos seed))
          (6 (nth-pos-ratio seed))
          (7 (nth-neg-ratio seed))
          (8 (nth-complex-rational seed))
          (9 (nth-rational-list seed))
          (10 (nth-symbol-list seed))
          (11 (nth-cons-atom seed))
          (12 (nth-nat-list seed))
          (13 (b* (((list i1 i2) (split-nat 2 seed)))
              (cons (nth-cons-atom i1)
                (nth-cons-atom i2))))
          (14 (nth-string-list seed))
          (15 (nth-atom-list seed))
          (t 1))))
    (if (all-but-zero-nil-tp val)
      val
      1)))
nth-all-but-zero-nil-t-uniform-builtinfunction
(defun nth-all-but-zero-nil-t-uniform-builtin
  (m seed.)
  (declare (xargs :mode :program))
  (declare (type (unsigned-byte 63) seed.))
  (declare (xargs :guard (and (natp m)
        (unsigned-byte-p 63 seed.))))
  (b* (((mv ans seed.) (nth-all-uniform-builtin m seed.)))
    (if (or (booleanp ans) (equal ans 0))
      (b* (((mv n seed.) (random-natural-seed seed.)))
        (mv (nth-all-but-zero-nil-t-builtin n)
          seed.))
      (mv ans seed.))))
other
(register-type all-but-zero-nil-t
  :domain-size t
  :enum/acc nth-all-but-zero-nil-t-uniform-builtin
  :enumerator nth-all-but-zero-nil-t-builtin
  :predicate all-but-zero-nil-tp)
all-but-nilpfunction
(defun all-but-nilp
  (x)
  (declare (xargs :guard t))
  (not (equal x 'nil)))
other
(register-data-constructor (recordp mset)
  ((allp caar) (allp cdar) (recordp cdr))
  :hints (("Goal" :in-theory (enable recordp
       no-nil-val-alistp
       ordered-unique-key-alistp)))
  :proper nil)
nth-all-but-nil-builtinfunction
(defun nth-all-but-nil-builtin
  (n)
  (declare (xargs :mode :program))
  (declare (xargs :guard (natp n)))
  (cond ((eql n 0) 0)
    ((eql n 12) t)
    (t (nth-all-but-zero-nil-t n))))
other
(register-custom-type all-but-nil
  t
  nth-all-but-nil-builtin
  all-but-nilp)
other
(defdata-subtype-strict all-but-zero-nil-t
  all)
other
(defdata-subtype-strict all-but-nil
  all)
other
(defdata-subtype-strict acons
  cons
  :hints (("Goal" :in-theory (enable aconsp))))
other
(defdata-subtype-strict cons all-but-nil)
other
(defdata-subtype-strict atom all)
other
(defdata-subtype-strict atom-list
  true-list)
other
(defdata-subtype-strict alist
  true-list)
other
(defdata-subtype-strict list all)
other
(defdata-subtype-strict true-list list)
other
(defdata cons-cccca-cccca
  (cons cons-cca-cca cons-cca-cca))
other
(defdata cons-a-ca
  (cons atom cons-atom))
other
(defdata cons-a-cca
  (cons atom cons-ca-ca))
other
(defdata cons-a-cccca
  (cons atom cons-cca-cca))
other
(defdata cons-ca-cca
  (cons cons-atom cons-ca-ca))
other
(defdata cons-ca-cccca
  (cons cons-atom cons-cca-cca))
other
(defdata cons-all-all-but-zero-nil-t
  (cons all all-but-zero-nil-t))
nth-improper-cons-builtinfunction
(defun nth-improper-cons-builtin
  (n)
  (declare (xargs :mode :program))
  (b* (((mv choice seed) (weighted-switch-nat '(1 1 1 1 1 1 1 1) n)))
    (case choice
      (0 (nth-cons-all-all-but-zero-nil-t seed))
      (1 (nth-cons-ca-ca seed))
      (2 (nth-cons-a-ca seed))
      (3 (nth-cons-a-cca seed))
      (4 (nth-cons-a-cccca seed))
      (5 (nth-cons-cccca-cccca seed))
      (6 (nth-cons-ca-cca seed))
      (7 (nth-cons-ca-cccca seed))
      (t '(1 . 2)))))
nth-improper-cons-uniform-builtinfunction
(defun nth-improper-cons-uniform-builtin
  (m seed)
  (declare (xargs :mode :program))
  (declare (type (unsigned-byte 63) seed))
  (declare (xargs :guard (and (natp m)
        (unsigned-byte-p 63 seed))))
  (b* (((mv n seed) (random-natural-seed seed)) ((mv choice ?rest) (weighted-switch-nat '(1 1 1 1 1 1 1 1) n)))
    (case choice
      (0 (nth-cons-all-all-but-zero-nil-t/acc m
          seed))
      (1 (nth-cons-ca-ca/acc m seed))
      (2 (nth-cons-a-ca/acc m seed))
      (3 (nth-cons-a-cca/acc m seed))
      (4 (nth-cons-a-cccca/acc m seed))
      (5 (nth-cons-cccca-cccca/acc m seed))
      (6 (nth-cons-ca-cca/acc m seed))
      (7 (nth-cons-ca-cccca/acc m seed))
      (t (mv '(1 . 2) seed)))))
other
(register-type improper-cons
  :domain-size t
  :enumerator nth-improper-cons-builtin
  :enum/acc nth-improper-cons-uniform-builtin
  :predicate improper-consp)
other
(defdata-subtype-strict improper-cons cons)
other
(defdata-subtype-strict proper-cons cons)
other
(defdata-subtype-strict proper-cons
  true-list)
other
(defdata-disjoint-strict proper-cons
  improper-cons)
other
(defdata-disjoint-strict atom cons)
nth-even-builtinfunction
(defun nth-even-builtin
  (n)
  (declare (xargs :verify-guards nil
      :guard (natp n)))
  (* 2 (nth-integer n)))
other
(register-type even
  :predicate evenp
  :enumerator nth-even-builtin)
nth-odd-builtinfunction
(defun nth-odd-builtin
  (n)
  (declare (xargs :verify-guards nil
      :guard (natp n)))
  (1+ (* 2 (nth-integer n))))
other
(register-type odd
  :predicate oddp
  :enumerator nth-odd-builtin)
other
(defdata-subtype-strict var symbol)
other
(in-theory (disable varp))
other
(defdata sym-aalist
  (listof (cons symbol symbol-alist)))
other
(defthm sym-aalist-sym-aalist1
  (equal (sym-aalist1p x)
    (sym-aalistp x)))
geometric-int-aroundfunction
(defun geometric-int-around
  (x n)
  (declare (xargs :guard (and (integerp x) (natp n))
      :verify-guards nil))
  (+ x (nth-integer n)))
geometric-rat-aroundfunction
(defun geometric-rat-around
  (x n)
  (declare (xargs :guard (and (rationalp x) (natp n))
      :verify-guards nil))
  (+ x (nth-rational n)))
geometric-int-leqfunction
(defun geometric-int-leq
  (x n)
  (declare (xargs :guard (and (integerp x) (natp n))
      :verify-guards nil))
  (- x (nth-nat n)))
geometric-rat-leqfunction
(defun geometric-rat-leq
  (x n)
  (declare (xargs :guard (and (rationalp x) (natp n))
      :verify-guards nil))
  (- x (nth-non-neg-rational n)))
geometric-int-geqfunction
(defun geometric-int-geq
  (x n)
  (declare (xargs :guard (and (integerp x) (natp n))
      :verify-guards nil))
  (+ x (nth-nat n)))
geometric-rat-geqfunction
(defun geometric-rat-geq
  (x n)
  (declare (xargs :guard (and (rationalp x) (natp n))
      :verify-guards nil))
  (+ x (nth-non-neg-rational n)))
geometric-int-around-bndfunction
(defun geometric-int-around-bnd
  (x lo hi n)
  (declare (xargs :guard (and (integerp x) (natp n))
      :verify-guards nil))
  (b* ((res (+ x (nth-integer n))) (res (max lo res))
      (res (min hi res)))
    res))
geometric-rat-around-bndfunction
(defun geometric-rat-around-bnd
  (x lo hi n)
  (declare (xargs :guard (and (rationalp x) (natp n))
      :verify-guards nil))
  (b* ((res (+ x (nth-rational n))) (res (max lo res))
      (res (min hi res)))
    res))
geometric-int-leq-bndfunction
(defun geometric-int-leq-bnd
  (x lo n)
  (declare (xargs :guard (and (integerp x) (natp n))
      :verify-guards nil))
  (b* ((res (- x (nth-nat n))) (res (max lo res)))
    res))
geometric-rat-leq-bndfunction
(defun geometric-rat-leq-bnd
  (x lo n)
  (declare (xargs :guard (and (rationalp x) (natp n))
      :verify-guards nil))
  (b* ((res (- x (nth-non-neg-rational n))) (res (max lo res)))
    res))
geometric-int-geq-bndfunction
(defun geometric-int-geq-bnd
  (x hi n)
  (declare (xargs :guard (and (integerp x) (natp n))
      :verify-guards nil))
  (b* ((res (+ x (nth-nat n))) (res (min hi res)))
    res))
geometric-rat-geq-bndfunction
(defun geometric-rat-geq-bnd
  (x hi n)
  (declare (xargs :guard (and (rationalp x) (natp n))
      :verify-guards nil))
  (b* ((res (+ x (nth-non-neg-rational n))) (res (min hi res)))
    res))
geometric-int-betweenfunction
(defun geometric-int-between
  (lo hi n)
  (declare (xargs :guard (and (integerp lo)
        (integerp hi)
        (natp n)
        (<= lo hi))
      :verify-guards nil))
  (b* ((mid (floor (+ lo hi) 2)) (x (nth-integer n))
      (res (+ mid x))
      (res (max lo res))
      (res (min hi res)))
    res))
geometric-rat-betweenfunction
(defun geometric-rat-between
  (lo hi n)
  (declare (xargs :guard (and (rationalp lo)
        (rationalp hi)
        (natp n)
        (<= lo hi))
      :verify-guards nil))
  (b* ((mid (/ (+ lo hi) 2)) (x (nth-rational n))
      (res (+ mid x))
      (res (max lo res))
      (res (min hi res)))
    res))
other
(defthm eqlable-keyword-listp
  (implies (keyword-listp keywords)
    (eqlable-listp keywords)))