• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
        • Omaps
        • Directed-untranslate
        • Include-book-paths
        • Ubi
        • Numbered-names
        • Digits-any-base
          • Defdigits
            • Defdigits-implementation
              • Defdigits-fn
              • Defdigits-infop
              • Defdigits-macro-definition
              • Defdigits-table
              • *defdigits-table-name*
          • Nat=>lendian*
          • Group-lendian
          • Defdigit-grouping
          • Ungroup-lendian
          • Lendian=>nat
          • Defthm-dab-return-types
          • Bendian=>nat
          • Nat=>bendian*
          • Trim-bendian*
          • Trim-lendian*
          • Nat=>lendian
          • Dab-digit-list-fix
          • Nat=>bendian
          • Ungroup-bendian
          • Group-bendian
          • Digits=>nat-injectivity-theorems
          • Dab-digit-listp
          • Nat=>lendian+
          • Dab-basep
          • Nat=>bendian+
          • Digits=>nat=>digits-inverses-theorems
          • Trim-lendian+
          • Trim-bendian+
          • Nat=>digits=>nat-inverses-theorems
          • Dab-digitp
          • Group/ungroup-inverses-theorems
          • Dab-digit-fix
          • Nat=>digits-injectivity-theorems
          • Dab-base
          • Digits-any-base-pow2
          • Dab-base-fix
        • Context-message-pair
        • With-auto-termination
        • Make-termination-theorem
        • Theorems-about-true-list-lists
        • Checkpoint-list
        • Sublis-expr+
        • Integers-from-to
        • Prove$
        • Defthm<w
        • System-utilities-non-built-in
        • Integer-range-fix
        • Minimize-ruler-extenders
        • Add-const-to-untranslate-preprocess
        • Unsigned-byte-fix
        • Signed-byte-fix
        • Defthmr
        • Paired-names
        • Unsigned-byte-list-fix
        • Signed-byte-list-fix
        • Show-books
        • Skip-in-book
        • Typed-tuplep
        • List-utilities
        • Checkpoint-list-pretty
        • Defunt
        • Keyword-value-list-to-alist
        • Magic-macroexpand
        • Top-command-number-fn
        • Bits-as-digits-in-base-2
        • Show-checkpoint-list
        • Ubyte11s-as-digits-in-base-2048
        • Named-formulas
        • Bytes-as-digits-in-base-256
        • String-utilities
        • Make-keyword-value-list-from-keys-and-value
        • Defmacroq
        • Integer-range-listp
        • Apply-fn-if-known
        • Trans-eval-error-triple
        • Checkpoint-info-list
        • Previous-subsumer-hints
        • Fms!-lst
        • Zp-listp
        • Trans-eval-state
        • Injections
        • Doublets-to-alist
        • Theorems-about-osets
        • Typed-list-utilities
        • Book-runes-alist
        • User-interface
        • Bits/ubyte11s-digit-grouping
        • Bits/bytes-digit-grouping
        • Message-utilities
        • Subsetp-eq-linear
        • Oset-utilities
        • Strict-merge-sort-<
        • Miscellaneous-enumerations
        • Maybe-unquote
        • Thm<w
        • Defthmd<w
        • Io-utilities
      • Set
      • Soft
      • C
      • Bv
      • Imp-language
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Lists-light
      • Axe
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Defdigits-implementation

Defdigits-fn

Event generated by defdigits.

Signature

(defdigits-fn name base digit-pred digit-fix 
              digits-pred digits-fix bendian-to-nat 
              lendian-to-nat nat-to-bendian 
              nat-to-lendian digit-pred-hints 
              digit-fix-hints digit-pred-guard-hints 
              digit-fix-guard-hints digits-pred-hints 
              digits-fix-hints digits-pred-guard-hints 
              digits-fix-guard-hints 
              digits-description 
              parents short long wrld) 
 
  → 
event

Arguments

wrld — Guard (plist-worldp wrld).

Returns

event — A maybe-pseudo-event-formp.

Definitions and Theorems

Function: defdigits-fn

