• 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-rewrite

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

Definition: bad-atom<=-transitive

(defaxiom bad-atom<=-transitive
  (implies (and (bad-atom<= x y)
                (bad-atom<= y z)
                (bad-atom x)
                (bad-atom y)
                (bad-atom z))
           (bad-atom<= x z))
  :rule-classes ((:rewrite :match-free :all)))

Definition: char-code-code-char-is-identity

(defaxiom char-code-code-char-is-identity
  (implies (and (integerp n) (<= 0 n) (< n 256))
           (equal (char-code (code-char n)) n)))

Definition: code-char-char-code-is-identity

(defaxiom code-char-char-code-is-identity
  (implies (characterp c)
           (equal (code-char (char-code c)) c)))

Definition: keyword-package

(defaxiom keyword-package
  (equal (pkg-imports "KEYWORD") nil))

Definition: acl2-package

(defaxiom acl2-package
  (equal (pkg-imports "ACL2")
         *common-lisp-symbols-from-main-lisp-package*))

Definition: acl2-output-channel-package

(defaxiom acl2-output-channel-package
  (equal (pkg-imports "ACL2-OUTPUT-CHANNEL")
         nil))

Definition: acl2-input-channel-package

(defaxiom acl2-input-channel-package
  (equal (pkg-imports "ACL2-INPUT-CHANNEL")
         nil))

Definition: no-duplicatesp-eq-pkg-imports

(defaxiom no-duplicatesp-eq-pkg-imports
  (no-duplicatesp-eq (pkg-imports pkg))
  :rule-classes :rewrite)

Definition: intern-in-package-of-symbol-is-identity

(defaxiom intern-in-package-of-symbol-is-identity
 (implies
  (and (stringp x)
       (symbolp y)
       (member-symbol-name x
                           (pkg-imports (symbol-package-name y))))
  (equal
   (intern-in-package-of-symbol x y)
   (car
      (member-symbol-name x
                          (pkg-imports (symbol-package-name y)))))))

Definition: symbol-package-name-intern-in-package-of-symbol

(defaxiom symbol-package-name-intern-in-package-of-symbol
 (implies
  (and
   (stringp x)
   (symbolp y)
   (not (member-symbol-name x
                            (pkg-imports (symbol-package-name y)))))
  (equal (symbol-package-name (intern-in-package-of-symbol x y))
         (symbol-package-name y))))

Definition: symbol-name-intern-in-package-of-symbol

(defaxiom symbol-name-intern-in-package-of-symbol
 (implies
     (and (stringp s) (symbolp any-symbol))
     (equal (symbol-name (intern-in-package-of-symbol s any-symbol))
            s)))

Definition: symbol-package-name-pkg-witness-name

(defaxiom symbol-package-name-pkg-witness-name
  (equal (symbol-package-name (pkg-witness pkg-name))
         (if (and (stringp pkg-name)
                  (not (equal pkg-name "")))
             pkg-name
           "ACL2")))

Definition: symbol-name-pkg-witness

(defaxiom symbol-name-pkg-witness
  (equal (symbol-name (pkg-witness pkg-name))
         *pkg-witness-name*))

Definition: intern-in-package-of-symbol-symbol-name

(defaxiom intern-in-package-of-symbol-symbol-name
  (implies (and (symbolp x)
                (equal (symbol-package-name x)
                       (symbol-package-name y)))
           (equal (intern-in-package-of-symbol (symbol-name x)
                                               y)
                  x)))

Definition: character-listp-coerce

