• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • C
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
        • Builtin-defaxioms/defthms
          • Builtin-defthms
          • Builtin-defaxioms
          • Builtin-defaxioms/defthms-by-rule-classes
            • Builtin-defaxioms/defthms-without-rule-classes
            • Builtin-defaxioms/defthms-of-class-type-prescription
            • Builtin-defaxioms/defthms-of-class-rewrite
            • Builtin-defaxioms/defthms-of-class-forward-chaining
            • Builtin-defaxioms/defthms-of-class-definition
            • Builtin-defaxioms/defthms-of-class-congruence
            • Builtin-defaxioms/defthms-of-class-linear
            • Builtin-defaxioms/defthms-of-class-compound-recognizer
            • Builtin-defaxioms/defthms-of-class-tau-system
            • Builtin-defaxioms/defthms-of-class-equivalence
            • Builtin-defaxioms/defthms-of-class-elim
            • Builtin-defaxioms/defthms-of-class-well-founded-relation
            • Builtin-defaxioms/defthms-of-class-type-set-inverter
            • Builtin-defaxioms/defthms-of-class-rewrite-quoted-constant
            • Builtin-defaxioms/defthms-of-class-refinement
            • Builtin-defaxioms/defthms-of-class-generalize
            • Builtin-defaxioms/defthms-of-class-clause-processor
            • Builtin-defaxioms/defthms-of-class-built-in-clause
            • Builtin-defaxioms/defthms-of-class-meta
            • Builtin-defaxioms/defthms-of-class-induction
          • Builtin-defaxioms/defthms-by-types/functions
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Builtin-defaxioms/defthms-by-rule-classes

Builtin-defaxioms/defthms-of-class-definition

Built-in axioms and theorems of the :definition rule class.

Theorem: apply$-warrant-do$-definition