(defun defdigits-fn (name base digit-pred digit-fix
                          digits-pred digits-fix bendian-to-nat
                          lendian-to-nat nat-to-bendian
                          nat-to-lendian digit-pred-hints
                          digit-fix-hints digit-pred-guard-hints
                          digit-fix-guard-hints digits-pred-hints
                          digits-fix-hints digits-pred-guard-hints
                          digits-fix-guard-hints
                          digits-description
                          parents short long wrld)
 (declare (xargs :guard (plist-worldp wrld)))
 (let ((__function__ 'defdigits-fn))
  (declare (ignorable __function__))
  (b*
   (((unless (symbolp name))
     (raise
      "The NAME input must be a symbol, ~
                but it is ~x0 instead."
      name))
    ((unless (dab-basep base))
     (raise
      "The :BASE input must be an integer greater than 1, ~
                but it is ~x0 instead."
      base))
    ((unless (symbolp digit-pred))
     (raise
      "The :DIGIT-PRED input must be a symbol, ~
                but it is ~x0 instead."
      digit-pred))
    ((unless (or (getpropc digit-pred 'macro-args
                           nil wrld)
                 (function-symbolp digit-pred wrld)))
     (raise
      "The symbol ~x0 must name an existing function, ~
                or a macro for an inline function, ~
                but it does not."
      digit-pred))
    ((unless (symbolp digit-fix))
     (raise
      "The :DIGIT-FIX input must be a symbol, ~
                but it is ~x0 instead."
      digit-fix))
    ((unless (or (getpropc digit-fix 'macro-args
                           nil wrld)
                 (function-symbolp digit-fix wrld)))
     (raise
      "The symbol ~x0 must name an existing function, ~
                or a macro for an inline function, ~
                but it does not."
      digit-fix))
    ((unless (symbolp digits-pred))
     (raise
      "The :DIGITS-PRED input must be a symbol, ~
                 but it is ~x0 instead."
      digits-pred))
    ((unless (or (getpropc digits-pred 'macro-args
                           nil wrld)
                 (function-symbolp digits-pred wrld)))
     (raise
      "The symbol ~x0 must name an existing function, ~
                or a macro for an inline function, ~
                but it does not."
      digits-pred))
    ((unless (symbolp digits-fix))
     (raise
      "The :DIGITS-FIX input must be a symbol, ~
                 but it is ~x0 instead."
      digits-fix))
    ((unless (or (getpropc digits-fix 'macro-args
                           nil wrld)
                 (function-symbolp digits-fix wrld)))
     (raise
      "The symbol ~x0 must name an existing function, ~
                or a macro for an inline function, ~
                but it does not."
      digits-fix))
    ((unless (symbolp bendian-to-nat))
     (raise
      "The :BENDIAN-TO-NAT input must be a symbol, ~
                 but it is ~x0 instead."
      bendian-to-nat))
    ((unless (symbolp lendian-to-nat))
     (raise
      "The :LENDIAN-TO-NAT input must be a symbol, ~
                 but it is ~x0 instead."
      lendian-to-nat))
    ((unless (symbolp nat-to-bendian))
     (raise
      "The :NAT-TO-BENDIAN input must be a symbol, ~
                 but it is ~x0 instead."
      nat-to-bendian))
    ((unless (symbolp nat-to-lendian))
     (raise
      "The :NAT-TO-LENDIAN input must be a symbol, ~
                 but it is ~x0 instead."
      nat-to-lendian))
    ((unless (stringp digits-description))
     (raise
      "The :DIGITS-DESCRIPTION input must be a string, ~
                but it is ~x0 instead."
      digits-description))
    (nat-to-bendian* (add-suffix-to-fn nat-to-bendian "*"))
    (nat-to-lendian* (add-suffix-to-fn nat-to-lendian "*"))
    (nat-to-bendian+ (add-suffix-to-fn nat-to-bendian "+"))
    (nat-to-lendian+ (add-suffix-to-fn nat-to-lendian "+"))
    (digit-pred-correct
         (packn-pos (list digit-pred '-is-dab-digitp-of-
                          base)
                    name))
    (digit-fix-correct
         (packn-pos (list digit-fix '-is-dab-digit-fix-of-
                          base)
                    name))
    (digit-pred-guard-correct
         (packn-pos (list digit-pred '-guard-is-t)
                    name))
    (digit-fix-guard-correct
         (packn-pos (list digit-fix '-guard-is-dab-digitp-of-
                          base)
                    name))
    (digits-pred-correct
         (packn-pos (list digits-pred '-is-dab-digit-listp-of-
                          base)
                    name))
    (digits-fix-correct
         (packn-pos (list digits-fix '-is-dab-digit-list-fix-of-
                          base)
                    name))
    (digits-pred-guard-correct
         (packn-pos (list digits-pred '-guard-is-t)
                    name))
    (digits-fix-guard-correct
         (packn-pos (list digits-fix
                          '-guard-is-dab-digit-listp-of-
                          base)
                    name))
    (len-of-nat-to-bendian (packn-pos (list 'len-of- nat-to-bendian)
                                      nat-to-bendian))
    (len-of-nat-to-lendian (packn-pos (list 'len-of- nat-to-lendian)
                                      nat-to-lendian))
    (bendian-to-nat-of-nat-to-bendian
         (packn-pos (list bendian-to-nat '-of-
                          nat-to-bendian)
                    name))
    (lendian-to-nat-of-nat-to-lendian
         (packn-pos (list lendian-to-nat '-of-
                          nat-to-lendian)
                    name))
    (bendian-to-nat-of-nat-to-bendian*
         (packn-pos (list bendian-to-nat '-of-
                          nat-to-bendian*)
                    name))
    (lendian-to-nat-of-nat-to-lendian*
         (packn-pos (list lendian-to-nat '-of-
                          nat-to-lendian*)
                    name))
    (bendian-to-nat-of-nat-to-bendian+
         (packn-pos (list bendian-to-nat '-of-
                          nat-to-bendian+)
                    name))
    (lendian-to-nat-of-nat-to-lendian+
         (packn-pos (list lendian-to-nat '-of-
                          nat-to-lendian+)
                    name))
    (nat-to-bendian-injectivity
         (add-suffix-to-fn nat-to-bendian "-INJECTIVITY"))
    (nat-to-lendian-injectivity
         (add-suffix-to-fn nat-to-lendian "-INJECTIVITY"))
    (nat-to-bendian*-injectivity
         (add-suffix-to-fn nat-to-bendian* "-INJECTIVITY"))
    (nat-to-lendian*-injectivity
         (add-suffix-to-fn nat-to-lendian* "-INJECTIVITY"))
    (nat-to-bendian+-injectivity
         (add-suffix-to-fn nat-to-bendian+ "-INJECTIVITY"))
    (nat-to-lendian+-injectivity
         (add-suffix-to-fn nat-to-lendian+ "-INJECTIVITY"))
    (nat-to-bendian-of-bendian-to-nat
         (packn-pos (list nat-to-bendian '-of-
                          bendian-to-nat)
                    name))
    (nat-to-lendian-of-lendian-to-nat
         (packn-pos (list nat-to-lendian '-of-
                          lendian-to-nat)
                    name))
    (nat-to-bendian*-of-bendian-to-nat
         (packn-pos (list nat-to-bendian* '-of-
                          bendian-to-nat)
                    name))
    (nat-to-lendian*-of-lendian-to-nat
         (packn-pos (list nat-to-lendian* '-of-
                          lendian-to-nat)
                    name))
    (nat-to-bendian+-of-bendian-to-nat
         (packn-pos (list nat-to-bendian+ '-of-
                          bendian-to-nat)
                    name))
    (nat-to-lendian+-of-lendian-to-nat
         (packn-pos (list nat-to-lendian+ '-of-
                          lendian-to-nat)
                    name))
    (bendian-to-nat-injectivity
         (add-suffix-to-fn bendian-to-nat "-INJECTIVITY"))
    (lendian-to-nat-injectivity
         (add-suffix-to-fn lendian-to-nat "-INJECTIVITY"))
    (bendian-to-nat-injectivity*
         (add-suffix-to-fn bendian-to-nat "-INJECTIVITY*"))
    (lendian-to-nat-injectivity*
         (add-suffix-to-fn lendian-to-nat "-INJECTIVITY*"))
    (bendian-to-nat-injectivity+
         (add-suffix-to-fn bendian-to-nat "-INJECTIVITY+"))
    (lendian-to-nat-injectivity+
         (add-suffix-to-fn lendian-to-nat "-INJECTIVITY+"))
    (len-of-nat-to-bendian*-leq-width
         (packn-pos (list 'len-of-
                          nat-to-bendian* '-leq-width)
                    name))
    (len-of-nat-to-lendian*-leq-width
         (packn-pos (list 'len-of-
                          nat-to-lendian* '-leq-width)
                    name))
    (len-0-of-nat-to-bendian*
         (packn-pos (list 'len-0-of- nat-to-bendian*)
                    name))
    (len-0-of-nat-to-lendian*
         (packn-pos (list 'len-0-of- nat-to-lendian*)
                    name))
    (consp-pf-nat-to-bendian*-iff-not-zp
         (packn-pos (list 'consp-of-
                          nat-to-bendian* '-iff-not-zp)
                    name))
    (consp-pf-nat-to-lendian*-iff-not-zp
         (packn-pos (list 'consp-of-
                          nat-to-lendian* '-iff-not-zp)
                    name))
    (trim-bendian*-of-nat-to-bendian*
         (packn-pos (list 'trim-bendian*-of nat-to-bendian*)
                    name))
    (trim-lendian*-of-nat-to-lendian*
         (packn-pos (list 'trim-lendian*-of nat-to-lendian*)
                    name))
    (bendian-to-nat-of-cons
         (add-suffix-to-fn bendian-to-nat "-OF-CONS"))
    (lendian-to-nat-of-cons
         (add-suffix-to-fn lendian-to-nat "-OF-CONS"))
    (bendian-to-nat-of-append
         (add-suffix-to-fn bendian-to-nat "-OF-APPEND"))
    (lendian-to-nat-of-append
         (add-suffix-to-fn lendian-to-nat "-OF-APPEND"))
    (bendian-to-nat-of-all-zeros
         (packn-pos (list bendian-to-nat '-of-all-zero-constant)
                    name))
    (lendian-to-nat-of-all-zeros
         (packn-pos (list lendian-to-nat '-of-all-zero-constant)
                    name))
    (bendian-to-nat-upper-bound
         (add-suffix-to-fn bendian-to-nat "-UPPER-BOUND"))
    (lendian-to-nat-upper-bound
         (add-suffix-to-fn lendian-to-nat "-UPPER-BOUND"))
    (lendian-to-nat-as-bendian-to-nat
         (packn-pos (list lendian-to-nat '-as-
                          bendian-to-nat)
                    name))
    (bendian-to-nat-as-lendian-to-nat
         (packn-pos (list bendian-to-nat '-as-
                          lendian-to-nat)
                    name))
    (lendian-to-nat-of-rev
         (add-suffix-to-fn lendian-to-nat "-OF-REV"))
    (bendian-to-nat-of-rev
         (add-suffix-to-fn bendian-to-nat "-OF-REV"))
    (x (packn-pos (list "X") name))
    (digits (packn-pos (list "DIGITS") name))
    (digits1 (packn-pos (list "DIGITS1") name))
    (digits2 (packn-pos (list "DIGITS2") name))
    (hidigit (packn-pos (list "HIDIGIT") name))
    (lodigit (packn-pos (list "LODIGIT") name))
    (hidigits (packn-pos (list "HIDIGITS") name))
    (lodigits (packn-pos (list "LODIGITS") name))
    (nat (packn-pos (list "NAT") name))
    (nat1 (packn-pos (list "NAT1") name))
    (nat2 (packn-pos (list "NAT2") name))
    (width (packn-pos (list "WIDTH") name))
    (n (packn-pos (list "N") name))
    (base-string (coerce (explode-nonnegative-integer base 10 nil)
                         'string))
    (digit-pred-correct-event
     (cons
      'defruled
      (cons digit-pred-correct
            (cons (cons 'equal
                        (cons (cons digit-pred (cons x 'nil))
                              (cons (cons 'dab-digitp
                                          (cons base (cons x 'nil)))
                                    'nil)))
                  (and digit-pred-hints
                       (list :hints digit-pred-hints))))))
    (digit-fix-correct-event
     (cons
      'defruled
      (cons digit-fix-correct
            (cons (cons 'equal
                        (cons (cons digit-fix (cons x 'nil))
                              (cons (cons 'dab-digit-fix
                                          (cons base (cons x 'nil)))
                                    'nil)))
                  (and digit-fix-hints
                       (list :hints digit-fix-hints))))))
    (digit-pred-guard-correct-event
     (b* ((fn (if (function-symbolp digit-pred wrld)
                  digit-pred
                (add-suffix-to-fn digit-pred "$INLINE"))))
      (cons
       'defrule
       (cons
        digit-pred-guard-correct
        (cons
         (guard fn nil wrld)
         (cons
             ':rule-classes
             (cons 'nil
                   (and digit-pred-guard-hints
                        (list :hints digit-pred-guard-hints)))))))))
    (digit-fix-guard-correct-event
     (b* ((fn (if (function-symbolp digit-fix wrld)
                  digit-fix
                (add-suffix-to-fn digit-fix "$INLINE"))))
      (cons
       'defrule
       (cons
        digit-fix-guard-correct
        (cons
         (cons 'implies
               (cons (cons digit-pred
                           (cons (car (formals fn wrld)) 'nil))
                     (cons (guard fn nil wrld) 'nil)))
         (cons
              ':rule-classes
              (cons 'nil
                    (and digit-fix-guard-hints
                         (list :hints digit-fix-guard-hints)))))))))
    (digits-pred-correct-event
     (cons
      'defruled
      (cons digits-pred-correct
            (cons (cons 'equal
                        (cons (cons digits-pred (cons x 'nil))
                              (cons (cons 'dab-digit-listp
                                          (cons base (cons x 'nil)))
                                    'nil)))
                  (and digits-pred-hints
                       (list :hints digits-pred-hints))))))
    (digits-fix-correct-event
     (cons
      'defruled
      (cons digits-fix-correct
            (cons (cons 'equal
                        (cons (cons digits-fix (cons x 'nil))
                              (cons (cons 'dab-digit-list-fix
                                          (cons base (cons x 'nil)))
                                    'nil)))
                  (and digits-fix-hints
                       (list :hints digits-fix-hints))))))
    (digits-pred-guard-correct-event
     (b* ((fn (if (function-symbolp digits-pred wrld)
                  digits-pred
                (add-suffix-to-fn digits-pred "$INLINE"))))
      (cons
       'defrule
       (cons
        digits-pred-guard-correct
        (cons
         (guard fn nil wrld)
         (cons
            ':rule-classes
            (cons 'nil
                  (and digits-pred-guard-hints
                       (list :hints digits-pred-guard-hints)))))))))
    (digits-fix-guard-correct-event
     (b* ((fn (if (function-symbolp digits-fix wrld)
                  digits-fix
                (add-suffix-to-fn digits-fix "$INLINE"))))
      (cons
       'defrule
       (cons
        digits-fix-guard-correct
        (cons
         (cons 'implies
               (cons (cons digits-pred
                           (cons (car (formals fn wrld)) 'nil))
                     (cons (guard fn nil wrld) 'nil)))
         (cons
             ':rule-classes
             (cons 'nil
                   (and digits-fix-guard-hints
                        (list :hints digits-fix-guard-hints)))))))))
    (bendian-to-nat-event
     (cons
      'define
      (cons
       bendian-to-nat
       (cons
        (cons (cons digits (cons digits-pred 'nil))
              'nil)
        (cons
         ':returns
         (cons
          (cons
           nat
           (cons
            'natp
            (cons
             ':hints
             (cons
              (cons
               (cons
                '"Goal"
                (cons
                 ':in-theory
                 (cons (cons 'quote
                             (cons (cons 'natp-of-bendian=>nat
                                         (cons bendian-to-nat 'nil))
                                   'nil))
                       'nil)))
               'nil)
              'nil))))
          (cons
           ':parents
           (cons
            (cons name 'nil)
            (cons
             ':short
             (cons
              (cons
               'xdoc::topstring
               (cons
                '"Convert a big-endian list of "
                (cons
                 digits-description
                 (cons '", seen as digits in base "
                       (cons base-string '(", to their value."))))))
              (cons
               (cons 'bendian=>nat
                     (cons base (cons digits 'nil)))
               (cons
                ':guard-hints
                (cons
                 (cons
                  (cons
                   '"Goal"
                   (cons
                    ':in-theory
                    (cons
                     (cons
                      'quote
                      (cons
                        (cons digits-pred-correct '((:e dab-basep)))
                        'nil))
                     'nil)))
                  'nil)
                 (cons
                  '///
                  (cons
                   (cons
                    'fty::deffixequiv
                    (cons
                     bendian-to-nat
                     (cons
                      ':hints
                      (cons
                       (cons
                        (cons
                         '"Goal"
                         (cons
                          ':in-theory
                          (cons
                              (cons 'quote
                                    (cons (cons digits-fix-correct
                                                (cons bendian-to-nat
                                                      '(bendian=>nat-of-dab-digit-list-fix-digits)))
                                          'nil))
                              'nil)))
                        'nil)
                       'nil))))
                   'nil)))))))))))))))
    (lendian-to-nat-event
     (cons
      'define
      (cons
       lendian-to-nat
       (cons
        (cons (cons digits (cons digits-pred 'nil))
              'nil)
        (cons
         ':returns
         (cons
          (cons
           nat
           (cons
            'natp
            (cons
             ':hints
             (cons
              (cons
               (cons
                '"Goal"
                (cons
                 ':in-theory
                 (cons (cons 'quote
                             (cons (cons 'natp-of-lendian=>nat
                                         (cons lendian-to-nat 'nil))
                                   'nil))
                       'nil)))
               'nil)
              'nil))))
          (cons
           ':parents
           (cons
            (cons name 'nil)
            (cons
             ':short
             (cons
              (cons
               'xdoc::topstring
               (cons
                '"Convert a little-endian list of "
                (cons
                 digits-description
                 (cons '", seen as digits in base "
                       (cons base-string '(", to their value."))))))
              (cons
               (cons 'lendian=>nat
                     (cons base (cons digits 'nil)))
               (cons
                ':guard-hints
                (cons
                 (cons
                  (cons
                   '"Goal"
                   (cons
                    ':in-theory
                    (cons
                     (cons
                      'quote
                      (cons
                        (cons digits-pred-correct '((:e dab-basep)))
                        'nil))
                     'nil)))
                  'nil)
                 (cons
                  '///
                  (cons
                   (cons
                    'fty::deffixequiv
                    (cons
                     lendian-to-nat
                     (cons
                      ':hints
                      (cons
                       (cons
                        (cons
                         '"Goal"
                         (cons
                          ':in-theory
                          (cons
                              (cons 'quote
                                    (cons (cons digits-fix-correct
                                                (cons lendian-to-nat
                                                      '(lendian=>nat-of-dab-digit-list-fix-digits)))
                                          'nil))
                              'nil)))
                        'nil)
                       'nil))))
                   'nil)))))))))))))))
    (nat-to-bendian-event
     (cons
      'define
      (cons
       nat-to-bendian
       (cons
        (cons (cons width '(natp))
              (cons (cons nat '(natp)) 'nil))
        (cons
         ':guard
         (cons
          (cons '<
                (cons nat
                      (cons (cons 'expt
                                  (cons base (cons width 'nil)))
                            'nil)))
          (cons
           ':returns
           (cons
            (cons
             digits
             (cons
              digits-pred
              (cons
               ':hints
               (cons
                (cons
                 (cons
                  '"Goal"
                  (cons
                   ':in-theory
                   (cons
                    (cons
                     'quote
                     (cons
                        (cons digits-pred-correct
                              (cons nat-to-bendian
                                    '(return-type-of-nat=>bendian)))
                        'nil))
                    'nil)))
                 'nil)
                'nil))))
            (cons
             ':parents
             (cons
              (cons name 'nil)
              (cons
               ':short
               (cons
                (cons
                 'xdoc::topstring
                 (cons
                  '"Convert a natural number to its big-endian list of "
                  (cons digits-description
                        (cons '", seen as digits in base "
                              (cons base-string
                                    '(", of specified length."))))))
                (cons
                 (cons 'nat=>bendian
                       (cons base (cons width (cons nat 'nil))))
                 (cons
                  ':guard-hints
                  (cons
                   '(("Goal" :in-theory '((:e dab-basep))))
                   (cons
                    '///
                    (cons
                     (cons
                      'fty::deffixequiv
                      (cons
                       nat-to-bendian
                       (cons
                        ':hints
                        (cons
                         (cons
                          (cons
                           '"Goal"
                           (cons
                            ':in-theory
                            (cons
                             (cons
                              'quote
                              (cons
                               (cons
                                  'nat=>bendian-of-nfix-width
                                  (cons 'nat=>bendian-of-nfix-nat
                                        (cons nat-to-bendian 'nil)))
                               'nil))
                             'nil)))
                          'nil)
                         'nil))))
                     (cons
                      (cons
                       'defrule
                       (cons
                        len-of-nat-to-bendian
                        (cons
                         (cons
                          'equal
                          (cons
                           (cons
                            'len
                            (cons
                                 (cons nat-to-bendian
                                       (cons width (cons nat 'nil)))
                                 'nil))
                           (cons (cons 'nfix (cons width 'nil))
                                 'nil)))
                         (cons
                          ':in-theory
                          (cons
                           (cons
                             'quote
                             (cons (cons 'len-of-nat=>bendian
                                         (cons nat-to-bendian 'nil))
                                   'nil))
                           'nil)))))
                      'nil))))))))))))))))))
    (nat-to-lendian-event
     (cons
      'define
      (cons
       nat-to-lendian
       (cons
        (cons (cons width '(natp))
              (cons (cons nat '(natp)) 'nil))
        (cons
         ':guard
         (cons
          (cons '<
                (cons nat
                      (cons (cons 'expt
                                  (cons base (cons width 'nil)))
                            'nil)))
          (cons
           ':returns
           (cons
            (cons
             digits
             (cons
              digits-pred
              (cons
               ':hints
               (cons
                (cons
                 (cons
                  '"Goal"
                  (cons
                   ':in-theory
                   (cons
                    (cons
                     'quote
                     (cons
                        (cons digits-pred-correct
                              (cons nat-to-lendian
                                    '(return-type-of-nat=>lendian)))
                        'nil))
                    'nil)))
                 'nil)
                'nil))))
            (cons
             ':parents
             (cons
              (cons name 'nil)
              (cons
               ':short
               (cons
                (cons
                 'xdoc::topstring
                 (cons
                  '"Convert a natural number to its little-endian list of "
                  (cons digits-description
                        (cons '", seen as digits in base "
                              (cons base-string
                                    '(", of specified length."))))))
                (cons
                 (cons 'nat=>lendian
                       (cons base (cons width (cons nat 'nil))))
                 (cons
                  ':guard-hints
                  (cons
                   '(("Goal" :in-theory '((:e dab-basep))))
                   (cons
                    '///
                    (cons
                     (cons
                      'fty::deffixequiv
                      (cons
                       nat-to-lendian
                       (cons
                        ':hints
                        (cons
                         (cons
                          (cons
                           '"Goal"
                           (cons
                            ':in-theory
                            (cons
                             (cons
                              'quote
                              (cons
                               (cons
                                  'nat=>lendian-of-nfix-width
                                  (cons 'nat=>lendian-of-nfix-nat
                                        (cons nat-to-lendian 'nil)))
                               'nil))
                             'nil)))
                          'nil)
                         'nil))))
                     (cons
                      (cons
                       'defrule
                       (cons
                        len-of-nat-to-lendian
                        (cons
                         (cons
                          'equal
                          (cons
                           (cons
                            'len
                            (cons
                                 (cons nat-to-lendian
                                       (cons width (cons nat 'nil)))
                                 'nil))
                           (cons (cons 'nfix (cons width 'nil))
                                 'nil)))
                         (cons
                          ':in-theory
                          (cons
                           (cons
                             'quote
                             (cons (cons 'len-of-nat=>lendian
                                         (cons nat-to-lendian 'nil))
                                   'nil))
                           'nil)))))
                      'nil))))))))))))))))))
    (nat-to-bendian*-event
     (cons
      'define
      (cons
       nat-to-bendian*
       (cons
        (cons (cons nat '(natp)) 'nil)
        (cons
         ':returns
         (cons
          (cons
           digits
           (cons
            digits-pred
            (cons
             ':hints
             (cons
              (cons
               (cons
                '"Goal"
                (cons
                 ':in-theory
                 (cons
                  (cons
                   'quote
                   (cons
                       (cons digits-pred-correct
                             (cons nat-to-bendian*
                                   '(return-type-of-nat=>bendian*)))
                       'nil))
                  'nil)))
               'nil)
              'nil))))
          (cons
           ':parents
           (cons
            (cons name 'nil)
            (cons
             ':short
             (cons
              (cons
               'xdoc::topstring
               (cons
                    '"Convert a natural number to "
                    (cons '"its minimum-length big-endian list of "
                          (cons digits-description
                                (cons '", seen as sigits in base "
                                      (cons base-string '(".")))))))
              (cons
               (cons 'nat=>bendian*
                     (cons base (cons nat 'nil)))
               (cons
                ':guard-hints
                (cons
                 '(("Goal" :in-theory '((:e dab-basep))))
                 (cons
                  '///
                  (cons
                   (cons
                    'fty::deffixequiv
                    (cons
                     nat-to-bendian*
                     (cons
                      ':hints
                      (cons
                       (cons
                        (cons
                         '"Goal"
                         (cons
                          ':in-theory
                          (cons
                           (cons
                            'quote
                            (cons (cons 'nat=>bendian*-of-nfix-nat
                                        (cons nat-to-bendian* 'nil))
                                  'nil))
                           'nil)))
                        'nil)
                       'nil))))
                   'nil)))))))))))))))
    (nat-to-lendian*-event
     (cons
      'define
      (cons
       nat-to-lendian*
       (cons
        (cons (cons nat '(natp)) 'nil)
        (cons
         ':returns
         (cons
          (cons
           digits
           (cons
            digits-pred
            (cons
             ':hints
             (cons
              (cons
               (cons
                '"Goal"
                (cons
                 ':in-theory
                 (cons
                  (cons
                   'quote
                   (cons
                       (cons digits-pred-correct
                             (cons nat-to-lendian*
                                   '(return-type-of-nat=>lendian*)))
                       'nil))
                  'nil)))
               'nil)
              'nil))))
          (cons
           ':parents
           (cons
            (cons name 'nil)
            (cons
             ':short
             (cons
              (cons
               'xdoc::topstring
               (cons
                  '"Convert a natural number to "
                  (cons '"its minimum-length little-endian list of "
                        (cons digits-description
                              (cons '", seen as sigits in base "
                                    (cons base-string '(".")))))))
              (cons
               (cons 'nat=>lendian*
                     (cons base (cons nat 'nil)))
               (cons
                ':guard-hints
                (cons
                 '(("Goal" :in-theory '((:e dab-basep))))
                 (cons
                  '///
                  (cons
                   (cons
                    'fty::deffixequiv
                    (cons
                     nat-to-lendian*
                     (cons
                      ':hints
                      (cons
                       (cons
                        (cons
                         '"Goal"
                         (cons
                          ':in-theory
                          (cons
                           (cons
                            'quote
                            (cons (cons 'nat=>lendian*-of-nfix-nat
                                        (cons nat-to-lendian* 'nil))
                                  'nil))
                           'nil)))
                        'nil)
                       'nil))))
                   'nil)))))))))))))))
    (nat-to-bendian+-event
     (cons
      'define
      (cons
       nat-to-bendian+
       (cons
        (cons (cons nat '(natp)) 'nil)
        (cons
         ':returns
         (cons
          (cons
           digits
           (cons
            digits-pred
            (cons
             ':hints
             (cons
              (cons
               (cons
                '"Goal"
                (cons
                 ':in-theory
                 (cons
                  (cons
                   'quote
                   (cons
                       (cons digits-pred-correct
                             (cons nat-to-bendian+
                                   '(return-type-of-nat=>bendian+)))
                       'nil))
                  'nil)))
               'nil)
              'nil))))
          (cons
           ':parents
           (cons
            (cons name 'nil)
            (cons
             ':short
             (cons
              (cons
               'xdoc::topstring
               (cons
                '"Convert a natural number to "
                (cons
                 '"its non-empty minimum-length big-endian list of "
                 (cons digits-description
                       (cons '", seen as sigits in base "
                             (cons base-string '(".")))))))
              (cons
               (cons 'nat=>bendian+
                     (cons base (cons nat 'nil)))
               (cons
                ':guard-hints
                (cons
                 '(("Goal" :in-theory '((:e dab-basep))))
                 (cons
                  '///
                  (cons
                   (cons
                    'fty::deffixequiv
                    (cons
                     nat-to-bendian+
                     (cons
                      ':hints
                      (cons
                       (cons
                        (cons
                         '"Goal"
                         (cons
                          ':in-theory
                          (cons
                           (cons
                            'quote
                            (cons (cons 'nat=>bendian+-of-nfix-nat
                                        (cons nat-to-bendian+ 'nil))
                                  'nil))
                           'nil)))
                        'nil)
                       'nil))))
                   'nil)))))))))))))))
    (nat-to-lendian+-event
     (cons
      'define
      (cons
       nat-to-lendian+
       (cons
        (cons (cons nat '(natp)) 'nil)
        (cons
         ':returns
         (cons
          (cons
           digits
           (cons
            digits-pred
            (cons
             ':hints
             (cons
              (cons
               (cons
                '"Goal"
                (cons
                 ':in-theory
                 (cons
                  (cons
                   'quote
                   (cons
                       (cons digits-pred-correct
                             (cons nat-to-lendian+
                                   '(return-type-of-nat=>lendian+)))
                       'nil))
                  'nil)))
               'nil)
              'nil))))
          (cons
           ':parents
           (cons
            (cons name 'nil)
            (cons
             ':short
             (cons
              (cons
               'xdoc::topstring
               (cons
                '"Convert a natural number to "
                (cons
                 '"its non-empty minimum-length little-endian list of "
                 (cons digits-description
                       (cons '", seen as sigits in base "
                             (cons base-string '(".")))))))
              (cons
               (cons 'nat=>lendian+
                     (cons base (cons nat 'nil)))
               (cons
                ':guard-hints
                (cons
                 '(("Goal" :in-theory '((:e dab-basep))))
                 (cons
                  '///
                  (cons
                   (cons
                    'fty::deffixequiv
                    (cons
                     nat-to-lendian+
                     (cons
                      ':hints
                      (cons
                       (cons
                        (cons
                         '"Goal"
                         (cons
                          ':in-theory
                          (cons
                           (cons
                            'quote
                            (cons (cons 'nat=>lendian+-of-nfix-nat
                                        (cons nat-to-lendian+ 'nil))
                                  'nil))
                           'nil)))
                        'nil)
                       'nil))))
                   'nil)))))))))))))))
    (bendian-to-nat-of-nat-to-bendian-event
     (cons
      'defrule
      (cons
       bendian-to-nat-of-nat-to-bendian
       (cons
        ':parents
        (cons
         (cons bendian-to-nat
               (cons nat-to-bendian 'nil))
         (cons
          (cons
           'implies
           (cons
            (cons
             '<
             (cons
              (cons 'nfix (cons nat 'nil))
              (cons (cons 'expt
                          (cons base
                                (cons (cons 'nfix (cons width 'nil))
                                      'nil)))
                    'nil)))
            (cons
             (cons
               'equal
               (cons (cons bendian-to-nat
                           (cons (cons nat-to-bendian
                                       (cons width (cons nat 'nil)))
                                 'nil))
                     (cons (cons 'nfix (cons nat 'nil))
                           'nil)))
             'nil)))
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
              (cons
               bendian-to-nat
               (cons
                 nat-to-bendian
                 '(bendian=>nat-of-nat=>bendian (:e dab-base-fix))))
              'nil))
            'nil))))))))
    (lendian-to-nat-of-nat-to-lendian-event
     (cons
      'defrule
      (cons
       lendian-to-nat-of-nat-to-lendian
       (cons
        ':parents
        (cons
         (cons lendian-to-nat
               (cons nat-to-lendian 'nil))
         (cons
          (cons
           'implies
           (cons
            (cons
             '<
             (cons
              (cons 'nfix (cons nat 'nil))
              (cons (cons 'expt
                          (cons base
                                (cons (cons 'nfix (cons width 'nil))
                                      'nil)))
                    'nil)))
            (cons
             (cons
               'equal
               (cons (cons lendian-to-nat
                           (cons (cons nat-to-lendian
                                       (cons width (cons nat 'nil)))
                                 'nil))
                     (cons (cons 'nfix (cons nat 'nil))
                           'nil)))
             'nil)))
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
              (cons
               lendian-to-nat
               (cons
                 nat-to-lendian
                 '(lendian=>nat-of-nat=>lendian (:e dab-base-fix))))
              'nil))
            'nil))))))))
    (bendian-to-nat-of-nat-to-bendian*-event
     (cons
      'defrule
      (cons
       bendian-to-nat-of-nat-to-bendian*
       (cons
        ':parents
        (cons
         (cons bendian-to-nat
               (cons nat-to-bendian* 'nil))
         (cons
          (cons
            'equal
            (cons (cons bendian-to-nat
                        (cons (cons nat-to-bendian* (cons nat 'nil))
                              'nil))
                  (cons (cons 'nfix (cons nat 'nil))
                        'nil)))
          (cons
           ':in-theory
           (cons
            (cons
                'quote
                (cons (cons bendian-to-nat
                            (cons nat-to-bendian*
                                  '(bendian=>nat-of-nat=>bendian*)))
                      'nil))
            'nil))))))))
    (lendian-to-nat-of-nat-to-lendian*-event
     (cons
      'defrule
      (cons
       lendian-to-nat-of-nat-to-lendian*
       (cons
        ':parents
        (cons
         (cons lendian-to-nat
               (cons nat-to-lendian* 'nil))
         (cons
          (cons
            'equal
            (cons (cons lendian-to-nat
                        (cons (cons nat-to-lendian* (cons nat 'nil))
                              'nil))
                  (cons (cons 'nfix (cons nat 'nil))
                        'nil)))
          (cons
           ':in-theory
           (cons
            (cons
                'quote
                (cons (cons lendian-to-nat
                            (cons nat-to-lendian*
                                  '(lendian=>nat-of-nat=>lendian*)))
                      'nil))
            'nil))))))))
    (bendian-to-nat-of-nat-to-bendian+-event
     (cons
      'defrule
      (cons
       bendian-to-nat-of-nat-to-bendian+
       (cons
        ':parents
        (cons
         (cons bendian-to-nat
               (cons nat-to-bendian+ 'nil))
         (cons
          (cons
            'equal
            (cons (cons bendian-to-nat
                        (cons (cons nat-to-bendian+ (cons nat 'nil))
                              'nil))
                  (cons (cons 'nfix (cons nat 'nil))
                        'nil)))
          (cons
           ':in-theory
           (cons
            (cons
                'quote
                (cons (cons bendian-to-nat
                            (cons nat-to-bendian+
                                  '(bendian=>nat-of-nat=>bendian+)))
                      'nil))
            'nil))))))))
    (lendian-to-nat-of-nat-to-lendian+-event
     (cons
      'defrule
      (cons
       lendian-to-nat-of-nat-to-lendian+
       (cons
        ':parents
        (cons
         (cons lendian-to-nat
               (cons nat-to-lendian+ 'nil))
         (cons
          (cons
            'equal
            (cons (cons lendian-to-nat
                        (cons (cons nat-to-lendian+ (cons nat 'nil))
                              'nil))
                  (cons (cons 'nfix (cons nat 'nil))
                        'nil)))
          (cons
           ':in-theory
           (cons
            (cons
                'quote
                (cons (cons lendian-to-nat
                            (cons nat-to-lendian+
                                  '(lendian=>nat-of-nat=>lendian+)))
                      'nil))
            'nil))))))))
    (nat-to-bendian-injectivity-event
     (cons
      'defrule
      (cons
       nat-to-bendian-injectivity
       (cons
        ':parents
        (cons
         (cons nat-to-bendian 'nil)
         (cons
          (cons
           'implies
           (cons
            (cons
             'and
             (cons
              (cons
               '<
               (cons
                (cons 'nfix (cons nat1 'nil))
                (cons
                    (cons 'expt
                          (cons base
                                (cons (cons 'nfix (cons width 'nil))
                                      'nil)))
                    'nil)))
              (cons
               (cons
                '<
                (cons
                 (cons 'nfix (cons nat2 'nil))
                 (cons
                    (cons 'expt
                          (cons base
                                (cons (cons 'nfix (cons width 'nil))
                                      'nil)))
                    'nil)))
               'nil)))
            (cons
             (cons
              'equal
              (cons
               (cons
                    'equal
                    (cons (cons nat-to-bendian
                                (cons width (cons nat1 'nil)))
                          (cons (cons nat-to-bendian
                                      (cons width (cons nat2 'nil)))
                                'nil)))
               (cons (cons 'equal
                           (cons (cons 'nfix (cons nat1 'nil))
                                 (cons (cons 'nfix (cons nat2 'nil))
                                       'nil)))
                     'nil)))
             'nil)))
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
                (cons nat-to-bendian
                      '(nat=>bendian-injectivity (:e dab-base-fix)))
                'nil))
            'nil))))))))
    (nat-to-lendian-injectivity-event
     (cons
      'defrule
      (cons
       nat-to-lendian-injectivity
       (cons
        ':parents
        (cons
         (cons nat-to-lendian 'nil)
         (cons
          (cons
           'implies
           (cons
            (cons
             'and
             (cons
              (cons
               '<
               (cons
                (cons 'nfix (cons nat1 'nil))
                (cons
                    (cons 'expt
                          (cons base
                                (cons (cons 'nfix (cons width 'nil))
                                      'nil)))
                    'nil)))
              (cons
               (cons
                '<
                (cons
                 (cons 'nfix (cons nat2 'nil))
                 (cons
                    (cons 'expt
                          (cons base
                                (cons (cons 'nfix (cons width 'nil))
                                      'nil)))
                    'nil)))
               'nil)))
            (cons
             (cons
              'equal
              (cons
               (cons
                    'equal
                    (cons (cons nat-to-lendian
                                (cons width (cons nat1 'nil)))
                          (cons (cons nat-to-lendian
                                      (cons width (cons nat2 'nil)))
                                'nil)))
               (cons (cons 'equal
                           (cons (cons 'nfix (cons nat1 'nil))
                                 (cons (cons 'nfix (cons nat2 'nil))
                                       'nil)))
                     'nil)))
             'nil)))
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
                (cons nat-to-lendian
                      '(nat=>lendian-injectivity (:e dab-base-fix)))
                'nil))
            'nil))))))))
    (nat-to-bendian*-injectivity-event
     (cons
      'defrule
      (cons
       nat-to-bendian*-injectivity
       (cons
        ':parents
        (cons
         (cons nat-to-bendian* 'nil)
         (cons
          (cons
           'equal
           (cons
            (cons
                 'equal
                 (cons (cons nat-to-bendian* (cons nat1 'nil))
                       (cons (cons nat-to-bendian* (cons nat2 'nil))
                             'nil)))
            (cons (cons 'equal
                        (cons (cons 'nfix (cons nat1 'nil))
                              (cons (cons 'nfix (cons nat2 'nil))
                                    'nil)))
                  'nil)))
          (cons
               ':in-theory
               (cons (cons 'quote
                           (cons (cons nat-to-bendian*
                                       '(nat=>bendian*-injectivity))
                                 'nil))
                     'nil))))))))
    (nat-to-lendian*-injectivity-event
     (cons
      'defrule
      (cons
       nat-to-lendian*-injectivity
       (cons
        ':parents
        (cons
         (cons nat-to-lendian* 'nil)
         (cons
          (cons
           'equal
           (cons
            (cons
                 'equal
                 (cons (cons nat-to-lendian* (cons nat1 'nil))
                       (cons (cons nat-to-lendian* (cons nat2 'nil))
                             'nil)))
            (cons (cons 'equal
                        (cons (cons 'nfix (cons nat1 'nil))
                              (cons (cons 'nfix (cons nat2 'nil))
                                    'nil)))
                  'nil)))
          (cons
               ':in-theory
               (cons (cons 'quote
                           (cons (cons nat-to-lendian*
                                       '(nat=>lendian*-injectivity))
                                 'nil))
                     'nil))))))))
    (nat-to-bendian+-injectivity-event
     (cons
      'defrule
      (cons
       nat-to-bendian+-injectivity
       (cons
        ':parents
        (cons
         (cons nat-to-bendian+ 'nil)
         (cons
          (cons
           'equal
           (cons
            (cons
                 'equal
                 (cons (cons nat-to-bendian+ (cons nat1 'nil))
                       (cons (cons nat-to-bendian+ (cons nat2 'nil))
                             'nil)))
            (cons (cons 'equal
                        (cons (cons 'nfix (cons nat1 'nil))
                              (cons (cons 'nfix (cons nat2 'nil))
                                    'nil)))
                  'nil)))
          (cons
               ':in-theory
               (cons (cons 'quote
                           (cons (cons nat-to-bendian+
                                       '(nat=>bendian+-injectivity))
                                 'nil))
                     'nil))))))))
    (nat-to-lendian+-injectivity-event
     (cons
      'defrule
      (cons
       nat-to-lendian+-injectivity
       (cons
        ':parents
        (cons
         (cons nat-to-lendian+ 'nil)
         (cons
          (cons
           'equal
           (cons
            (cons
                 'equal
                 (cons (cons nat-to-lendian+ (cons nat1 'nil))
                       (cons (cons nat-to-lendian+ (cons nat2 'nil))
                             'nil)))
            (cons (cons 'equal
                        (cons (cons 'nfix (cons nat1 'nil))
                              (cons (cons 'nfix (cons nat2 'nil))
                                    'nil)))
                  'nil)))
          (cons
               ':in-theory
               (cons (cons 'quote
                           (cons (cons nat-to-lendian+
                                       '(nat=>lendian+-injectivity))
                                 'nil))
                     'nil))))))))
    (nat-to-bendian-of-bendian-to-nat-event
     (cons
      'defrule
      (cons
       nat-to-bendian-of-bendian-to-nat
       (cons
        ':parents
        (cons
         (cons nat-to-bendian
               (cons bendian-to-nat 'nil))
         (cons
          (cons
           'equal
           (cons
            (cons
                nat-to-bendian
                (cons (cons 'len (cons digits 'nil))
                      (cons (cons bendian-to-nat (cons digits 'nil))
                            'nil)))
            (cons (cons digits-fix (cons digits 'nil))
                  'nil)))
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
                 (cons bendian-to-nat
                       (cons nat-to-bendian
                             (cons 'nat=>bendian-of-bendian=>nat
                                   (cons digits-fix-correct 'nil))))
                 'nil))
            'nil))))))))
    (nat-to-lendian-of-lendian-to-nat-event
     (cons
      'defrule
      (cons
       nat-to-lendian-of-lendian-to-nat
       (cons
        ':parents
        (cons
         (cons nat-to-lendian
               (cons lendian-to-nat 'nil))
         (cons
          (cons
           'equal
           (cons
            (cons
                nat-to-lendian
                (cons (cons 'len (cons digits 'nil))
                      (cons (cons lendian-to-nat (cons digits 'nil))
                            'nil)))
            (cons (cons digits-fix (cons digits 'nil))
                  'nil)))
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
                 (cons lendian-to-nat
                       (cons nat-to-lendian
                             (cons 'nat=>lendian-of-lendian=>nat
                                   (cons digits-fix-correct 'nil))))
                 'nil))
            'nil))))))))
    (nat-to-bendian*-of-bendian-to-nat-event
     (cons
      'defrule
      (cons
       nat-to-bendian*-of-bendian-to-nat
       (cons
        ':parents
        (cons
         (cons nat-to-bendian*
               (cons bendian-to-nat 'nil))
         (cons
          (cons
           'equal
           (cons
              (cons nat-to-bendian*
                    (cons (cons bendian-to-nat (cons digits 'nil))
                          'nil))
              (cons (cons 'trim-bendian*
                          (cons (cons digits-fix (cons digits 'nil))
                                'nil))
                    'nil)))
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
                 (cons bendian-to-nat
                       (cons nat-to-bendian*
                             (cons 'nat=>bendian*-of-bendian=>nat
                                   (cons digits-fix-correct 'nil))))
                 'nil))
            'nil))))))))
    (nat-to-lendian*-of-lendian-to-nat-event
     (cons
      'defrule
      (cons
       nat-to-lendian*-of-lendian-to-nat
       (cons
        ':parents
        (cons
         (cons nat-to-lendian*
               (cons lendian-to-nat 'nil))
         (cons
          (cons
           'equal
           (cons
              (cons nat-to-lendian*
                    (cons (cons lendian-to-nat (cons digits 'nil))
                          'nil))
              (cons (cons 'trim-lendian*
                          (cons (cons digits-fix (cons digits 'nil))
                                'nil))
                    'nil)))
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
                 (cons lendian-to-nat
                       (cons nat-to-lendian*
                             (cons 'nat=>lendian*-of-lendian=>nat
                                   (cons digits-fix-correct 'nil))))
                 'nil))
            'nil))))))))
    (nat-to-bendian+-of-bendian-to-nat-event
     (cons
      'defrule
      (cons
       nat-to-bendian+-of-bendian-to-nat
       (cons
        ':parents
        (cons
         (cons nat-to-bendian+
               (cons bendian-to-nat 'nil))
         (cons
          (cons
           'equal
           (cons
              (cons nat-to-bendian+
                    (cons (cons bendian-to-nat (cons digits 'nil))
                          'nil))
              (cons (cons 'trim-bendian+
                          (cons (cons digits-fix (cons digits 'nil))
                                'nil))
                    'nil)))
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
                 (cons bendian-to-nat
                       (cons nat-to-bendian+
                             (cons 'nat=>bendian+-of-bendian=>nat
                                   (cons digits-fix-correct 'nil))))
                 'nil))
            'nil))))))))
    (nat-to-lendian+-of-lendian-to-nat-event
     (cons
      'defrule
      (cons
       nat-to-lendian+-of-lendian-to-nat
       (cons
        ':parents
        (cons
         (cons nat-to-lendian+
               (cons lendian-to-nat 'nil))
         (cons
          (cons
           'equal
           (cons
              (cons nat-to-lendian+
                    (cons (cons lendian-to-nat (cons digits 'nil))
                          'nil))
              (cons (cons 'trim-lendian+
                          (cons (cons digits-fix (cons digits 'nil))
                                'nil))
                    'nil)))
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
                 (cons lendian-to-nat
                       (cons nat-to-lendian+
                             (cons 'nat=>lendian+-of-lendian=>nat
                                   (cons digits-fix-correct 'nil))))
                 'nil))
            'nil))))))))
    (bendian-to-nat-injectivity-event
     (cons
      'defrule
      (cons
       bendian-to-nat-injectivity
       (cons
        ':parents
        (cons
         (cons bendian-to-nat 'nil)
         (cons
          (cons
           'implies
           (cons
            (cons 'equal
                  (cons (cons 'len (cons digits1 'nil))
                        (cons (cons 'len (cons digits2 'nil))
                              'nil)))
            (cons
             (cons
              'equal
              (cons
               (cons
                'equal
                (cons
                     (cons bendian-to-nat (cons digits1 'nil))
                     (cons (cons bendian-to-nat (cons digits2 'nil))
                           'nil)))
               (cons
                (cons
                   'equal
                   (cons (cons digits-fix (cons digits1 'nil))
                         (cons (cons digits-fix (cons digits2 'nil))
                               'nil)))
                'nil)))
             'nil)))
          (cons
           ':in-theory
           (cons
            (cons 'quote
                  (cons (cons bendian-to-nat
                              (cons 'bendian=>nat-injectivity
                                    (cons digits-fix-correct 'nil)))
                        'nil))
            'nil))))))))
    (lendian-to-nat-injectivity-event
     (cons
      'defrule
      (cons
       lendian-to-nat-injectivity
       (cons
        ':parents
        (cons
         (cons lendian-to-nat 'nil)
         (cons
          (cons
           'implies
           (cons
            (cons 'equal
                  (cons (cons 'len (cons digits1 'nil))
                        (cons (cons 'len (cons digits2 'nil))
                              'nil)))
            (cons
             (cons
              'equal
              (cons
               (cons
                'equal
                (cons
                     (cons lendian-to-nat (cons digits1 'nil))
                     (cons (cons lendian-to-nat (cons digits2 'nil))
                           'nil)))
               (cons
                (cons
                   'equal
                   (cons (cons digits-fix (cons digits1 'nil))
                         (cons (cons digits-fix (cons digits2 'nil))
                               'nil)))
                'nil)))
             'nil)))
          (cons
           ':in-theory
           (cons
            (cons 'quote
                  (cons (cons lendian-to-nat
                              (cons 'lendian=>nat-injectivity
                                    (cons digits-fix-correct 'nil)))
                        'nil))
            'nil))))))))
    (bendian-to-nat-injectivity*-event
     (cons
      'defrule
      (cons
       bendian-to-nat-injectivity*
       (cons
        ':parents
        (cons
         (cons bendian-to-nat 'nil)
         (cons
          (cons
           'implies
           (cons
            (cons
             'and
             (cons
              (cons
               'equal
               (cons
                   (cons 'trim-bendian*
                         (cons (cons digits-fix (cons digits1 'nil))
                               'nil))
                   (cons digits1 'nil)))
              (cons
               (cons
                'equal
                (cons
                   (cons 'trim-bendian*
                         (cons (cons digits-fix (cons digits2 'nil))
                               'nil))
                   (cons digits2 'nil)))
               'nil)))
            (cons
             (cons
              'equal
              (cons
               (cons
                'equal
                (cons
                     (cons bendian-to-nat (cons digits1 'nil))
                     (cons (cons bendian-to-nat (cons digits2 'nil))
                           'nil)))
               (cons (cons 'equal
                           (cons digits1 (cons digits2 'nil)))
                     'nil)))
             'nil)))
          (cons
           ':in-theory
           (cons
            (cons 'quote
                  (cons (cons bendian-to-nat
                              (cons 'bendian=>nat-injectivity*
                                    (cons digits-fix-correct 'nil)))
                        'nil))
            'nil))))))))
    (lendian-to-nat-injectivity*-event
     (cons
      'defrule
      (cons
       lendian-to-nat-injectivity*
       (cons
        ':parents
        (cons
         (cons lendian-to-nat 'nil)
         (cons
          (cons
           'implies
           (cons
            (cons
             'and
             (cons
              (cons
               'equal
               (cons
                   (cons 'trim-lendian*
                         (cons (cons digits-fix (cons digits1 'nil))
                               'nil))
                   (cons digits1 'nil)))
              (cons
               (cons
                'equal
                (cons
                   (cons 'trim-lendian*
                         (cons (cons digits-fix (cons digits2 'nil))
                               'nil))
                   (cons digits2 'nil)))
               'nil)))
            (cons
             (cons
              'equal
              (cons
               (cons
                'equal
                (cons
                     (cons lendian-to-nat (cons digits1 'nil))
                     (cons (cons lendian-to-nat (cons digits2 'nil))
                           'nil)))
               (cons (cons 'equal
                           (cons digits1 (cons digits2 'nil)))
                     'nil)))
             'nil)))
          (cons
           ':in-theory
           (cons
            (cons 'quote
                  (cons (cons lendian-to-nat
                              (cons 'lendian=>nat-injectivity*
                                    (cons digits-fix-correct 'nil)))
                        'nil))
            'nil))))))))
    (bendian-to-nat-injectivity+-event
     (cons
      'defrule
      (cons
       bendian-to-nat-injectivity+
       (cons
        ':parents
        (cons
         (cons bendian-to-nat 'nil)
         (cons
          (cons
           'implies
           (cons
            (cons
             'and
             (cons
              (cons
               'equal
               (cons
                   (cons 'trim-bendian+
                         (cons (cons digits-fix (cons digits1 'nil))
                               'nil))
                   (cons digits1 'nil)))
              (cons
               (cons
                'equal
                (cons
                   (cons 'trim-bendian+
                         (cons (cons digits-fix (cons digits2 'nil))
                               'nil))
                   (cons digits2 'nil)))
               'nil)))
            (cons
             (cons
              'equal
              (cons
               (cons
                'equal
                (cons
                     (cons bendian-to-nat (cons digits1 'nil))
                     (cons (cons bendian-to-nat (cons digits2 'nil))
                           'nil)))
               (cons (cons 'equal
                           (cons digits1 (cons digits2 'nil)))
                     'nil)))
             'nil)))
          (cons
           ':in-theory
           (cons
            (cons 'quote
                  (cons (cons bendian-to-nat
                              (cons 'bendian=>nat-injectivity+
                                    (cons digits-fix-correct 'nil)))
                        'nil))
            'nil))))))))
    (lendian-to-nat-injectivity+-event
     (cons
      'defrule
      (cons
       lendian-to-nat-injectivity+
       (cons
        ':parents
        (cons
         (cons lendian-to-nat 'nil)
         (cons
          (cons
           'implies
           (cons
            (cons
             'and
             (cons
              (cons
               'equal
               (cons
                   (cons 'trim-lendian+
                         (cons (cons digits-fix (cons digits1 'nil))
                               'nil))
                   (cons digits1 'nil)))
              (cons
               (cons
                'equal
                (cons
                   (cons 'trim-lendian+
                         (cons (cons digits-fix (cons digits2 'nil))
                               'nil))
                   (cons digits2 'nil)))
               'nil)))
            (cons
             (cons
              'equal
              (cons
               (cons
                'equal
                (cons
                     (cons lendian-to-nat (cons digits1 'nil))
                     (cons (cons lendian-to-nat (cons digits2 'nil))
                           'nil)))
               (cons (cons 'equal
                           (cons digits1 (cons digits2 'nil)))
                     'nil)))
             'nil)))
          (cons
           ':in-theory
           (cons
            (cons 'quote
                  (cons (cons lendian-to-nat
                              (cons 'lendian=>nat-injectivity+
                                    (cons digits-fix-correct 'nil)))
                        'nil))
            'nil))))))))
    (len-of-nat-to-bendian*-leq-width-event
     (cons
      'defruled
      (cons
       len-of-nat-to-bendian*-leq-width
       (cons
        ':parents
        (cons
         (cons nat-to-bendian* 'nil)
         (cons
          (cons
           'implies
           (cons
            (cons 'and
                  (cons (cons 'natp (cons nat 'nil))
                        (cons (cons 'natp (cons width 'nil))
                              'nil)))
            (cons
             (cons
              'equal
              (cons
               (cons
                '<=
                (cons
                  (cons 'len
                        (cons (cons nat-to-bendian* (cons nat 'nil))
                              'nil))
                  (cons width 'nil)))
               (cons
                (cons
                    '<
                    (cons nat
                          (cons (cons 'expt
                                      (cons base (cons width 'nil)))
                                'nil)))
                'nil)))
             'nil)))
          (cons
           ':rule-classes
           (cons
            (cons
             (cons
              ':rewrite
              (cons
               ':corollary
               (cons
                (cons
                 'implies
                 (cons
                  (cons 'and
                        (cons (cons 'natp (cons nat 'nil))
                              (cons (cons 'natp (cons width 'nil))
                                    'nil)))
                  (cons
                   (cons
                    'equal
                    (cons
                     (cons
                      '>
                      (cons
                       (cons
                        'len
                        (cons (cons nat-to-bendian* (cons nat 'nil))
                              'nil))
                       (cons width 'nil)))
                     (cons
                      (cons
                       '>=
                       (cons
                          nat
                          (cons (cons 'expt
                                      (cons base (cons width 'nil)))
                                'nil)))
                      'nil)))
                   'nil)))
                '(:hints (("Goal" :in-theory '(not)))))))
             'nil)
            (cons
             ':in-theory
             (cons
              (cons 'quote
                    (cons (cons 'dab-basep
                                (cons 'natp
                                      (cons nat-to-bendian* 'nil)))
                          'nil))
              (cons
               ':use
               (cons (cons ':instance
                           (cons 'len-of-nat=>bendian*-leq-width
                                 (cons (cons 'base (cons base 'nil))
                                       'nil)))
                     'nil))))))))))))
    (len-of-nat-to-lendian*-leq-width-event
     (cons
      'defruled
      (cons
       len-of-nat-to-lendian*-leq-width
       (cons
        ':parents
        (cons
         (cons nat-to-lendian* 'nil)
         (cons
          (cons
           'implies
           (cons
            (cons 'and
                  (cons (cons 'natp (cons nat 'nil))
                        (cons (cons 'natp (cons width 'nil))
                              'nil)))
            (cons
             (cons
              'equal
              (cons
               (cons
                '<=
                (cons
                  (cons 'len
                        (cons (cons nat-to-lendian* (cons nat 'nil))
                              'nil))
                  (cons width 'nil)))
               (cons
                (cons
                    '<
                    (cons nat
                          (cons (cons 'expt
                                      (cons base (cons width 'nil)))
                                'nil)))
                'nil)))
             'nil)))
          (cons
           ':rule-classes
           (cons
            (cons
             (cons
              ':rewrite
              (cons
               ':corollary
               (cons
                (cons
                 'implies
                 (cons
                  (cons 'and
                        (cons (cons 'natp (cons nat 'nil))
                              (cons (cons 'natp (cons width 'nil))
                                    'nil)))
                  (cons
                   (cons
                    'equal
                    (cons
                     (cons
                      '>
                      (cons
                       (cons
                        'len
                        (cons (cons nat-to-lendian* (cons nat 'nil))
                              'nil))
                       (cons width 'nil)))
                     (cons
                      (cons
                       '>=
                       (cons
                          nat
                          (cons (cons 'expt
                                      (cons base (cons width 'nil)))
                                'nil)))
                      'nil)))
                   'nil)))
                '(:hints (("Goal" :in-theory '(not)))))))
             'nil)
            (cons
             ':in-theory
             (cons
              (cons 'quote
                    (cons (cons 'dab-basep
                                (cons 'natp
                                      (cons nat-to-lendian* 'nil)))
                          'nil))
              (cons
               ':use
               (cons (cons ':instance
                           (cons 'len-of-nat=>lendian*-leq-width
                                 (cons (cons 'base (cons base 'nil))
                                       'nil)))
                     'nil))))))))))))
    (len-0-of-nat-to-bendian*-event
     (cons
      'defrule
      (cons
       len-0-of-nat-to-bendian*
       (cons
        (cons
         'equal
         (cons
          (cons
              'equal
              (cons (cons 'len
                          (cons (cons nat-to-bendian* (cons x 'nil))
                                'nil))
                    '(0)))
          (cons (cons 'zp (cons x 'nil)) 'nil)))
        (cons
         ':enable
         (cons
          nat-to-bendian*
          (cons
               ':use
               (cons (cons ':instance
                           (cons 'len-0-of-nat=>bendian*
                                 (cons (cons 'base (cons base 'nil))
                                       'nil)))
                     'nil))))))))
    (len-0-of-nat-to-lendian*-event
     (cons
      'defrule
      (cons
       len-0-of-nat-to-lendian*
       (cons
        (cons
         'equal
         (cons
          (cons
              'equal
              (cons (cons 'len
                          (cons (cons nat-to-lendian* (cons x 'nil))
                                'nil))
                    '(0)))
          (cons (cons 'zp (cons x 'nil)) 'nil)))
        (cons
         ':enable
         (cons
          nat-to-lendian*
          (cons
               ':use
               (cons (cons ':instance
                           (cons 'len-0-of-nat=>lendian*
                                 (cons (cons 'base (cons base 'nil))
                                       'nil)))
                     'nil))))))))
    (consp-pf-nat-to-bendian*-iff-not-zp-event
     (cons
      'defrule
      (cons
       consp-pf-nat-to-bendian*-iff-not-zp
       (cons
        (cons
           'equal
           (cons (cons 'consp
                       (cons (cons nat-to-bendian* (cons nat 'nil))
                             'nil))
                 (cons (cons 'not
                             (cons (cons 'zp (cons nat 'nil)) 'nil))
                       'nil)))
        (cons
         ':enable
         (cons
          nat-to-bendian*
          (cons
               ':use
               (cons (cons ':instance
                           (cons 'consp-of-nat=>bendian*-iff-not-zp
                                 (cons (cons 'base (cons base 'nil))
                                       'nil)))
                     'nil))))))))
    (consp-pf-nat-to-lendian*-iff-not-zp-event
     (cons
      'defrule
      (cons
       consp-pf-nat-to-lendian*-iff-not-zp
       (cons
        (cons
           'equal
           (cons (cons 'consp
                       (cons (cons nat-to-lendian* (cons nat 'nil))
                             'nil))
                 (cons (cons 'not
                             (cons (cons 'zp (cons nat 'nil)) 'nil))
                       'nil)))
        (cons
         ':enable
         (cons
          nat-to-lendian*
          (cons
               ':use
               (cons (cons ':instance
                           (cons 'consp-of-nat=>lendian*-iff-not-zp
                                 (cons (cons 'base (cons base 'nil))
                                       'nil)))
                     'nil))))))))
    (trim-bendian*-of-nat-to-bendian*-event
     (cons
      'defrule
      (cons
       trim-bendian*-of-nat-to-bendian*
       (cons
        (cons
            'equal
            (cons (cons 'trim-bendian*
                        (cons (cons nat-to-bendian* (cons nat 'nil))
                              'nil))
                  (cons (cons nat-to-bendian* (cons nat 'nil))
                        'nil)))
        (cons
         ':enable
         (cons
          nat-to-bendian*
          (cons
               ':use
               (cons (cons ':instance
                           (cons 'trim-bendian*-of-nat=>bendian*
                                 (cons (cons 'base (cons base 'nil))
                                       'nil)))
                     'nil))))))))
    (trim-lendian*-of-nat-to-lendian*-event
     (cons
      'defrule
      (cons
       trim-lendian*-of-nat-to-lendian*
       (cons
        (cons
            'equal
            (cons (cons 'trim-lendian*
                        (cons (cons nat-to-lendian* (cons nat 'nil))
                              'nil))
                  (cons (cons nat-to-lendian* (cons nat 'nil))
                        'nil)))
        (cons
         ':enable
         (cons
          nat-to-lendian*
          (cons
               ':use
               (cons (cons ':instance
                           (cons 'trim-lendian*-of-nat=>lendian*
                                 (cons (cons 'base (cons base 'nil))
                                       'nil)))
                     'nil))))))))
    (bendian-to-nat-of-cons-event
     (cons
      'defruled
      (cons
       bendian-to-nat-of-cons
       (cons
        (cons
         'equal
         (cons
          (cons bendian-to-nat
                (cons (cons 'cons
                            (cons hidigit (cons lodigits 'nil)))
                      'nil))
          (cons
           (cons
            '+
            (cons
             (cons
              '*
              (cons
               (cons digit-fix (cons hidigit 'nil))
               (cons
                  (cons 'expt
                        (cons base
                              (cons (cons 'len (cons lodigits 'nil))
                                    'nil)))
                  'nil)))
             (cons (cons bendian-to-nat (cons lodigits 'nil))
                   'nil)))
           'nil)))
        (cons
         ':enable
         (cons
          (cons bendian-to-nat
                (cons digit-fix-correct 'nil))
          (cons
               ':use
               (cons (cons ':instance
                           (cons 'bendian=>nat-of-cons
                                 (cons (cons 'base (cons base 'nil))
                                       'nil)))
                     'nil))))))))
    (lendian-to-nat-of-cons-event
     (cons
      'defruled
      (cons
       lendian-to-nat-of-cons
       (cons
        (cons
         'equal
         (cons
          (cons lendian-to-nat
                (cons (cons 'cons
                            (cons lodigit (cons hidigits 'nil)))
                      'nil))
          (cons
           (cons
            '+
            (cons
             (cons digit-fix (cons lodigit 'nil))
             (cons
              (cons
               '*
               (cons
                    base
                    (cons (cons lendian-to-nat (cons hidigits 'nil))
                          'nil)))
              'nil)))
           'nil)))
        (cons
         ':enable
         (cons
          (cons lendian-to-nat
                (cons digit-fix-correct 'nil))
          (cons
               ':use
               (cons (cons ':instance
                           (cons 'lendian=>nat-of-cons
                                 (cons (cons 'base (cons base 'nil))
                                       'nil)))
                     'nil))))))))
    (bendian-to-nat-of-append-event
     (cons
      'defruled
      (cons
       bendian-to-nat-of-append
       (cons
        (cons
         'equal
         (cons
          (cons bendian-to-nat
                (cons (cons 'append
                            (cons hidigits (cons lodigits 'nil)))
                      'nil))
          (cons
           (cons
            '+
            (cons
             (cons
              '*
              (cons
               (cons bendian-to-nat (cons hidigits 'nil))
               (cons
                  (cons 'expt
                        (cons base
                              (cons (cons 'len (cons lodigits 'nil))
                                    'nil)))
                  'nil)))
             (cons (cons bendian-to-nat (cons lodigits 'nil))
                   'nil)))
           'nil)))
        (cons
         ':enable
         (cons
          bendian-to-nat
          (cons
               ':use
               (cons (cons ':instance
                           (cons 'bendian=>nat-of-append
                                 (cons (cons 'base (cons base 'nil))
                                       'nil)))
                     'nil))))))))
    (lendian-to-nat-of-append-event
     (cons
      'defruled
      (cons
       lendian-to-nat-of-append
       (cons
        (cons
         'equal
         (cons
          (cons lendian-to-nat
                (cons (cons 'append
                            (cons lodigits (cons hidigits 'nil)))
                      'nil))
          (cons
           (cons
            '+
            (cons
             (cons lendian-to-nat (cons lodigits 'nil))
             (cons
              (cons
               '*
               (cons
                (cons lendian-to-nat (cons hidigits 'nil))
                (cons
                  (cons 'expt
                        (cons base
                              (cons (cons 'len (cons lodigits 'nil))
                                    'nil)))
                  'nil)))
              'nil)))
           'nil)))
        (cons
         ':enable
         (cons
          lendian-to-nat
          (cons
               ':use
               (cons (cons ':instance
                           (cons 'lendian=>nat-of-append
                                 (cons (cons 'base (cons base 'nil))
                                       'nil)))
                     'nil))))))))
    (bendian-to-nat-of-all-zeros-event
     (cons
      'defrule
      (cons
       bendian-to-nat-of-all-zeros
       (cons
        (cons 'equal
              (cons (cons bendian-to-nat
                          (cons (cons 'repeat (cons n '(0)))
                                'nil))
                    '(0)))
        (cons
         ':enable
         (cons
          bendian-to-nat
          (cons
               ':use
               (cons (cons ':instance
                           (cons 'bendian=>nat-of-all-zeros
                                 (cons (cons 'base (cons base 'nil))
                                       'nil)))
                     'nil))))))))
    (lendian-to-nat-of-all-zeros-event
     (cons
      'defrule
      (cons
       lendian-to-nat-of-all-zeros
       (cons
        (cons 'equal
              (cons (cons lendian-to-nat
                          (cons (cons 'repeat (cons n '(0)))
                                'nil))
                    '(0)))
        (cons
         ':enable
         (cons
          lendian-to-nat
          (cons
               ':use
               (cons (cons ':instance
                           (cons 'lendian=>nat-of-all-zeros
                                 (cons (cons 'base (cons base 'nil))
                                       'nil)))
                     'nil))))))))
    (bendian-to-nat-upper-bound-event
     (cons
      'defrule
      (cons
       bendian-to-nat-upper-bound
       (cons
        (cons
         '<
         (cons
              (cons bendian-to-nat (cons digits 'nil))
              (cons (cons 'expt
                          (cons base
                                (cons (cons 'len (cons digits 'nil))
                                      'nil)))
                    'nil)))
        (cons
         ':rule-classes
         (cons
          (cons
           (cons
            ':linear
            (cons
                ':trigger-terms
                (cons (cons (cons bendian-to-nat (cons digits 'nil))
                            'nil)
                      'nil)))
           'nil)
          (cons
           ':enable
           (cons
            bendian-to-nat
            (cons
               ':use
               (cons (cons ':instance
                           (cons 'bendian=>nat-upper-bound
                                 (cons (cons 'base (cons base 'nil))
                                       'nil)))
                     'nil))))))))))
    (lendian-to-nat-upper-bound-event
     (cons
      'defrule
      (cons
       lendian-to-nat-upper-bound
       (cons
        (cons
         '<
         (cons
              (cons lendian-to-nat (cons digits 'nil))
              (cons (cons 'expt
                          (cons base
                                (cons (cons 'len (cons digits 'nil))
                                      'nil)))
                    'nil)))
        (cons
         ':rule-classes
         (cons
          (cons
           (cons
            ':linear
            (cons
                ':trigger-terms
                (cons (cons (cons lendian-to-nat (cons digits 'nil))
                            'nil)
                      'nil)))
           'nil)
          (cons
           ':enable
           (cons
            lendian-to-nat
            (cons
               ':use
               (cons (cons ':instance
                           (cons 'lendian=>nat-upper-bound
                                 (cons (cons 'base (cons base 'nil))
                                       'nil)))
                     'nil))))))))))
    (lendian-to-nat-as-bendian-to-nat-event
     (cons
      'defruled
      (cons
       lendian-to-nat-as-bendian-to-nat
       (cons
        (cons 'equal
              (cons (cons lendian-to-nat (cons digits 'nil))
                    (cons (cons bendian-to-nat
                                (cons (cons 'rev (cons digits 'nil))
                                      'nil))
                          'nil)))
        (cons ':enable
              (cons (cons lendian-to-nat
                          (cons bendian-to-nat
                                '(lendian=>nat-as-bendian=>nat)))
                    'nil))))))
    (bendian-to-nat-as-lendian-to-nat-event
     (cons
      'defruled
      (cons
       bendian-to-nat-as-lendian-to-nat
       (cons
        (cons 'equal
              (cons (cons bendian-to-nat (cons digits 'nil))
                    (cons (cons lendian-to-nat
                                (cons (cons 'rev (cons digits 'nil))
                                      'nil))
                          'nil)))
        (cons ':enable
              (cons (cons bendian-to-nat
                          (cons lendian-to-nat '(bendian=>nat)))
                    'nil))))))
    (lendian-to-nat-of-rev-event
     (cons
      'defruled
      (cons
       lendian-to-nat-of-rev
       (cons
          (cons 'equal
                (cons (cons lendian-to-nat
                            (cons (cons 'rev (cons digits 'nil))
                                  'nil))
                      (cons (cons bendian-to-nat (cons digits 'nil))
                            'nil)))
          (cons ':enable
                (cons (cons bendian-to-nat-as-lendian-to-nat 'nil)
                      'nil))))))
    (bendian-to-nat-of-rev-event
     (cons
      'defruled
      (cons
       bendian-to-nat-of-rev
       (cons
          (cons 'equal
                (cons (cons bendian-to-nat
                            (cons (cons 'rev (cons digits 'nil))
                                  'nil))
                      (cons (cons lendian-to-nat (cons digits 'nil))
                            'nil)))
          (cons ':enable
                (cons (cons lendian-to-nat-as-bendian-to-nat 'nil)
                      'nil))))))
    (invariant-event
     '(progn
       (theory-invariant
         (incompatible (:rewrite lendian-to-nat-as-bendian-to-nat)
                       (:rewrite bendian-to-nat-as-lendian-to-nat)))
       (theory-invariant
           (incompatible (:rewrite lendian-to-nat-as-bendian-to-nat)
                         (:rewrite lendian-to-nat-of-rev)))
       (theory-invariant
           (incompatible (:rewrite lendian-to-nat-as-bendian-to-nat)
                         (:rewrite bendian-to-nat-of-rev)))
       (theory-invariant
           (incompatible (:rewrite bendian-to-nat-as-lendian-to-nat)
                         (:rewrite lendian-to-nat-of-rev)))
       (theory-invariant
           (incompatible (:rewrite bendian-to-nat-as-lendian-to-nat)
                         (:rewrite bendian-to-nat-of-rev)))
       (theory-invariant
            (incompatible (:rewrite lendian-to-nat-of-rev)
                          (:rewrite bendian-to-nat-of-rev)))))
    (name-event
       (cons 'defxdoc
             (cons name
                   (append (and parents (list :parents parents))
                           (append (and short (list :short short))
                                   (and long (list :long long)))))))
    (table-event
     (cons
      'table
      (cons
       *defdigits-table-name*
       (cons
        (cons 'quote (cons name 'nil))
        (cons
           (cons 'quote
                 (cons (make-defdigits-info
                            :base base
                            :digits-pred digits-pred
                            :digits-fix digits-fix
                            :bendian-to-nat bendian-to-nat
                            :lendian-to-nat lendian-to-nat
                            :nat-to-bendian nat-to-bendian
                            :nat-to-lendian nat-to-lendian
                            :digits-description digits-description
                            :digits-pred-correct digits-pred-correct
                            :digits-fix-correct digits-fix-correct)
                       'nil))
           'nil))))))
   (cons
    'encapsulate
    (cons
     'nil
     (cons
      '(logic)
      (cons
       digit-pred-correct-event
       (cons
        digit-fix-correct-event
        (cons
         digit-pred-guard-correct-event
         (cons
          digit-fix-guard-correct-event
          (cons
           digits-pred-correct-event
           (cons
            digits-fix-correct-event
            (cons
             digits-pred-guard-correct-event
             (cons
              digits-fix-guard-correct-event
              (cons
               '(evmac-prepare-proofs)
               (cons
                bendian-to-nat-event
                (cons
                 lendian-to-nat-event
                 (cons
                  nat-to-bendian-event
                  (cons
                   nat-to-lendian-event
                   (cons
                    nat-to-bendian*-event
                    (cons
                     nat-to-lendian*-event
                     (cons
                      nat-to-bendian+-event
                      (cons
                       nat-to-lendian+-event
                       (cons
                        bendian-to-nat-of-nat-to-bendian-event
                        (cons
                         lendian-to-nat-of-nat-to-lendian-event
                         (cons
                          bendian-to-nat-of-nat-to-bendian*-event
                          (cons
                           lendian-to-nat-of-nat-to-lendian*-event
                           (cons
                            bendian-to-nat-of-nat-to-bendian+-event
                            (cons
                             lendian-to-nat-of-nat-to-lendian+-event
                             (cons
                              nat-to-bendian-injectivity-event
                              (cons
                               nat-to-lendian-injectivity-event
                               (cons
                                nat-to-bendian*-injectivity-event
                                (cons
                                 nat-to-lendian*-injectivity-event
                                 (cons
                                  nat-to-bendian+-injectivity-event
                                  (cons
                                   nat-to-lendian+-injectivity-event
                                   (cons
                                    nat-to-bendian-of-bendian-to-nat-event
                                    (cons
                                     nat-to-lendian-of-lendian-to-nat-event
                                     (cons
                                      nat-to-bendian*-of-bendian-to-nat-event
                                      (cons
                                       nat-to-lendian*-of-lendian-to-nat-event
                                       (cons
                                        nat-to-bendian+-of-bendian-to-nat-event
                                        (cons
                                         nat-to-lendian+-of-lendian-to-nat-event
                                         (cons
                                          bendian-to-nat-injectivity-event
                                          (cons
                                           lendian-to-nat-injectivity-event
                                           (cons
                                            bendian-to-nat-injectivity*-event
                                            (cons
                                             lendian-to-nat-injectivity*-event
                                             (cons
                                              bendian-to-nat-injectivity+-event
                                              (cons
                                               lendian-to-nat-injectivity+-event
                                               (cons
                                                len-of-nat-to-bendian*-leq-width-event
                                                (cons
                                                 len-of-nat-to-lendian*-leq-width-event
                                                 (cons
                                                  len-0-of-nat-to-bendian*-event
                                                  (cons
                                                   len-0-of-nat-to-lendian*-event
                                                   (cons
                                                    consp-pf-nat-to-bendian*-iff-not-zp-event
                                                    (cons
                                                     consp-pf-nat-to-lendian*-iff-not-zp-event
                                                     (cons
                                                      trim-bendian*-of-nat-to-bendian*-event
                                                      (cons
                                                       trim-lendian*-of-nat-to-lendian*-event
                                                       (cons
                                                        bendian-to-nat-of-cons-event
                                                        (cons
                                                         lendian-to-nat-of-cons-event
                                                         (cons
                                                          bendian-to-nat-of-append-event
                                                          (cons
                                                           lendian-to-nat-of-append-event
                                                           (cons
                                                            bendian-to-nat-of-all-zeros-event
                                                            (cons
                                                             lendian-to-nat-of-all-zeros-event
                                                             (cons
                                                              bendian-to-nat-upper-bound-event
                                                              (cons
                                                               lendian-to-nat-upper-bound-event
                                                               (cons
                                                                lendian-to-nat-as-bendian-to-nat-event
                                                                (cons
                                                                 bendian-to-nat-as-lendian-to-nat-event
                                                                 (cons
                                                                  lendian-to-nat-of-rev-event
                                                                  (cons
                                                                   bendian-to-nat-of-rev-event
                                                                   (cons
                                                                    invariant-event
                                                                    (cons
                                                                     name-event
                                                                     (cons
                                                                     
 table-event
                                                                     
 'nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))