(defaxiom character-listp-coerce
 (character-listp (coerce str 'list))
 :rule-classes
 (:rewrite (:forward-chaining :trigger-terms ((coerce str 'list)))))

Definition: coerce-inverse-2

(defaxiom coerce-inverse-2
  (implies (stringp x)
           (equal (coerce (coerce x 'list) 'string)
                  x)))

Definition: coerce-inverse-1

(defaxiom coerce-inverse-1
  (implies (character-listp x)
           (equal (coerce (coerce x 'string) 'list)
                  x)))

Definition: imagpart-complex

(defaxiom imagpart-complex
  (implies (and (real/rationalp x)
                (real/rationalp y))
           (equal (imagpart (complex x y)) y)))

Definition: realpart-complex

(defaxiom realpart-complex
  (implies (and (real/rationalp x)
                (real/rationalp y))
           (equal (realpart (complex x y)) x)))

Definition: realpart-imagpart-elim

(defaxiom realpart-imagpart-elim
  (implies (acl2-numberp x)
           (equal (complex (realpart x) (imagpart x))
                  x))
  :rule-classes (:rewrite :elim))

Definition: complex-definition

(defaxiom complex-definition
  (implies (and (real/rationalp x)
                (real/rationalp y))
           (equal (complex x y) (+ x (* #C(0 1) y)))))

Definition: rational-implies2

(defaxiom rational-implies2
  (implies (rationalp x)
           (equal (* (/ (denominator x)) (numerator x))
                  x)))

Definition: distributivity

(defaxiom distributivity
  (equal (* x (+ y z))
         (+ (* x y) (* x z))))

Definition: inverse-of-*

(defaxiom inverse-of-*
  (implies (and (acl2-numberp x) (not (equal x 0)))
           (equal (* x (/ x)) 1)))

Definition: unicity-of-1

(defaxiom unicity-of-1
  (equal (* 1 x) (fix x)))

Definition: commutativity-of-*

(defaxiom commutativity-of-*
  (equal (* x y) (* y x)))

Definition: associativity-of-*

(defaxiom associativity-of-*
  (equal (* (* x y) z) (* x (* y z))))

Definition: inverse-of-+

(defaxiom inverse-of-+
  (equal (+ x (- x)) 0))

Definition: unicity-of-0

(defaxiom unicity-of-0
  (equal (+ 0 x) (fix x)))

Definition: commutativity-of-+

(defaxiom commutativity-of-+
  (equal (+ x y) (+ y x)))

Definition: associativity-of-+

(defaxiom associativity-of-+
  (equal (+ (+ x y) z) (+ x (+ y z))))

Definition: cons-equal

(defaxiom cons-equal
  (equal (equal (cons x1 y1) (cons x2 y2))
         (and (equal x1 x2) (equal y1 y2))))

Definition: cdr-cons

(defaxiom cdr-cons
  (equal (cdr (cons x y)) y))

Definition: car-cons

(defaxiom car-cons
  (equal (car (cons x y)) x))

Theorem: apply$-do$

(defthm apply$-do$
 (and
     (implies (force (apply$-warrant-do$))
              (equal (badge 'do$)
                     '(apply$-badge 6 1 :fn nil :fn :fn nil nil)))
     (implies
          (and (force (apply$-warrant-do$))
               (and (tamep-functionp (car args))
                    (tamep-functionp (car (cdr (cdr args))))
                    (tamep-functionp (car (cdr (cdr (cdr args)))))))
          (equal (apply$ '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)))))))))))

Theorem: apply$-warrant-do$-necc

(defthm apply$-warrant-do$-necc
 (implies
  (not
   (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)))))))))))
  (not (apply$-warrant-do$))))

Theorem: apply$-loop$-default-values

(defthm apply$-loop$-default-values
  (implies (force (apply$-warrant-loop$-default-values))
           (and (equal (badge 'loop$-default-values)
                       '(apply$-badge 2 1 . t))
                (equal (apply$ 'loop$-default-values args)
                       (loop$-default-values (car args)
                                             (car (cdr args)))))))

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

(defthm apply$-warrant-loop$-default-values-necc
  (implies
       (not (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))))))
       (not (apply$-warrant-loop$-default-values))))

Theorem: apply$-loop$-default-values1

(defthm apply$-loop$-default-values1
  (implies (force (apply$-warrant-loop$-default-values1))
           (and (equal (badge 'loop$-default-values1)
                       '(apply$-badge 2 1 . t))
                (equal (apply$ 'loop$-default-values1 args)
                       (loop$-default-values1 (car args)
                                              (car (cdr args)))))))

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

(defthm apply$-warrant-loop$-default-values1-necc
  (implies
       (not (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))))))
       (not (apply$-warrant-loop$-default-values1))))

Theorem: apply$-eviscerate-do$-alist

(defthm apply$-eviscerate-do$-alist
  (implies (force (apply$-warrant-eviscerate-do$-alist))
           (and (equal (badge 'eviscerate-do$-alist)
                       '(apply$-badge 2 1 . t))
                (equal (apply$ 'eviscerate-do$-alist args)
                       (eviscerate-do$-alist (car args)
                                             (car (cdr args)))))))

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

(defthm apply$-warrant-eviscerate-do$-alist-necc
  (implies
       (not (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))))))
       (not (apply$-warrant-eviscerate-do$-alist))))

Theorem: apply$-stobj-print-name

(defthm apply$-stobj-print-name
  (implies (force (apply$-warrant-stobj-print-name))
           (and (equal (badge 'stobj-print-name)
                       '(apply$-badge 1 1 . t))
                (equal (apply$ 'stobj-print-name args)
                       (stobj-print-name (car args))))))

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

(defthm apply$-warrant-stobj-print-name-necc
  (implies (not (and (equal (badge-userfn 'stobj-print-name)
                            '(apply$-badge 1 1 . t))
                     (equal (apply$-userfn 'stobj-print-name args)
                            (stobj-print-name (car args)))))
           (not (apply$-warrant-stobj-print-name))))

Theorem: apply$-lexp

(defthm apply$-lexp
  (implies (force (apply$-warrant-lexp))
           (and (equal (badge 'lexp)
                       '(apply$-badge 1 1 . t))
                (equal (apply$ 'lexp args)
                       (lexp (car args))))))

Theorem: apply$-warrant-lexp-necc

(defthm apply$-warrant-lexp-necc
  (implies (not (and (equal (badge-userfn 'lexp)
                            '(apply$-badge 1 1 . t))
                     (equal (apply$-userfn 'lexp args)
                            (lexp (car args)))))
           (not (apply$-warrant-lexp))))

Theorem: apply$-lex-fix

(defthm apply$-lex-fix
  (implies (force (apply$-warrant-lex-fix))
           (and (equal (badge 'lex-fix)
                       '(apply$-badge 1 1 . t))
                (equal (apply$ 'lex-fix args)
                       (lex-fix (car args))))))

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

(defthm apply$-warrant-lex-fix-necc
  (implies (not (and (equal (badge-userfn 'lex-fix)
                            '(apply$-badge 1 1 . t))
                     (equal (apply$-userfn 'lex-fix args)
                            (lex-fix (car args)))))
           (not (apply$-warrant-lex-fix))))

Theorem: apply$-nfix-list

(defthm apply$-nfix-list
  (implies (force (apply$-warrant-nfix-list))
           (and (equal (badge 'nfix-list)
                       '(apply$-badge 1 1 . t))
                (equal (apply$ 'nfix-list args)
                       (nfix-list (car args))))))

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

(defthm apply$-warrant-nfix-list-necc
  (implies (not (and (equal (badge-userfn 'nfix-list)
                            '(apply$-badge 1 1 . t))
                     (equal (apply$-userfn 'nfix-list args)
                            (nfix-list (car args)))))
           (not (apply$-warrant-nfix-list))))

Theorem: apply$-l<

(defthm apply$-l<
  (implies (force (apply$-warrant-l<))
           (and (equal (badge 'l<)
                       '(apply$-badge 2 1 . t))
                (equal (apply$ 'l< args)
                       (l< (car args) (car (cdr args)))))))

Theorem: apply$-warrant-l<-necc

(defthm apply$-warrant-l<-necc
  (implies (not (and (equal (badge-userfn 'l<)
                            '(apply$-badge 2 1 . t))
                     (equal (apply$-userfn 'l< args)
                            (l< (car args) (car (cdr args))))))
           (not (apply$-warrant-l<))))

Theorem: apply$-d<

(defthm apply$-d<
  (implies (force (apply$-warrant-d<))
           (and (equal (badge 'd<)
                       '(apply$-badge 2 1 . t))
                (equal (apply$ 'd< args)
                       (d< (car args) (car (cdr args)))))))

Theorem: apply$-warrant-d<-necc

(defthm apply$-warrant-d<-necc
  (implies (not (and (equal (badge-userfn 'd<)
                            '(apply$-badge 2 1 . t))
                     (equal (apply$-userfn 'd< args)
                            (d< (car args) (car (cdr args))))))
           (not (apply$-warrant-d<))))

Theorem: apply$-mempos

(defthm apply$-mempos
  (implies (force (apply$-warrant-mempos))
           (and (equal (badge 'mempos)
                       '(apply$-badge 2 1 . t))
                (equal (apply$ 'mempos args)
                       (mempos (car args) (car (cdr args)))))))

Theorem: apply$-warrant-mempos-necc

(defthm apply$-warrant-mempos-necc
  (implies (not (and (equal (badge-userfn 'mempos)
                            '(apply$-badge 2 1 . t))
                     (equal (apply$-userfn 'mempos args)
                            (mempos (car args) (car (cdr args))))))
           (not (apply$-warrant-mempos))))

Theorem: apply$-append$+

(defthm apply$-append$+
  (and (implies (force (apply$-warrant-append$+))
                (equal (badge 'append$+)
                       '(apply$-badge 3 1 :fn nil nil)))
       (implies (and (force (apply$-warrant-append$+))
                     (tamep-functionp (car args)))
                (equal (apply$ 'append$+ args)
                       (append$+ (car args)
                                 (car (cdr args))
                                 (car (cdr (cdr args))))))))

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

(defthm apply$-warrant-append$+-necc
 (implies
     (not (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))))))))
     (not (apply$-warrant-append$+))))

Theorem: apply$-append$+-ac

(defthm apply$-append$+-ac
 (and (implies (force (apply$-warrant-append$+-ac))
               (equal (badge 'append$+-ac)
                      '(apply$-badge 4 1 :fn nil nil nil)))
      (implies (and (force (apply$-warrant-append$+-ac))
                    (tamep-functionp (car args)))
               (equal (apply$ 'append$+-ac args)
                      (append$+-ac (car args)
                                   (car (cdr args))
                                   (car (cdr (cdr args)))
                                   (car (cdr (cdr (cdr args)))))))))

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

(defthm apply$-warrant-append$+-ac-necc
 (implies
  (not
     (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)))))))))
  (not (apply$-warrant-append$+-ac))))

Theorem: apply$-append$

(defthm apply$-append$
  (and (implies (force (apply$-warrant-append$))
                (equal (badge 'append$)
                       '(apply$-badge 2 1 :fn nil)))
       (implies (and (force (apply$-warrant-append$))
                     (tamep-functionp (car args)))
                (equal (apply$ 'append$ args)
                       (append$ (car args)
                                (car (cdr args)))))))

Theorem: apply$-warrant-append$-necc

(defthm apply$-warrant-append$-necc
  (implies (not (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)))))))
           (not (apply$-warrant-append$))))

Theorem: apply$-append$-ac

(defthm apply$-append$-ac
  (and (implies (force (apply$-warrant-append$-ac))
                (equal (badge 'append$-ac)
                       '(apply$-badge 3 1 :fn nil nil)))
       (implies (and (force (apply$-warrant-append$-ac))
                     (tamep-functionp (car args)))
                (equal (apply$ 'append$-ac args)
                       (append$-ac (car args)
                                   (car (cdr args))
                                   (car (cdr (cdr args))))))))

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

(defthm apply$-warrant-append$-ac-necc
 (implies
   (not (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))))))))
   (not (apply$-warrant-append$-ac))))

Theorem: apply$-collect$+

(defthm apply$-collect$+
  (and (implies (force (apply$-warrant-collect$+))
                (equal (badge 'collect$+)
                       '(apply$-badge 3 1 :fn nil nil)))
       (implies (and (force (apply$-warrant-collect$+))
                     (tamep-functionp (car args)))
                (equal (apply$ 'collect$+ args)
                       (collect$+ (car args)
                                  (car (cdr args))
                                  (car (cdr (cdr args))))))))

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

(defthm apply$-warrant-collect$+-necc
 (implies
    (not (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))))))))
    (not (apply$-warrant-collect$+))))

Theorem: apply$-collect$+-ac

(defthm apply$-collect$+-ac
 (and
     (implies (force (apply$-warrant-collect$+-ac))
              (equal (badge 'collect$+-ac)
                     '(apply$-badge 4 1 :fn nil nil nil)))
     (implies (and (force (apply$-warrant-collect$+-ac))
                   (tamep-functionp (car args)))
              (equal (apply$ 'collect$+-ac args)
                     (collect$+-ac (car args)
                                   (car (cdr args))
                                   (car (cdr (cdr args)))
                                   (car (cdr (cdr (cdr args)))))))))

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

(defthm apply$-warrant-collect$+-ac-necc
 (implies
  (not
    (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)))))))))
  (not (apply$-warrant-collect$+-ac))))

Theorem: apply$-collect$

(defthm apply$-collect$
  (and (implies (force (apply$-warrant-collect$))
                (equal (badge 'collect$)
                       '(apply$-badge 2 1 :fn nil)))
       (implies (and (force (apply$-warrant-collect$))
                     (tamep-functionp (car args)))
                (equal (apply$ 'collect$ args)
                       (collect$ (car args)
                                 (car (cdr args)))))))

Theorem: apply$-warrant-collect$-necc

(defthm apply$-warrant-collect$-necc
  (implies (not (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)))))))
           (not (apply$-warrant-collect$))))

Theorem: apply$-collect$-ac

(defthm apply$-collect$-ac
  (and (implies (force (apply$-warrant-collect$-ac))
                (equal (badge 'collect$-ac)
                       '(apply$-badge 3 1 :fn nil nil)))
       (implies (and (force (apply$-warrant-collect$-ac))
                     (tamep-functionp (car args)))
                (equal (apply$ 'collect$-ac args)
                       (collect$-ac (car args)
                                    (car (cdr args))
                                    (car (cdr (cdr args))))))))

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

(defthm apply$-warrant-collect$-ac-necc
 (implies
  (not (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))))))))
  (not (apply$-warrant-collect$-ac))))

Theorem: apply$-thereis$+

(defthm apply$-thereis$+
  (and (implies (force (apply$-warrant-thereis$+))
                (equal (badge 'thereis$+)
                       '(apply$-badge 3 1 :fn nil nil)))
       (implies (and (force (apply$-warrant-thereis$+))
                     (tamep-functionp (car args)))
                (equal (apply$ 'thereis$+ args)
                       (thereis$+ (car args)
                                  (car (cdr args))
                                  (car (cdr (cdr args))))))))

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

(defthm apply$-warrant-thereis$+-necc
 (implies
    (not (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))))))))
    (not (apply$-warrant-thereis$+))))

Theorem: apply$-thereis$

(defthm apply$-thereis$
  (and (implies (force (apply$-warrant-thereis$))
                (equal (badge 'thereis$)
                       '(apply$-badge 2 1 :fn nil)))
       (implies (and (force (apply$-warrant-thereis$))
                     (tamep-functionp (car args)))
                (equal (apply$ 'thereis$ args)
                       (thereis$ (car args)
                                 (car (cdr args)))))))

Theorem: apply$-warrant-thereis$-necc

(defthm apply$-warrant-thereis$-necc
  (implies (not (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)))))))
           (not (apply$-warrant-thereis$))))

Theorem: apply$-always$+

(defthm apply$-always$+
  (and (implies (force (apply$-warrant-always$+))
                (equal (badge 'always$+)
                       '(apply$-badge 3 1 :fn nil nil)))
       (implies (and (force (apply$-warrant-always$+))
                     (tamep-functionp (car args)))
                (equal (apply$ 'always$+ args)
                       (always$+ (car args)
                                 (car (cdr args))
                                 (car (cdr (cdr args))))))))

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

(defthm apply$-warrant-always$+-necc
 (implies
     (not (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))))))))
     (not (apply$-warrant-always$+))))

Theorem: apply$-always$

(defthm apply$-always$
  (and (implies (force (apply$-warrant-always$))
                (equal (badge 'always$)
                       '(apply$-badge 2 1 :fn nil)))
       (implies (and (force (apply$-warrant-always$))
                     (tamep-functionp (car args)))
                (equal (apply$ 'always$ args)
                       (always$ (car args)
                                (car (cdr args)))))))

Theorem: apply$-warrant-always$-necc

(defthm apply$-warrant-always$-necc
  (implies (not (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)))))))
           (not (apply$-warrant-always$))))

Theorem: apply$-sum$+

(defthm apply$-sum$+
  (and (implies (force (apply$-warrant-sum$+))
                (equal (badge 'sum$+)
                       '(apply$-badge 3 1 :fn nil nil)))
       (implies (and (force (apply$-warrant-sum$+))
                     (tamep-functionp (car args)))
                (equal (apply$ 'sum$+ args)
                       (sum$+ (car args)
                              (car (cdr args))
                              (car (cdr (cdr args))))))))

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

(defthm apply$-warrant-sum$+-necc
  (implies
       (not (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))))))))
       (not (apply$-warrant-sum$+))))

Theorem: apply$-sum$+-ac

(defthm apply$-sum$+-ac
  (and (implies (force (apply$-warrant-sum$+-ac))
                (equal (badge 'sum$+-ac)
                       '(apply$-badge 4 1 :fn nil nil nil)))
       (implies (and (force (apply$-warrant-sum$+-ac))
                     (tamep-functionp (car args)))
                (equal (apply$ 'sum$+-ac args)
                       (sum$+-ac (car args)
                                 (car (cdr args))
                                 (car (cdr (cdr args)))
                                 (car (cdr (cdr (cdr args)))))))))

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

(defthm apply$-warrant-sum$+-ac-necc
 (implies
  (not
    (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)))))))))
  (not (apply$-warrant-sum$+-ac))))

Theorem: apply$-sum$

(defthm apply$-sum$
  (and (implies (force (apply$-warrant-sum$))
                (equal (badge 'sum$)
                       '(apply$-badge 2 1 :fn nil)))
       (implies (and (force (apply$-warrant-sum$))
                     (tamep-functionp (car args)))
                (equal (apply$ 'sum$ args)
                       (sum$ (car args) (car (cdr args)))))))

Theorem: apply$-warrant-sum$-necc

(defthm apply$-warrant-sum$-necc
 (implies
    (not (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)))))))
    (not (apply$-warrant-sum$))))

Theorem: apply$-sum$-ac

(defthm apply$-sum$-ac
  (and (implies (force (apply$-warrant-sum$-ac))
                (equal (badge 'sum$-ac)
                       '(apply$-badge 3 1 :fn nil nil)))
       (implies (and (force (apply$-warrant-sum$-ac))
                     (tamep-functionp (car args)))
                (equal (apply$ 'sum$-ac args)
                       (sum$-ac (car args)
                                (car (cdr args))
                                (car (cdr (cdr args))))))))

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

(defthm apply$-warrant-sum$-ac-necc
 (implies
      (not (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))))))))
      (not (apply$-warrant-sum$-ac))))

Theorem: apply$-when$+

(defthm apply$-when$+
  (and (implies (force (apply$-warrant-when$+))
                (equal (badge 'when$+)
                       '(apply$-badge 3 1 :fn nil nil)))
       (implies (and (force (apply$-warrant-when$+))
                     (tamep-functionp (car args)))
                (equal (apply$ 'when$+ args)
                       (when$+ (car args)
                               (car (cdr args))
                               (car (cdr (cdr args))))))))

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

(defthm apply$-warrant-when$+-necc
  (implies
       (not (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))))))))
       (not (apply$-warrant-when$+))))

Theorem: apply$-when$+-ac

(defthm apply$-when$+-ac
  (and (implies (force (apply$-warrant-when$+-ac))
                (equal (badge 'when$+-ac)
                       '(apply$-badge 4 1 :fn nil nil nil)))
       (implies (and (force (apply$-warrant-when$+-ac))
                     (tamep-functionp (car args)))
                (equal (apply$ 'when$+-ac args)
                       (when$+-ac (car args)
                                  (car (cdr args))
                                  (car (cdr (cdr args)))
                                  (car (cdr (cdr (cdr args)))))))))

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

(defthm apply$-warrant-when$+-ac-necc
 (implies
  (not
   (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)))))))))
  (not (apply$-warrant-when$+-ac))))

Theorem: apply$-when$

(defthm apply$-when$
  (and (implies (force (apply$-warrant-when$))
                (equal (badge 'when$)
                       '(apply$-badge 2 1 :fn nil)))
       (implies (and (force (apply$-warrant-when$))
                     (tamep-functionp (car args)))
                (equal (apply$ 'when$ args)
                       (when$ (car args) (car (cdr args)))))))

Theorem: apply$-warrant-when$-necc

(defthm apply$-warrant-when$-necc
 (implies
   (not (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)))))))
   (not (apply$-warrant-when$))))

Theorem: apply$-when$-ac

(defthm apply$-when$-ac
  (and (implies (force (apply$-warrant-when$-ac))
                (equal (badge 'when$-ac)
                       '(apply$-badge 3 1 :fn nil nil)))
       (implies (and (force (apply$-warrant-when$-ac))
                     (tamep-functionp (car args)))
                (equal (apply$ 'when$-ac args)
                       (when$-ac (car args)
                                 (car (cdr args))
                                 (car (cdr (cdr args))))))))

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

(defthm apply$-warrant-when$-ac-necc
 (implies
     (not (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))))))))
     (not (apply$-warrant-when$-ac))))

Theorem: apply$-until$+

(defthm apply$-until$+
  (and (implies (force (apply$-warrant-until$+))
                (equal (badge 'until$+)
                       '(apply$-badge 3 1 :fn nil nil)))
       (implies (and (force (apply$-warrant-until$+))
                     (tamep-functionp (car args)))
                (equal (apply$ 'until$+ args)
                       (until$+ (car args)
                                (car (cdr args))
                                (car (cdr (cdr args))))))))

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

(defthm apply$-warrant-until$+-necc
 (implies
      (not (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))))))))
      (not (apply$-warrant-until$+))))

Theorem: apply$-until$+-ac

(defthm apply$-until$+-ac
  (and (implies (force (apply$-warrant-until$+-ac))
                (equal (badge 'until$+-ac)
                       '(apply$-badge 4 1 :fn nil nil nil)))
       (implies (and (force (apply$-warrant-until$+-ac))
                     (tamep-functionp (car args)))
                (equal (apply$ 'until$+-ac args)
                       (until$+-ac (car args)
                                   (car (cdr args))
                                   (car (cdr (cdr args)))
                                   (car (cdr (cdr (cdr args)))))))))

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

(defthm apply$-warrant-until$+-ac-necc
 (implies
  (not
      (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)))))))))
  (not (apply$-warrant-until$+-ac))))

Theorem: apply$-until$

(defthm apply$-until$
  (and (implies (force (apply$-warrant-until$))
                (equal (badge 'until$)
                       '(apply$-badge 2 1 :fn nil)))
       (implies (and (force (apply$-warrant-until$))
                     (tamep-functionp (car args)))
                (equal (apply$ 'until$ args)
                       (until$ (car args) (car (cdr args)))))))

Theorem: apply$-warrant-until$-necc

(defthm apply$-warrant-until$-necc
 (implies
  (not (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)))))))
  (not (apply$-warrant-until$))))

Theorem: apply$-until$-ac

(defthm apply$-until$-ac
  (and (implies (force (apply$-warrant-until$-ac))
                (equal (badge 'until$-ac)
                       '(apply$-badge 3 1 :fn nil nil)))
       (implies (and (force (apply$-warrant-until$-ac))
                     (tamep-functionp (car args)))
                (equal (apply$ 'until$-ac args)
                       (until$-ac (car args)
                                  (car (cdr args))
                                  (car (cdr (cdr args))))))))

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

(defthm apply$-warrant-until$-ac-necc
 (implies
    (not (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))))))))
    (not (apply$-warrant-until$-ac))))

Theorem: apply$-equivalence-necc

(defthm apply$-equivalence-necc
  (implies (not (equal (ec-call (apply$ fn1 args))
                       (ec-call (apply$ fn2 args))))
           (not (apply$-equivalence fn1 fn2))))

Theorem: arities-okp-implies-logicp

(defthm arities-okp-implies-logicp
  (implies (and (arities-okp user-table w)
                (assoc fn user-table))
           (logicp fn w)))

Theorem: arities-okp-implies-arity

(defthm arities-okp-implies-arity
  (implies (and (arities-okp user-table w)
                (assoc fn user-table))
           (equal (arity fn w)
                  (cdr (assoc fn user-table)))))

Theorem: term-listp-implies-pseudo-term-listp

(defthm term-listp-implies-pseudo-term-listp
  (implies (term-listp x w)
           (pseudo-term-listp x))
  :rule-classes (:rewrite :forward-chaining))

Theorem: termp-implies-pseudo-termp

(defthm termp-implies-pseudo-termp
  (implies (termp x w) (pseudo-termp x))
  :rule-classes (:rewrite :forward-chaining))

Theorem: legal-variable-or-constant-namep-implies-symbolp

(defthm legal-variable-or-constant-namep-implies-symbolp
  (implies (not (symbolp x))
           (not (legal-variable-or-constant-namep x))))

Theorem: untame-apply$-takes-arity-args

(defthm untame-apply$-takes-arity-args
 (implies
  (badge-userfn fn)
  (equal (untame-apply$ fn args)
         (untame-apply$ fn
                        (take (apply$-badge-arity (badge-userfn fn))
                              args))))
 :rule-classes
 ((:rewrite
   :corollary
   (implies
    (and (syntaxp (and (quotep fn) (symbolp args)))
         (badge-userfn fn))
    (equal
         (untame-apply$ fn args)
         (untame-apply$ fn
                        (take (apply$-badge-arity (badge-userfn fn))
                              args)))))))

Theorem: to-dfp-of-rize

(defthm to-dfp-of-rize
  (implies (dfp x)
           (equal (to-dfp (rize x)) x)))

Theorem: to-df-of-df-rationalize

(defthm to-df-of-df-rationalize
  (implies (dfp x)
           (equal (to-df (df-rationalize x)) x)))

Theorem: dfp-df-pi

(defthm dfp-df-pi (dfp (df-pi)))

Theorem: dfp-df-atanh-fn

(defthm dfp-df-atanh-fn
  (dfp (df-atanh-fn x)))

Theorem: dfp-df-acosh-fn

(defthm dfp-df-acosh-fn
  (dfp (df-acosh-fn x)))

Theorem: dfp-df-asinh-fn

(defthm dfp-df-asinh-fn
  (dfp (df-asinh-fn x)))

Theorem: dfp-df-tanh-fn

(defthm dfp-df-tanh-fn
  (dfp (df-tanh-fn x)))

Theorem: dfp-df-cosh-fn

(defthm dfp-df-cosh-fn
  (dfp (df-cosh-fn x)))

Theorem: dfp-df-sinh-fn

(defthm dfp-df-sinh-fn
  (dfp (df-sinh-fn x)))

Theorem: dfp-df-atan-fn

(defthm dfp-df-atan-fn
  (dfp (df-atan-fn x)))

Theorem: dfp-df-acos-fn

(defthm dfp-df-acos-fn
  (dfp (df-acos-fn x)))

Theorem: dfp-df-asin-fn

(defthm dfp-df-asin-fn
  (dfp (df-asin-fn x)))

Theorem: dfp-df-tan-fn

(defthm dfp-df-tan-fn
  (dfp (df-tan-fn x)))

Theorem: dfp-df-cos-fn

(defthm dfp-df-cos-fn
  (dfp (df-cos-fn x)))

Theorem: dfp-df-sin-fn

(defthm dfp-df-sin-fn
  (dfp (df-sin-fn x)))

Theorem: dfp-df-abs-fn

(defthm dfp-df-abs-fn
  (dfp (df-abs-fn x)))

Theorem: dfp-unary-df-log

(defthm dfp-unary-df-log
  (dfp (unary-df-log x)))

Theorem: dfp-binary-df-log

(defthm dfp-binary-df-log
  (dfp (binary-df-log x y)))

Theorem: dfp-df-sqrt-fn

(defthm dfp-df-sqrt-fn
  (dfp (df-sqrt-fn x)))

Theorem: dfp-df-exp-fn

(defthm dfp-df-exp-fn
  (dfp (df-exp-fn x)))

Theorem: dfp-df-expt-fn

(defthm dfp-df-expt-fn
  (dfp (df-expt-fn x y)))

Theorem: dfp-minus

(defthm dfp-minus
  (implies (dfp x) (dfp (- x))))

Theorem: df-round-idempotent

(defthm df-round-idempotent
  (equal (df-round (df-round x))
         (df-round x)))

Theorem: dfp-implies-to-df-is-identity

(defthm dfp-implies-to-df-is-identity
  (implies (dfp x) (equal (to-df x) x))
  :rule-classes (:forward-chaining :rewrite))

Theorem: dfp-to-df

(defthm dfp-to-df (dfp (to-df x)))

Theorem: to-df-monotonicity

(defthm to-df-monotonicity
  (implies (and (<= x y)
                (rationalp x)
                (rationalp y))
           (<= (to-df x) (to-df y)))
  :rule-classes (:linear :rewrite))

Theorem: to-df-default

(defthm to-df-default
  (implies (not (rationalp x))
           (equal (to-df x) 0)))

Theorem: to-df-idempotent

(defthm to-df-idempotent
  (equal (to-df (to-df x)) (to-df x)))

Theorem: symbol-listp-strict-merge-sort-symbol<

(defthm symbol-listp-strict-merge-sort-symbol<
  (implies (symbol-listp x)
           (symbol-listp (strict-merge-sort-symbol< x))))

Theorem: ancestors-check-constraint

(defthm ancestors-check-constraint
  (implies (and (pseudo-termp lit)
                (ancestor-listp ancestors)
                (true-listp tokens))
           (mv-let (on-ancestors assumed-true)
                   (ancestors-check lit ancestors tokens)
             (implies (and on-ancestors assumed-true)
                      (member-equal-mod-commuting
                           lit (strip-ancestor-literals ancestors)
                           nil)))))

Theorem: ancestors-check-builtin-property

(defthm ancestors-check-builtin-property
  (mv-let (on-ancestors assumed-true)
          (ancestors-check-builtin lit ancestors tokens)
    (implies (and on-ancestors assumed-true)
             (member-equal-mod-commuting
                  lit (strip-ancestor-literals ancestors)
                  nil))))

Theorem: symbol-listp-cdr-assoc-equal

(defthm symbol-listp-cdr-assoc-equal
  (implies (symbol-list-listp x)
           (symbol-listp (cdr (assoc-equal key x)))))

Theorem: canonical-pathname-is-idempotent

(defthm canonical-pathname-is-idempotent
  (equal (canonical-pathname (canonical-pathname x dir-p state)
                             dir-p state)
         (canonical-pathname x dir-p state)))

Theorem: eqlablep-nth

(defthm eqlablep-nth
  (implies (eqlable-listp x)
           (eqlablep (nth n x))))

Theorem: resize-list-exec-is-resize-list

(defthm resize-list-exec-is-resize-list
  (implies (true-listp acc)
           (equal (resize-list-exec lst n default-value acc)
                  (revappend acc
                             (resize-list lst n default-value)))))

Theorem: lexorder-transitive

(defthm lexorder-transitive
  (implies (and (lexorder x y) (lexorder y z))
           (lexorder x z))
  :rule-classes ((:rewrite :match-free :all)))

Theorem: lexorder-reflexive

(defthm lexorder-reflexive
  (lexorder x x))

Theorem: alphorder-transitive

(defthm alphorder-transitive
  (implies (and (alphorder x y)
                (alphorder y z)
                (not (consp x))
                (not (consp y))
                (not (consp z)))
           (alphorder x z))
  :rule-classes ((:rewrite :match-free :all)))

Theorem: alphorder-reflexive

(defthm alphorder-reflexive
  (implies (not (consp x))
           (alphorder x x)))

Theorem: type-alistp-mfc-type-alist

(defthm type-alistp-mfc-type-alist
  (type-alistp (mfc-type-alist mfc)))

Theorem: pseudo-term-listp-mfc-clause

(defthm pseudo-term-listp-mfc-clause
  (pseudo-term-listp (mfc-clause mfc)))

Theorem: default-realpart

(defthm default-realpart
  (implies (not (acl2-numberp x))
           (equal (realpart x) 0)))

Theorem: default-numerator

(defthm default-numerator
  (implies (not (rationalp x))
           (equal (numerator x) 0)))

Theorem: default-intern-in-package-of-symbol

(defthm default-intern-in-package-of-symbol
  (implies (not (and (stringp x) (symbolp y)))
           (equal (intern-in-package-of-symbol x y)
                  nil)))

Theorem: default-imagpart

(defthm default-imagpart
  (implies (not (acl2-numberp x))
           (equal (imagpart x) 0)))

Theorem: default-denominator

(defthm default-denominator
  (implies (not (rationalp x))
           (equal (denominator x) 1)))

Theorem: default-coerce-3

(defthm default-coerce-3
  (implies (not (consp x))
           (equal (coerce x 'string) "")))

Theorem: default-coerce-2

(defthm default-coerce-2
  (implies (and (syntaxp (not (equal y ''string)))
                (not (equal y 'list)))
           (equal (coerce x y)
                  (coerce x 'string))))

Theorem: make-character-list-make-character-list

(defthm make-character-list-make-character-list
  (equal (make-character-list (make-character-list x))
         (make-character-list x)))

Theorem: default-coerce-1

(defthm default-coerce-1
  (implies (not (stringp x))
           (equal (coerce x 'list) nil)))

Theorem: imagpart-+

(defthm imagpart-+
  (equal (imagpart (+ x y))
         (+ (imagpart x) (imagpart y))))

Theorem: realpart-+

(defthm realpart-+
  (equal (realpart (+ x y))
         (+ (realpart x) (realpart y))))

Theorem: complex-0

(defthm complex-0
  (equal (complex x 0) (realfix x)))

Theorem: default-complex-2

(defthm default-complex-2
  (implies (not (real/rationalp y))
           (equal (complex x y)
                  (if (real/rationalp x) x 0))))

Theorem: default-complex-1

(defthm default-complex-1
  (implies (not (real/rationalp x))
           (equal (complex x y) (complex 0 y))))

Theorem: default-code-char

(defthm default-code-char
  (implies (and (syntaxp (not (equal x ''0)))
                (not (and (integerp x) (>= x 0) (< x 256))))
           (equal (code-char x) *null-char*)))

Theorem: default-char-code

(defthm default-char-code
  (implies (not (characterp x))
           (equal (char-code x) 0)))

Theorem: cons-car-cdr

(defthm cons-car-cdr
  (equal (cons (car x) (cdr x))
         (if (consp x) x (cons nil nil))))

Theorem: default-cdr

(defthm default-cdr
  (implies (not (consp x))
           (equal (cdr x) nil)))

Theorem: default-car

(defthm default-car
  (implies (not (consp x))
           (equal (car x) nil)))

Theorem: default-<-2

(defthm default-<-2
  (implies (not (acl2-numberp y))
           (equal (< x y) (< x 0))))

Theorem: default-<-1

(defthm default-<-1
  (implies (not (acl2-numberp x))
           (equal (< x y) (< 0 y))))

Theorem: default-unary-/

(defthm default-unary-/
  (implies (or (not (acl2-numberp x)) (equal x 0))
           (equal (/ x) 0)))

Theorem: default-unary-minus

(defthm default-unary-minus
  (implies (not (acl2-numberp x))
           (equal (- x) 0)))

Theorem: default-*-2

(defthm default-*-2
  (implies (not (acl2-numberp y))
           (equal (* x y) 0)))

Theorem: default-*-1

(defthm default-*-1
  (implies (not (acl2-numberp x))
           (equal (* x y) 0)))

Theorem: default-+-2

(defthm default-+-2
  (implies (not (acl2-numberp y))
           (equal (+ x y) (fix x))))

Theorem: default-+-1

(defthm default-+-1
  (implies (not (acl2-numberp x))
           (equal (+ x y) (fix y))))

Theorem: intersection-eql-exec-is-intersection-equal

(defthm intersection-eql-exec-is-intersection-equal
  (equal (intersection-eql-exec l1 l2)
         (intersection-equal l1 l2)))

Theorem: intersection-eq-exec-is-intersection-equal

(defthm intersection-eq-exec-is-intersection-equal
  (equal (intersection-eq-exec l1 l2)
         (intersection-equal l1 l2)))

Theorem: state-p1-update-nth-2-world

(defthm state-p1-update-nth-2-world
  (implies (and (state-p1 state)
                (plist-worldp wrld)
                (known-package-alistp (getpropc 'known-package-alist
                                                'global-value
                                                nil wrld))
                (symbol-alistp (getpropc 'acl2-defaults-table
                                         'table-alist
                                         nil wrld)))
           (state-p1 (update-nth 2
                                 (add-pair 'current-acl2-world
                                           wrld (nth 2 state))
                                 state))))

Theorem: rationalp-implies-acl2-numberp

(defthm rationalp-implies-acl2-numberp
  (implies (rationalp x)
           (acl2-numberp x)))

Theorem: rationalp-unary-/

(defthm rationalp-unary-/
  (implies (rationalp x)
           (rationalp (/ x))))

Theorem: rationalp-unary--

(defthm rationalp-unary--
  (implies (rationalp x)
           (rationalp (- x))))

Theorem: rationalp-*

(defthm rationalp-*
  (implies (and (rationalp x) (rationalp y))
           (rationalp (* x y))))

Theorem: rationalp-+

(defthm rationalp-+
  (implies (and (rationalp x) (rationalp y))
           (rationalp (+ x y))))

Theorem: all-boundp-initial-global-table-alt

(defthm all-boundp-initial-global-table-alt
  (implies (and (state-p1 state)
                (assoc-eq x *initial-global-table*))
           (boundp-global1 x state)))

Theorem: put-assoc-eql-exec-is-put-assoc-equal

(defthm put-assoc-eql-exec-is-put-assoc-equal
  (equal (put-assoc-eql-exec name val alist)
         (put-assoc-equal name val alist)))

Theorem: put-assoc-eq-exec-is-put-assoc-equal

(defthm put-assoc-eq-exec-is-put-assoc-equal
  (equal (put-assoc-eq-exec name val alist)
         (put-assoc-equal name val alist)))

Theorem: update-acl2-oracle-preserves-state-p1

(defthm update-acl2-oracle-preserves-state-p1
  (implies (and (state-p1 state) (true-listp x))
           (state-p1 (update-acl2-oracle x state))))

Theorem: state-p1-read-acl2-oracle

(defthm state-p1-read-acl2-oracle
  (implies (state-p1 state)
           (state-p1 (mv-nth 2 (read-acl2-oracle state)))))

Theorem: pairlis$-true-list-fix

(defthm pairlis$-true-list-fix
  (equal (pairlis$ x (true-list-fix y))
         (pairlis$ x y)))

Theorem: nth-add1

(defthm nth-add1
  (implies (and (integerp n) (>= n 0))
           (equal (nth (+ 1 n) (cons a l))
                  (nth n l))))

Theorem: nth-0-cons

(defthm nth-0-cons
  (equal (nth 0 (cons a l)) a))

Theorem: add-pair-preserves-all-boundp

(defthm add-pair-preserves-all-boundp
  (implies (all-boundp alist1 alist2)
           (all-boundp alist1 (add-pair sym val alist2))))

Theorem: assoc-add-pair

(defthm assoc-add-pair
  (equal (assoc sym1 (add-pair sym2 val alist))
         (if (equal sym1 sym2)
             (cons sym1 val)
           (assoc sym1 alist))))

Theorem: len-update-nth

(defthm len-update-nth
  (equal (len (update-nth n val x))
         (max (1+ (nfix n)) (len x))))

Theorem: nth-update-nth-array

(defthm nth-update-nth-array
  (equal (nth m (update-nth-array n i val l))
         (if (equal (nfix m) (nfix n))
             (update-nth i val (nth m l))
           (nth m l))))

Theorem: nth-update-nth

(defthm nth-update-nth
  (equal (nth m (update-nth n val l))
         (if (equal (nfix m) (nfix n))
             val
           (nth m l))))

Theorem: standard-char-p-nth

(defthm standard-char-p-nth
  (implies (and (standard-char-listp chars)
                (<= 0 i)
                (< i (len chars)))
           (standard-char-p (nth i chars))))

Theorem: character-listp-string-upcase1-1

(defthm character-listp-string-upcase1-1
  (character-listp (string-upcase1 x)))

Theorem: character-listp-string-downcase-1

(defthm character-listp-string-downcase-1
  (character-listp (string-downcase1 x)))

Theorem: upper-case-p-char-upcase

(defthm upper-case-p-char-upcase
  (implies (lower-case-p x)
           (upper-case-p (char-upcase x))))

Theorem: lower-case-p-char-downcase

(defthm lower-case-p-char-downcase
  (implies (upper-case-p x)
           (lower-case-p (char-downcase x))))

Theorem: ordered-symbol-alistp-getprops

(defthm ordered-symbol-alistp-getprops
  (implies (plist-worldp w)
           (ordered-symbol-alistp (getprops key world-name w))))

Theorem: ordered-symbol-alistp-add-pair

(defthm ordered-symbol-alistp-add-pair
  (implies (and (ordered-symbol-alistp gs)
                (symbolp w5))
           (ordered-symbol-alistp (add-pair w5 w6 gs))))

Theorem: symbol<-irreflexive

(defthm symbol<-irreflexive
  (implies (symbolp x)
           (not (symbol< x x))))

Theorem: ordered-symbol-alistp-remove1-assoc-eq

(defthm ordered-symbol-alistp-remove1-assoc-eq
  (implies (ordered-symbol-alistp l)
           (ordered-symbol-alistp (remove1-assoc-eq key l))))

Theorem: symbol<-trichotomy

(defthm symbol<-trichotomy
  (implies (and (symbolp x)
                (symbolp y)
                (not (symbol< x y)))
           (iff (symbol< y x) (not (equal x y)))))

Theorem: string<-l-trichotomy

(defthm string<-l-trichotomy
  (implies (and (not (string<-l x y i))
                (integerp i)
                (integerp j)
                (character-listp x)
                (character-listp y))
           (iff (string<-l y x j)
                (not (equal x y))))
  :rule-classes ((:rewrite :match-free :all)))

Theorem: symbol<-transitive

(defthm symbol<-transitive
  (implies (and (symbol< x y)
                (symbol< y z)
                (symbolp x)
                (symbolp y)
                (symbolp z))
           (symbol< x z))
  :rule-classes ((:rewrite :match-free :all)))

Theorem: string<-l-transitive

(defthm string<-l-transitive
  (implies (and (string<-l x y i)
                (string<-l y z j)
                (integerp i)
                (integerp j)
                (integerp k)
                (character-listp x)
                (character-listp y)
                (character-listp z))
           (string<-l x z k))
  :rule-classes ((:rewrite :match-free :all)))

Theorem: symbol<-asymmetric

(defthm symbol<-asymmetric
  (implies (symbol< sym1 sym2)
           (not (symbol< sym2 sym1))))

Theorem: string<-l-asymmetric

(defthm string<-l-asymmetric
  (implies (and (eqlable-listp x1)
                (eqlable-listp x2)
                (integerp i)
                (string<-l x1 x2 i))
           (not (string<-l x2 x1 i))))

Theorem: default-symbol-package-name

(defthm default-symbol-package-name
  (implies (not (symbolp x))
           (equal (symbol-package-name x) "")))

Theorem: default-symbol-name

(defthm default-symbol-name
  (implies (not (symbolp x))
           (equal (symbol-name x) "")))

Theorem: state-p-implies-and-forward-to-state-p1

(defthm state-p-implies-and-forward-to-state-p1
  (implies (state-p state-state)
           (state-p1 state-state))
  :rule-classes (:forward-chaining :rewrite))

Theorem: all-boundp-initial-global-table

(defthm all-boundp-initial-global-table
  (implies (and (state-p1 state)
                (assoc-eq x *initial-global-table*))
           (assoc-equal x (nth 2 state))))

Theorem: array2p-cons

(defthm array2p-cons
  (implies (and (< j (cadr (dimensions name l)))
                (not (< j 0))
                (integerp j)
                (< i (car (dimensions name l)))
                (not (< i 0))
                (integerp i)
                (array2p name l))
           (array2p name (cons (cons (cons i j) val) l))))

Theorem: array1p-cons

(defthm array1p-cons
 (implies
  (and
   (<
     n
     (caadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))
   (not (< n 0))
   (integerp n)
   (array1p name l))
  (array1p name (cons (cons n val) l))))

Theorem: remove-assoc-eql-exec-is-remove-assoc-equal

(defthm remove-assoc-eql-exec-is-remove-assoc-equal
  (equal (remove-assoc-eql-exec x l)
         (remove-assoc-equal x l)))

Theorem: remove-assoc-eq-exec-is-remove-assoc-equal

(defthm remove-assoc-eq-exec-is-remove-assoc-equal
  (equal (remove-assoc-eq-exec x l)
         (remove-assoc-equal x l)))

Theorem: remove1-assoc-eql-exec-is-remove1-assoc-equal

(defthm remove1-assoc-eql-exec-is-remove1-assoc-equal
  (equal (remove1-assoc-eql-exec key lst)
         (remove1-assoc-equal key lst)))

Theorem: remove1-assoc-eq-exec-is-remove1-assoc-equal

(defthm remove1-assoc-eq-exec-is-remove1-assoc-equal
  (equal (remove1-assoc-eq-exec key lst)
         (remove1-assoc-equal key lst)))

Theorem: string<-irreflexive

(defthm string<-irreflexive
  (not (string< s s)))

Theorem: string<-l-irreflexive

(defthm string<-l-irreflexive
  (not (string<-l x x i)))

Theorem: position-eql-exec-is-position-equal

(defthm position-eql-exec-is-position-equal
  (equal (position-eql-exec item lst)
         (position-equal item lst)))

Theorem: position-eq-exec-is-position-equal

(defthm position-eq-exec-is-position-equal
  (implies (not (stringp lst))
           (equal (position-eq-exec item lst)
                  (position-equal item lst))))

Theorem: position-ac-eql-exec-is-position-equal-ac

(defthm position-ac-eql-exec-is-position-equal-ac
  (equal (position-ac-eql-exec item lst acc)
         (position-equal-ac item lst acc)))

Theorem: position-ac-eq-exec-is-position-equal-ac

(defthm position-ac-eq-exec-is-position-equal-ac
  (equal (position-ac-eq-exec item lst acc)
         (position-equal-ac item lst acc)))

Theorem: intersectp-eql-exec-is-intersectp-equal

(defthm intersectp-eql-exec-is-intersectp-equal
  (equal (intersectp-eql-exec x y)
         (intersectp-equal x y)))

Theorem: intersectp-eq-exec-is-intersectp-equal

(defthm intersectp-eq-exec-is-intersectp-equal
  (equal (intersectp-eq-exec x y)
         (intersectp-equal x y)))

Theorem: union-eql-exec-is-union-equal

(defthm union-eql-exec-is-union-equal
  (equal (union-eql-exec l1 l2)
         (union-equal l1 l2)))

Theorem: union-eq-exec-is-union-equal

(defthm union-eq-exec-is-union-equal
  (equal (union-eq-exec l1 l2)
         (union-equal l1 l2)))

Theorem: add-to-set-eql-exec-is-add-to-set-equal

(defthm add-to-set-eql-exec-is-add-to-set-equal
  (equal (add-to-set-eql-exec x lst)
         (add-to-set-equal x lst)))

Theorem: add-to-set-eq-exec-is-add-to-set-equal

(defthm add-to-set-eq-exec-is-add-to-set-equal
  (equal (add-to-set-eq-exec x lst)
         (add-to-set-equal x lst)))

Theorem: last-cdr-is-nil

(defthm last-cdr-is-nil
  (implies (true-listp x)
           (equal (last-cdr x) nil)))

Theorem: set-difference-eql-exec-is-set-difference-equal

(defthm set-difference-eql-exec-is-set-difference-equal
  (equal (set-difference-eql-exec l1 l2)
         (set-difference-equal l1 l2)))

Theorem: set-difference-eq-exec-is-set-difference-equal

(defthm set-difference-eq-exec-is-set-difference-equal
  (equal (set-difference-eq-exec l1 l2)
         (set-difference-equal l1 l2)))

Theorem: pairlis$-tailrec-is-pairlis$

(defthm pairlis$-tailrec-is-pairlis$
  (implies (true-listp acc)
           (equal (pairlis$-tailrec x y acc)
                  (revappend acc (pairlis$ x y)))))

Theorem: character-listp-revappend

(defthm character-listp-revappend
  (implies (true-listp x)
           (equal (character-listp (revappend x y))
                  (and (character-listp x)
                       (character-listp y)))))

Theorem: character-listp-remove-duplicates

(defthm character-listp-remove-duplicates
  (implies (character-listp x)
           (character-listp (remove-duplicates x))))

Theorem: remove-duplicates-eql-exec-is-remove-duplicates-equal

(defthm remove-duplicates-eql-exec-is-remove-duplicates-equal
  (equal (remove-duplicates-eql-exec x)
         (remove-duplicates-equal x)))

Theorem: remove-duplicates-eq-exec-is-remove-duplicates-equal

(defthm remove-duplicates-eq-exec-is-remove-duplicates-equal
  (equal (remove-duplicates-eq-exec x)
         (remove-duplicates-equal x)))

Theorem: remove1-eql-exec-is-remove1-equal

(defthm remove1-eql-exec-is-remove1-equal
  (equal (remove1-eql-exec x l)
         (remove1-equal x l)))

Theorem: remove1-eq-exec-is-remove1-equal

(defthm remove1-eq-exec-is-remove1-equal
  (equal (remove1-eq-exec x l)
         (remove1-equal x l)))

Theorem: remove-eql-exec-is-remove-equal

(defthm remove-eql-exec-is-remove-equal
  (equal (remove-eql-exec x l)
         (remove-equal x l)))

Theorem: remove-eq-exec-is-remove-equal

(defthm remove-eq-exec-is-remove-equal
  (equal (remove-eq-exec x l)
         (remove-equal x l)))

Theorem: character-listp-append

(defthm character-listp-append
  (implies (true-listp x)
           (equal (character-listp (append x y))
                  (and (character-listp x)
                       (character-listp y)))))

Theorem: standard-char-listp-append

(defthm standard-char-listp-append
  (implies (true-listp x)
           (equal (standard-char-listp (append x y))
                  (and (standard-char-listp x)
                       (standard-char-listp y)))))

Theorem: default-pkg-imports

(defthm default-pkg-imports
  (implies (not (stringp x))
           (equal (pkg-imports x) nil)))

Theorem: characterp-nth

(defthm characterp-nth
  (implies (and (character-listp x)
                (<= 0 i)
                (< i (len x)))
           (characterp (nth i x))))

Theorem: o-p-implies-o<g

(defthm o-p-implies-o<g
  (implies (o-p a) (o<g a)))

Theorem: rassoc-eql-exec-is-rassoc-equal

(defthm rassoc-eql-exec-is-rassoc-equal
  (equal (rassoc-eql-exec x alist)
         (rassoc-equal x alist)))

Theorem: rassoc-eq-exec-is-rassoc-equal

(defthm rassoc-eq-exec-is-rassoc-equal
  (equal (rassoc-eq-exec x alist)
         (rassoc-equal x alist)))

Theorem: no-duplicatesp-eql-exec-is-no-duplicatesp-equal

(defthm no-duplicatesp-eql-exec-is-no-duplicatesp-equal
  (equal (no-duplicatesp-eql-exec x)
         (no-duplicatesp-equal x)))

Theorem: no-duplicatesp-eq-exec-is-no-duplicatesp-equal

(defthm no-duplicatesp-eq-exec-is-no-duplicatesp-equal
  (equal (no-duplicatesp-eq-exec x)
         (no-duplicatesp-equal x)))

Theorem: complex-equal

(defthm complex-equal
  (implies (and (real/rationalp x1)
                (real/rationalp y1)
                (real/rationalp x2)
                (real/rationalp y2))
           (equal (equal (complex x1 y1) (complex x2 y2))
                  (and (equal x1 x2) (equal y1 y2)))))

Theorem: boolean-listp-cons

(defthm boolean-listp-cons
  (equal (boolean-listp (cons x y))
         (and (booleanp x) (boolean-listp y))))

Theorem: zip-open

(defthm zip-open
  (implies (syntaxp (not (variablep x)))
           (equal (zip x)
                  (or (not (integerp x)) (equal x 0)))))

Theorem: zp-open

(defthm zp-open
  (implies (syntaxp (not (variablep x)))
           (equal (zp x)
                  (if (integerp x) (<= x 0) t))))

Theorem: assoc-eql-exec-is-assoc-equal

(defthm assoc-eql-exec-is-assoc-equal
  (equal (assoc-eql-exec x l)
         (assoc-equal x l)))

Theorem: assoc-eq-exec-is-assoc-equal

(defthm assoc-eq-exec-is-assoc-equal
  (equal (assoc-eq-exec x l)
         (assoc-equal x l)))

Theorem: subsetp-eql-exec-is-subsetp-equal

(defthm subsetp-eql-exec-is-subsetp-equal
  (equal (subsetp-eql-exec x y)
         (subsetp-equal x y)))

Theorem: subsetp-eq-exec-is-subsetp-equal

(defthm subsetp-eq-exec-is-subsetp-equal
  (equal (subsetp-eq-exec x y)
         (subsetp-equal x y)))

Theorem: member-eql-exec-is-member-equal

(defthm member-eql-exec-is-member-equal
  (equal (member-eql-exec x l)
         (member-equal x l)))

Theorem: member-eq-exec-is-member-equal

(defthm member-eq-exec-is-member-equal
  (equal (member-eq-exec x l)
         (member-equal x l)))

Theorem: append-to-nil

(defthm append-to-nil
  (implies (true-listp x)
           (equal (append x nil) x)))

Theorem: dfp-constrained-df-pi

(defthm dfp-constrained-df-pi
  (dfp (constrained-df-pi)))

Theorem: dfp-constrained-df-atanh-fn

(defthm dfp-constrained-df-atanh-fn
  (dfp (constrained-df-atanh-fn x)))

Theorem: dfp-constrained-df-acosh-fn

(defthm dfp-constrained-df-acosh-fn
  (dfp (constrained-df-acosh-fn x)))

Theorem: dfp-constrained-df-asinh-fn

(defthm dfp-constrained-df-asinh-fn
  (dfp (constrained-df-asinh-fn x)))

Theorem: dfp-constrained-df-tanh-fn

(defthm dfp-constrained-df-tanh-fn
  (dfp (constrained-df-tanh-fn x)))

Theorem: dfp-constrained-df-cosh-fn

(defthm dfp-constrained-df-cosh-fn
  (dfp (constrained-df-cosh-fn x)))

Theorem: dfp-constrained-df-sinh-fn

(defthm dfp-constrained-df-sinh-fn
  (dfp (constrained-df-sinh-fn x)))

Theorem: dfp-constrained-df-atan-fn

(defthm dfp-constrained-df-atan-fn
  (dfp (constrained-df-atan-fn x)))

Theorem: dfp-constrained-df-acos-fn

(defthm dfp-constrained-df-acos-fn
  (dfp (constrained-df-acos-fn x)))

Theorem: dfp-constrained-df-asin-fn

(defthm dfp-constrained-df-asin-fn
  (dfp (constrained-df-asin-fn x)))

Theorem: dfp-constrained-df-tan-fn

(defthm dfp-constrained-df-tan-fn
  (dfp (constrained-df-tan-fn x)))

Theorem: dfp-constrained-df-cos-fn

(defthm dfp-constrained-df-cos-fn
  (dfp (constrained-df-cos-fn x)))

Theorem: dfp-constrained-df-sin-fn

(defthm dfp-constrained-df-sin-fn
  (dfp (constrained-df-sin-fn x)))

Theorem: dfp-constrained-df-abs-fn

(defthm dfp-constrained-df-abs-fn
  (dfp (constrained-df-abs-fn x)))

Theorem: dfp-constrained-unary-df-log

(defthm dfp-constrained-unary-df-log
  (dfp (constrained-unary-df-log x)))

Theorem: dfp-constrained-binary-df-log

(defthm dfp-constrained-binary-df-log
  (dfp (constrained-binary-df-log x y)))

Theorem: dfp-constrained-df-sqrt-fn

(defthm dfp-constrained-df-sqrt-fn
  (dfp (constrained-df-sqrt-fn x)))

Theorem: dfp-constrained-df-exp-fn

(defthm dfp-constrained-df-exp-fn
  (dfp (constrained-df-exp-fn x)))

Theorem: dfp-constrained-df-expt-fn

(defthm dfp-constrained-df-expt-fn
  (dfp (constrained-df-expt-fn x y)))

Theorem: ev-fncall+-fns-is-subset-of-badged-fns-of-world

(defthm ev-fncall+-fns-is-subset-of-badged-fns-of-world
  (subsetp (ev-fncall+-fns fn args wrld big-n safe-mode gc-off nil)
           (warranted-fns-of-world wrld)))

Theorem: all-function-symbolps-ev-fncall+-fns

(defthm all-function-symbolps-ev-fncall+-fns
  (let ((fns (ev-fncall+-fns fn
                             args wrld big-n safe-mode gc-off nil)))
    (all-function-symbolps fns wrld)))

Theorem: to-df-of-constrained-df-rationalize

(defthm to-df-of-constrained-df-rationalize
  (implies (dfp x)
           (equal (to-df (constrained-df-rationalize x))
                  x)))

Theorem: df-round-monotonicity

(defthm df-round-monotonicity
  (implies (and (<= x y)
                (rationalp x)
                (rationalp y))
           (<= (df-round x) (df-round y)))
  :rule-classes (:linear :rewrite))

Theorem: df-round-is-identity-for-dfp

(defthm df-round-is-identity-for-dfp
  (implies (dfp r)
           (equal (df-round r) r)))

Theorem: dfp-df-round

(defthm dfp-df-round (dfp (df-round r)))

Theorem: constrained-to-df-monotonicity

(defthm constrained-to-df-monotonicity
  (implies (and (<= x y)
                (rationalp x)
                (rationalp y))
           (<= (constrained-to-df x)
               (constrained-to-df y)))
  :rule-classes (:linear :rewrite))

Theorem: constrained-to-df-0

(defthm constrained-to-df-0
  (equal (constrained-to-df 0) 0))

Theorem: constrained-to-df-default

(defthm constrained-to-df-default
  (implies (not (rationalp x))
           (equal (constrained-to-df x) 0)))

Theorem: to-df-minus

(defthm to-df-minus
  (implies (and (rationalp x)
                (equal (constrained-to-df x) x))
           (equal (constrained-to-df (- x))
                  (- x))))

Theorem: constrained-to-df-idempotent

(defthm constrained-to-df-idempotent
  (equal (constrained-to-df (constrained-to-df x))
         (constrained-to-df x)))

Theorem: char-upcase/downcase-non-standard-inverses

(defthm char-upcase/downcase-non-standard-inverses
 (implies
  (characterp x)
  (and
   (implies
    (upper-case-p-non-standard x)
    (equal (char-upcase-non-standard (char-downcase-non-standard x))
           x))
   (implies
    (lower-case-p-non-standard x)
    (equal (char-downcase-non-standard (char-upcase-non-standard x))
           x)))))

Theorem: upper-case-p-non-standard-char-upcase-non-standard

(defthm upper-case-p-non-standard-char-upcase-non-standard
 (implies (lower-case-p-non-standard x)
          (upper-case-p-non-standard (char-upcase-non-standard x))))

Theorem: lower-case-p-non-standard-char-downcase-non-standard

(defthm lower-case-p-non-standard-char-downcase-non-standard
  (implies
       (upper-case-p-non-standard x)
       (lower-case-p-non-standard (char-downcase-non-standard x))))

Theorem: char-downcase-maps-non-standard-to-non-standard

(defthm char-downcase-maps-non-standard-to-non-standard
  (implies (characterp x)
           (equal (standard-char-p (char-downcase-non-standard x))
                  (standard-char-p x))))

Theorem: char-upcase-maps-non-standard-to-non-standard

(defthm char-upcase-maps-non-standard-to-non-standard
  (implies (characterp x)
           (equal (standard-char-p (char-upcase-non-standard x))
                  (standard-char-p x))))

Theorem: distributivity-of-minus-over-+

(defthm distributivity-of-minus-over-+
  (equal (- (+ x y)) (+ (- x) (- y))))

Theorem: fold-consts-in-+

(defthm fold-consts-in-+
  (implies (and (syntaxp (quotep x))
                (syntaxp (quotep y)))
           (equal (+ x (+ y z)) (+ (+ x y) z))))

Theorem: commutativity-2-of-+

(defthm commutativity-2-of-+
  (equal (+ x (+ y z)) (+ y (+ x z))))