(defthm apply$-warrant-do$-definition
 (equal
  (apply$-warrant-do$)
  (let ((args (apply$-warrant-do$-witness)))
   (implies
     (and (tamep-functionp (car args))
          (tamep-functionp (car (cdr (cdr args))))
          (tamep-functionp (car (cdr (cdr (cdr args))))))
     (and (equal (badge-userfn 'do$)
                 '(apply$-badge 6 1 :fn nil :fn :fn nil nil))
          (equal (apply$-userfn 'do$ args)
                 (do$ (car args)
                      (car (cdr args))
                      (car (cdr (cdr args)))
                      (car (cdr (cdr (cdr args))))
                      (car (cdr (cdr (cdr (cdr args)))))
                      (car (cdr (cdr (cdr (cdr (cdr args))))))))))))
 :rule-classes :definition)

Theorem: apply$-warrant-loop$-default-values-definition

(defthm apply$-warrant-loop$-default-values-definition
  (equal (apply$-warrant-loop$-default-values)
         (let ((args (apply$-warrant-loop$-default-values-witness)))
           (and (equal (badge-userfn 'loop$-default-values)
                       '(apply$-badge 2 1 . t))
                (equal (apply$-userfn 'loop$-default-values
                                      args)
                       (loop$-default-values (car args)
                                             (car (cdr args)))))))
  :rule-classes :definition)

Theorem: apply$-warrant-loop$-default-values1-definition

(defthm apply$-warrant-loop$-default-values1-definition
 (equal (apply$-warrant-loop$-default-values1)
        (let ((args (apply$-warrant-loop$-default-values1-witness)))
          (and (equal (badge-userfn 'loop$-default-values1)
                      '(apply$-badge 2 1 . t))
               (equal (apply$-userfn 'loop$-default-values1
                                     args)
                      (loop$-default-values1 (car args)
                                             (car (cdr args)))))))
 :rule-classes :definition)

Theorem: apply$-warrant-eviscerate-do$-alist-definition

(defthm apply$-warrant-eviscerate-do$-alist-definition
  (equal (apply$-warrant-eviscerate-do$-alist)
         (let ((args (apply$-warrant-eviscerate-do$-alist-witness)))
           (and (equal (badge-userfn 'eviscerate-do$-alist)
                       '(apply$-badge 2 1 . t))
                (equal (apply$-userfn 'eviscerate-do$-alist
                                      args)
                       (eviscerate-do$-alist (car args)
                                             (car (cdr args)))))))
  :rule-classes :definition)

Theorem: apply$-warrant-stobj-print-name-definition

(defthm apply$-warrant-stobj-print-name-definition
  (equal (apply$-warrant-stobj-print-name)
         (let ((args (apply$-warrant-stobj-print-name-witness)))
           (and (equal (badge-userfn 'stobj-print-name)
                       '(apply$-badge 1 1 . t))
                (equal (apply$-userfn 'stobj-print-name args)
                       (stobj-print-name (car args))))))
  :rule-classes :definition)

Theorem: apply$-warrant-lexp-definition

(defthm apply$-warrant-lexp-definition
  (equal (apply$-warrant-lexp)
         (let ((args (apply$-warrant-lexp-witness)))
           (and (equal (badge-userfn 'lexp)
                       '(apply$-badge 1 1 . t))
                (equal (apply$-userfn 'lexp args)
                       (lexp (car args))))))
  :rule-classes :definition)

Theorem: apply$-warrant-lex-fix-definition

(defthm apply$-warrant-lex-fix-definition
  (equal (apply$-warrant-lex-fix)
         (let ((args (apply$-warrant-lex-fix-witness)))
           (and (equal (badge-userfn 'lex-fix)
                       '(apply$-badge 1 1 . t))
                (equal (apply$-userfn 'lex-fix args)
                       (lex-fix (car args))))))
  :rule-classes :definition)

Theorem: apply$-warrant-nfix-list-definition

(defthm apply$-warrant-nfix-list-definition
  (equal (apply$-warrant-nfix-list)
         (let ((args (apply$-warrant-nfix-list-witness)))
           (and (equal (badge-userfn 'nfix-list)
                       '(apply$-badge 1 1 . t))
                (equal (apply$-userfn 'nfix-list args)
                       (nfix-list (car args))))))
  :rule-classes :definition)

Theorem: apply$-warrant-l<-definition

(defthm apply$-warrant-l<-definition
  (equal (apply$-warrant-l<)
         (let ((args (apply$-warrant-l<-witness)))
           (and (equal (badge-userfn 'l<)
                       '(apply$-badge 2 1 . t))
                (equal (apply$-userfn 'l< args)
                       (l< (car args) (car (cdr args)))))))
  :rule-classes :definition)

Theorem: apply$-warrant-d<-definition

(defthm apply$-warrant-d<-definition
  (equal (apply$-warrant-d<)
         (let ((args (apply$-warrant-d<-witness)))
           (and (equal (badge-userfn 'd<)
                       '(apply$-badge 2 1 . t))
                (equal (apply$-userfn 'd< args)
                       (d< (car args) (car (cdr args)))))))
  :rule-classes :definition)

Theorem: apply$-warrant-mempos-definition

(defthm apply$-warrant-mempos-definition
  (equal (apply$-warrant-mempos)
         (let ((args (apply$-warrant-mempos-witness)))
           (and (equal (badge-userfn 'mempos)
                       '(apply$-badge 2 1 . t))
                (equal (apply$-userfn 'mempos args)
                       (mempos (car args) (car (cdr args)))))))
  :rule-classes :definition)

Theorem: apply$-warrant-append$+-definition

(defthm apply$-warrant-append$+-definition
  (equal
       (apply$-warrant-append$+)
       (let ((args (apply$-warrant-append$+-witness)))
         (implies (tamep-functionp (car args))
                  (and (equal (badge-userfn 'append$+)
                              '(apply$-badge 3 1 :fn nil nil))
                       (equal (apply$-userfn 'append$+ args)
                              (append$+ (car args)
                                        (car (cdr args))
                                        (car (cdr (cdr args)))))))))
  :rule-classes :definition)

Theorem: apply$-warrant-append$+-ac-definition

(defthm apply$-warrant-append$+-ac-definition
 (equal
  (apply$-warrant-append$+-ac)
  (let ((args (apply$-warrant-append$+-ac-witness)))
    (implies
         (tamep-functionp (car args))
         (and (equal (badge-userfn 'append$+-ac)
                     '(apply$-badge 4 1 :fn nil nil nil))
              (equal (apply$-userfn 'append$+-ac args)
                     (append$+-ac (car args)
                                  (car (cdr args))
                                  (car (cdr (cdr args)))
                                  (car (cdr (cdr (cdr args))))))))))
 :rule-classes :definition)

Theorem: apply$-warrant-append$-definition

(defthm apply$-warrant-append$-definition
  (equal (apply$-warrant-append$)
         (let ((args (apply$-warrant-append$-witness)))
           (implies (tamep-functionp (car args))
                    (and (equal (badge-userfn 'append$)
                                '(apply$-badge 2 1 :fn nil))
                         (equal (apply$-userfn 'append$ args)
                                (append$ (car args)
                                         (car (cdr args))))))))
  :rule-classes :definition)

Theorem: apply$-warrant-append$-ac-definition

(defthm apply$-warrant-append$-ac-definition
 (equal
     (apply$-warrant-append$-ac)
     (let ((args (apply$-warrant-append$-ac-witness)))
       (implies (tamep-functionp (car args))
                (and (equal (badge-userfn 'append$-ac)
                            '(apply$-badge 3 1 :fn nil nil))
                     (equal (apply$-userfn 'append$-ac args)
                            (append$-ac (car args)
                                        (car (cdr args))
                                        (car (cdr (cdr args)))))))))
 :rule-classes :definition)

Theorem: apply$-warrant-collect$+-definition

(defthm apply$-warrant-collect$+-definition
 (equal
      (apply$-warrant-collect$+)
      (let ((args (apply$-warrant-collect$+-witness)))
        (implies (tamep-functionp (car args))
                 (and (equal (badge-userfn 'collect$+)
                             '(apply$-badge 3 1 :fn nil nil))
                      (equal (apply$-userfn 'collect$+ args)
                             (collect$+ (car args)
                                        (car (cdr args))
                                        (car (cdr (cdr args)))))))))
 :rule-classes :definition)

Theorem: apply$-warrant-collect$+-ac-definition

(defthm apply$-warrant-collect$+-ac-definition
 (equal
  (apply$-warrant-collect$+-ac)
  (let ((args (apply$-warrant-collect$+-ac-witness)))
   (implies
        (tamep-functionp (car args))
        (and (equal (badge-userfn 'collect$+-ac)
                    '(apply$-badge 4 1 :fn nil nil nil))
             (equal (apply$-userfn 'collect$+-ac args)
                    (collect$+-ac (car args)
                                  (car (cdr args))
                                  (car (cdr (cdr args)))
                                  (car (cdr (cdr (cdr args))))))))))
 :rule-classes :definition)

Theorem: apply$-warrant-collect$-definition

(defthm apply$-warrant-collect$-definition
  (equal (apply$-warrant-collect$)
         (let ((args (apply$-warrant-collect$-witness)))
           (implies (tamep-functionp (car args))
                    (and (equal (badge-userfn 'collect$)
                                '(apply$-badge 2 1 :fn nil))
                         (equal (apply$-userfn 'collect$ args)
                                (collect$ (car args)
                                          (car (cdr args))))))))
  :rule-classes :definition)

Theorem: apply$-warrant-collect$-ac-definition

(defthm apply$-warrant-collect$-ac-definition
 (equal
    (apply$-warrant-collect$-ac)
    (let ((args (apply$-warrant-collect$-ac-witness)))
      (implies (tamep-functionp (car args))
               (and (equal (badge-userfn 'collect$-ac)
                           '(apply$-badge 3 1 :fn nil nil))
                    (equal (apply$-userfn 'collect$-ac args)
                           (collect$-ac (car args)
                                        (car (cdr args))
                                        (car (cdr (cdr args)))))))))
 :rule-classes :definition)

Theorem: apply$-warrant-thereis$+-definition

(defthm apply$-warrant-thereis$+-definition
 (equal
      (apply$-warrant-thereis$+)
      (let ((args (apply$-warrant-thereis$+-witness)))
        (implies (tamep-functionp (car args))
                 (and (equal (badge-userfn 'thereis$+)
                             '(apply$-badge 3 1 :fn nil nil))
                      (equal (apply$-userfn 'thereis$+ args)
                             (thereis$+ (car args)
                                        (car (cdr args))
                                        (car (cdr (cdr args)))))))))
 :rule-classes :definition)

Theorem: apply$-warrant-thereis$-definition

(defthm apply$-warrant-thereis$-definition
  (equal (apply$-warrant-thereis$)
         (let ((args (apply$-warrant-thereis$-witness)))
           (implies (tamep-functionp (car args))
                    (and (equal (badge-userfn 'thereis$)
                                '(apply$-badge 2 1 :fn nil))
                         (equal (apply$-userfn 'thereis$ args)
                                (thereis$ (car args)
                                          (car (cdr args))))))))
  :rule-classes :definition)

Theorem: apply$-warrant-always$+-definition

(defthm apply$-warrant-always$+-definition
  (equal
       (apply$-warrant-always$+)
       (let ((args (apply$-warrant-always$+-witness)))
         (implies (tamep-functionp (car args))
                  (and (equal (badge-userfn 'always$+)
                              '(apply$-badge 3 1 :fn nil nil))
                       (equal (apply$-userfn 'always$+ args)
                              (always$+ (car args)
                                        (car (cdr args))
                                        (car (cdr (cdr args)))))))))
  :rule-classes :definition)

Theorem: apply$-warrant-always$-definition

(defthm apply$-warrant-always$-definition
  (equal (apply$-warrant-always$)
         (let ((args (apply$-warrant-always$-witness)))
           (implies (tamep-functionp (car args))
                    (and (equal (badge-userfn 'always$)
                                '(apply$-badge 2 1 :fn nil))
                         (equal (apply$-userfn 'always$ args)
                                (always$ (car args)
                                         (car (cdr args))))))))
  :rule-classes :definition)

Theorem: apply$-warrant-sum$+-definition

(defthm apply$-warrant-sum$+-definition
  (equal (apply$-warrant-sum$+)
         (let ((args (apply$-warrant-sum$+-witness)))
           (implies (tamep-functionp (car args))
                    (and (equal (badge-userfn 'sum$+)
                                '(apply$-badge 3 1 :fn nil nil))
                         (equal (apply$-userfn 'sum$+ args)
                                (sum$+ (car args)
                                       (car (cdr args))
                                       (car (cdr (cdr args)))))))))
  :rule-classes :definition)

Theorem: apply$-warrant-sum$+-ac-definition

(defthm apply$-warrant-sum$+-ac-definition
 (equal
  (apply$-warrant-sum$+-ac)
  (let ((args (apply$-warrant-sum$+-ac-witness)))
   (implies (tamep-functionp (car args))
            (and (equal (badge-userfn 'sum$+-ac)
                        '(apply$-badge 4 1 :fn nil nil nil))
                 (equal (apply$-userfn 'sum$+-ac args)
                        (sum$+-ac (car args)
                                  (car (cdr args))
                                  (car (cdr (cdr args)))
                                  (car (cdr (cdr (cdr args))))))))))
 :rule-classes :definition)

Theorem: apply$-warrant-sum$-definition

(defthm apply$-warrant-sum$-definition
 (equal
      (apply$-warrant-sum$)
      (let ((args (apply$-warrant-sum$-witness)))
        (implies (tamep-functionp (car args))
                 (and (equal (badge-userfn 'sum$)
                             '(apply$-badge 2 1 :fn nil))
                      (equal (apply$-userfn 'sum$ args)
                             (sum$ (car args) (car (cdr args))))))))
 :rule-classes :definition)

Theorem: apply$-warrant-sum$-ac-definition

(defthm apply$-warrant-sum$-ac-definition
 (equal (apply$-warrant-sum$-ac)
        (let ((args (apply$-warrant-sum$-ac-witness)))
          (implies (tamep-functionp (car args))
                   (and (equal (badge-userfn 'sum$-ac)
                               '(apply$-badge 3 1 :fn nil nil))
                        (equal (apply$-userfn 'sum$-ac args)
                               (sum$-ac (car args)
                                        (car (cdr args))
                                        (car (cdr (cdr args)))))))))
 :rule-classes :definition)

Theorem: apply$-warrant-when$+-definition

(defthm apply$-warrant-when$+-definition
  (equal (apply$-warrant-when$+)
         (let ((args (apply$-warrant-when$+-witness)))
           (implies (tamep-functionp (car args))
                    (and (equal (badge-userfn 'when$+)
                                '(apply$-badge 3 1 :fn nil nil))
                         (equal (apply$-userfn 'when$+ args)
                                (when$+ (car args)
                                        (car (cdr args))
                                        (car (cdr (cdr args)))))))))
  :rule-classes :definition)

Theorem: apply$-warrant-when$+-ac-definition

(defthm apply$-warrant-when$+-ac-definition
 (equal
    (apply$-warrant-when$+-ac)
    (let ((args (apply$-warrant-when$+-ac-witness)))
      (implies
           (tamep-functionp (car args))
           (and (equal (badge-userfn 'when$+-ac)
                       '(apply$-badge 4 1 :fn nil nil nil))
                (equal (apply$-userfn 'when$+-ac args)
                       (when$+-ac (car args)
                                  (car (cdr args))
                                  (car (cdr (cdr args)))
                                  (car (cdr (cdr (cdr args))))))))))
 :rule-classes :definition)

Theorem: apply$-warrant-when$-definition

(defthm apply$-warrant-when$-definition
 (equal
     (apply$-warrant-when$)
     (let ((args (apply$-warrant-when$-witness)))
       (implies (tamep-functionp (car args))
                (and (equal (badge-userfn 'when$)
                            '(apply$-badge 2 1 :fn nil))
                     (equal (apply$-userfn 'when$ args)
                            (when$ (car args) (car (cdr args))))))))
 :rule-classes :definition)

Theorem: apply$-warrant-when$-ac-definition

(defthm apply$-warrant-when$-ac-definition
  (equal
       (apply$-warrant-when$-ac)
       (let ((args (apply$-warrant-when$-ac-witness)))
         (implies (tamep-functionp (car args))
                  (and (equal (badge-userfn 'when$-ac)
                              '(apply$-badge 3 1 :fn nil nil))
                       (equal (apply$-userfn 'when$-ac args)
                              (when$-ac (car args)
                                        (car (cdr args))
                                        (car (cdr (cdr args)))))))))
  :rule-classes :definition)

Theorem: apply$-warrant-until$+-definition

(defthm apply$-warrant-until$+-definition
 (equal (apply$-warrant-until$+)
        (let ((args (apply$-warrant-until$+-witness)))
          (implies (tamep-functionp (car args))
                   (and (equal (badge-userfn 'until$+)
                               '(apply$-badge 3 1 :fn nil nil))
                        (equal (apply$-userfn 'until$+ args)
                               (until$+ (car args)
                                        (car (cdr args))
                                        (car (cdr (cdr args)))))))))
 :rule-classes :definition)

Theorem: apply$-warrant-until$+-ac-definition

(defthm apply$-warrant-until$+-ac-definition
 (equal
   (apply$-warrant-until$+-ac)
   (let ((args (apply$-warrant-until$+-ac-witness)))
     (implies
          (tamep-functionp (car args))
          (and (equal (badge-userfn 'until$+-ac)
                      '(apply$-badge 4 1 :fn nil nil nil))
               (equal (apply$-userfn 'until$+-ac args)
                      (until$+-ac (car args)
                                  (car (cdr args))
                                  (car (cdr (cdr args)))
                                  (car (cdr (cdr (cdr args))))))))))
 :rule-classes :definition)

Theorem: apply$-warrant-until$-definition

(defthm apply$-warrant-until$-definition
  (equal (apply$-warrant-until$)
         (let ((args (apply$-warrant-until$-witness)))
           (implies (tamep-functionp (car args))
                    (and (equal (badge-userfn 'until$)
                                '(apply$-badge 2 1 :fn nil))
                         (equal (apply$-userfn 'until$ args)
                                (until$ (car args)
                                        (car (cdr args))))))))
  :rule-classes :definition)

Theorem: apply$-warrant-until$-ac-definition

(defthm apply$-warrant-until$-ac-definition
 (equal
      (apply$-warrant-until$-ac)
      (let ((args (apply$-warrant-until$-ac-witness)))
        (implies (tamep-functionp (car args))
                 (and (equal (badge-userfn 'until$-ac)
                             '(apply$-badge 3 1 :fn nil nil))
                      (equal (apply$-userfn 'until$-ac args)
                             (until$-ac (car args)
                                        (car (cdr args))
                                        (car (cdr (cdr args)))))))))
 :rule-classes :definition)