Built-in axioms and theorems
of the
Definition:
(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:
(defaxiom char-code-code-char-is-identity (implies (and (integerp n) (<= 0 n) (< n 256)) (equal (char-code (code-char n)) n)))
Definition:
(defaxiom code-char-char-code-is-identity (implies (characterp c) (equal (code-char (char-code c)) c)))
Definition:
(defaxiom keyword-package (equal (pkg-imports "KEYWORD") nil))
Definition:
(defaxiom acl2-package (equal (pkg-imports "ACL2") *common-lisp-symbols-from-main-lisp-package*))
Definition:
(defaxiom acl2-output-channel-package (equal (pkg-imports "ACL2-OUTPUT-CHANNEL") nil))
Definition:
(defaxiom acl2-input-channel-package (equal (pkg-imports "ACL2-INPUT-CHANNEL") nil))
Definition:
(defaxiom no-duplicatesp-eq-pkg-imports (no-duplicatesp-eq (pkg-imports pkg)) :rule-classes :rewrite)
Definition:
(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:
(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:
(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:
(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:
(defaxiom symbol-name-pkg-witness (equal (symbol-name (pkg-witness pkg-name)) *pkg-witness-name*))
Definition:
(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:
(defaxiom character-listp-coerce (character-listp (coerce str 'list)) :rule-classes (:rewrite (:forward-chaining :trigger-terms ((coerce str 'list)))))
Definition:
(defaxiom coerce-inverse-2 (implies (stringp x) (equal (coerce (coerce x 'list) 'string) x)))
Definition:
(defaxiom coerce-inverse-1 (implies (character-listp x) (equal (coerce (coerce x 'string) 'list) x)))
Definition:
(defaxiom imagpart-complex (implies (and (real/rationalp x) (real/rationalp y)) (equal (imagpart (complex x y)) y)))
Definition:
(defaxiom realpart-complex (implies (and (real/rationalp x) (real/rationalp y)) (equal (realpart (complex x y)) x)))
Definition:
(defaxiom realpart-imagpart-elim (implies (acl2-numberp x) (equal (complex (realpart x) (imagpart x)) x)) :rule-classes (:rewrite :elim))
Definition:
(defaxiom complex-definition (implies (and (real/rationalp x) (real/rationalp y)) (equal (complex x y) (+ x (* #C(0 1) y)))))
Definition:
(defaxiom rational-implies2 (implies (rationalp x) (equal (* (/ (denominator x)) (numerator x)) x)))
Definition:
(defaxiom distributivity (equal (* x (+ y z)) (+ (* x y) (* x z))))
Definition:
(defaxiom inverse-of-* (implies (and (acl2-numberp x) (not (equal x 0))) (equal (* x (/ x)) 1)))
Definition:
(defaxiom unicity-of-1 (equal (* 1 x) (fix x)))
Definition:
(defaxiom commutativity-of-* (equal (* x y) (* y x)))
Definition:
(defaxiom associativity-of-* (equal (* (* x y) z) (* x (* y z))))
Definition:
(defaxiom inverse-of-+ (equal (+ x (- x)) 0))
Definition:
(defaxiom unicity-of-0 (equal (+ 0 x) (fix x)))
Definition:
(defaxiom commutativity-of-+ (equal (+ x y) (+ y x)))
Definition:
(defaxiom associativity-of-+ (equal (+ (+ x y) z) (+ x (+ y z))))
Definition:
(defaxiom cons-equal (equal (equal (cons x1 y1) (cons x2 y2)) (and (equal x1 x2) (equal y1 y2))))
Definition:
(defaxiom cdr-cons (equal (cdr (cons x y)) y))
Definition:
(defaxiom car-cons (equal (car (cons x y)) x))
Theorem:
(defthm apply$-do$ (and (implies (force (apply$-warrant-do$)) (equal (badge 'do$) '(apply$-badge 7 1 :fn nil :fn :fn nil 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)))))) (car (cdr (cdr (cdr (cdr (cdr (cdr args))))))))))))
Theorem:
(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 7 1 :fn nil :fn :fn nil 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)))))) (car (cdr (cdr (cdr (cdr (cdr (cdr args)))))))))))) (not (apply$-warrant-do$))))
Theorem:
(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:
(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:
(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:
(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:
(defthm apply$-eviscerate-do$-alist (implies (force (apply$-warrant-eviscerate-do$-alist)) (and (equal (badge 'eviscerate-do$-alist) '(apply$-badge 1 1 . t)) (equal (apply$ 'eviscerate-do$-alist args) (eviscerate-do$-alist (car args))))))
Theorem:
(defthm apply$-warrant-eviscerate-do$-alist-necc (implies (not (and (equal (badge-userfn 'eviscerate-do$-alist) '(apply$-badge 1 1 . t)) (equal (apply$-userfn 'eviscerate-do$-alist args) (eviscerate-do$-alist (car args))))) (not (apply$-warrant-eviscerate-do$-alist))))
Theorem:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(defthm apply$-equivalence-necc (implies (not (equal (ec-call (apply$ fn1 args)) (ec-call (apply$ fn2 args)))) (not (apply$-equivalence fn1 fn2))))
Theorem:
(defthm arities-okp-implies-logicp (implies (and (arities-okp user-table w) (assoc fn user-table)) (logicp fn w)))
Theorem:
(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:
(defthm term-listp-implies-pseudo-term-listp (implies (term-listp x w) (pseudo-term-listp x)) :rule-classes (:rewrite :forward-chaining))
Theorem:
(defthm termp-implies-pseudo-termp (implies (termp x w) (pseudo-termp x)) :rule-classes (:rewrite :forward-chaining))
Theorem:
(defthm legal-variable-or-constant-namep-implies-symbolp (implies (not (symbolp x)) (not (legal-variable-or-constant-namep x))))
Theorem:
(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:
(defthm to-dfp-of-rize (implies (dfp x) (equal (to-dfp (rize x)) x)))
Theorem:
(defthm to-df-of-df-rationalize (implies (dfp x) (equal (to-df (df-rationalize x)) x)))
Theorem:
(defthm dfp-df-pi (dfp (df-pi)))
Theorem:
(defthm dfp-df-atanh-fn (dfp (df-atanh-fn x)))
Theorem:
(defthm dfp-df-acosh-fn (dfp (df-acosh-fn x)))
Theorem:
(defthm dfp-df-asinh-fn (dfp (df-asinh-fn x)))
Theorem:
(defthm dfp-df-tanh-fn (dfp (df-tanh-fn x)))
Theorem:
(defthm dfp-df-cosh-fn (dfp (df-cosh-fn x)))
Theorem:
(defthm dfp-df-sinh-fn (dfp (df-sinh-fn x)))
Theorem:
(defthm dfp-df-atan-fn (dfp (df-atan-fn x)))
Theorem:
(defthm dfp-df-acos-fn (dfp (df-acos-fn x)))
Theorem:
(defthm dfp-df-asin-fn (dfp (df-asin-fn x)))
Theorem:
(defthm dfp-df-tan-fn (dfp (df-tan-fn x)))
Theorem:
(defthm dfp-df-cos-fn (dfp (df-cos-fn x)))
Theorem:
(defthm dfp-df-sin-fn (dfp (df-sin-fn x)))
Theorem:
(defthm dfp-df-abs-fn (dfp (df-abs-fn x)))
Theorem:
(defthm dfp-unary-df-log (dfp (unary-df-log x)))
Theorem:
(defthm dfp-binary-df-log (dfp (binary-df-log x y)))
Theorem:
(defthm dfp-df-sqrt-fn (dfp (df-sqrt-fn x)))
Theorem:
(defthm dfp-df-exp-fn (dfp (df-exp-fn x)))
Theorem:
(defthm dfp-df-expt-fn (dfp (df-expt-fn x y)))
Theorem:
(defthm dfp-minus (implies (dfp x) (dfp (- x))))
Theorem:
(defthm df-round-idempotent (equal (df-round (df-round x)) (df-round x)))
Theorem:
(defthm dfp-implies-to-df-is-identity (implies (dfp x) (equal (to-df x) x)) :rule-classes (:forward-chaining :rewrite))
Theorem:
(defthm dfp-to-df (dfp (to-df x)))
Theorem:
(defthm to-df-monotonicity (implies (and (<= x y) (rationalp x) (rationalp y)) (<= (to-df x) (to-df y))) :rule-classes (:linear :rewrite))
Theorem:
(defthm to-df-default (implies (not (rationalp x)) (equal (to-df x) 0)))
Theorem:
(defthm to-df-idempotent (equal (to-df (to-df x)) (to-df x)))
Theorem:
(defthm symbol-listp-strict-merge-sort-symbol< (implies (symbol-listp x) (symbol-listp (strict-merge-sort-symbol< x))))
Theorem:
(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:
(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:
(defthm symbol-listp-cdr-assoc-equal (implies (symbol-list-listp x) (symbol-listp (cdr (assoc-equal key x)))))
Theorem:
(defthm canonical-pathname-is-idempotent (equal (canonical-pathname (canonical-pathname x dir-p state) dir-p state) (canonical-pathname x dir-p state)))
Theorem:
(defthm eqlablep-nth (implies (eqlable-listp x) (eqlablep (nth n x))))
Theorem:
(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:
(defthm lexorder-transitive (implies (and (lexorder x y) (lexorder y z)) (lexorder x z)) :rule-classes ((:rewrite :match-free :all)))
Theorem:
(defthm lexorder-reflexive (lexorder x x))
Theorem:
(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:
(defthm alphorder-reflexive (implies (not (consp x)) (alphorder x x)))
Theorem:
(defthm type-alistp-mfc-type-alist (type-alistp (mfc-type-alist mfc)))
Theorem:
(defthm pseudo-term-listp-mfc-clause (pseudo-term-listp (mfc-clause mfc)))
Theorem:
(defthm default-realpart (implies (not (acl2-numberp x)) (equal (realpart x) 0)))
Theorem:
(defthm default-numerator (implies (not (rationalp x)) (equal (numerator x) 0)))
Theorem:
(defthm default-intern-in-package-of-symbol (implies (not (and (stringp x) (symbolp y))) (equal (intern-in-package-of-symbol x y) nil)))
Theorem:
(defthm default-imagpart (implies (not (acl2-numberp x)) (equal (imagpart x) 0)))
Theorem:
(defthm default-denominator (implies (not (rationalp x)) (equal (denominator x) 1)))
Theorem:
(defthm default-coerce-3 (implies (not (consp x)) (equal (coerce x 'string) "")))
Theorem:
(defthm default-coerce-2 (implies (and (syntaxp (not (equal y ''string))) (not (equal y 'list))) (equal (coerce x y) (coerce x 'string))))
Theorem:
(defthm make-character-list-make-character-list (equal (make-character-list (make-character-list x)) (make-character-list x)))
Theorem:
(defthm default-coerce-1 (implies (not (stringp x)) (equal (coerce x 'list) nil)))
Theorem:
(defthm imagpart-+ (equal (imagpart (+ x y)) (+ (imagpart x) (imagpart y))))
Theorem:
(defthm realpart-+ (equal (realpart (+ x y)) (+ (realpart x) (realpart y))))
Theorem:
(defthm complex-0 (equal (complex x 0) (realfix x)))
Theorem:
(defthm default-complex-2 (implies (not (real/rationalp y)) (equal (complex x y) (if (real/rationalp x) x 0))))
Theorem:
(defthm default-complex-1 (implies (not (real/rationalp x)) (equal (complex x y) (complex 0 y))))
Theorem:
(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:
(defthm default-char-code (implies (not (characterp x)) (equal (char-code x) 0)))
Theorem:
(defthm cons-car-cdr (equal (cons (car x) (cdr x)) (if (consp x) x (cons nil nil))))
Theorem:
(defthm default-cdr (implies (not (consp x)) (equal (cdr x) nil)))
Theorem:
(defthm default-car (implies (not (consp x)) (equal (car x) nil)))
Theorem:
(defthm default-<-2 (implies (not (acl2-numberp y)) (equal (< x y) (< x 0))))
Theorem:
(defthm default-<-1 (implies (not (acl2-numberp x)) (equal (< x y) (< 0 y))))
Theorem:
(defthm default-unary-/ (implies (or (not (acl2-numberp x)) (equal x 0)) (equal (/ x) 0)))
Theorem:
(defthm default-unary-minus (implies (not (acl2-numberp x)) (equal (- x) 0)))
Theorem:
(defthm default-*-2 (implies (not (acl2-numberp y)) (equal (* x y) 0)))
Theorem:
(defthm default-*-1 (implies (not (acl2-numberp x)) (equal (* x y) 0)))
Theorem:
(defthm default-+-2 (implies (not (acl2-numberp y)) (equal (+ x y) (fix x))))
Theorem:
(defthm default-+-1 (implies (not (acl2-numberp x)) (equal (+ x y) (fix y))))
Theorem:
(defthm intersection-eql-exec-is-intersection-equal (equal (intersection-eql-exec l1 l2) (intersection-equal l1 l2)))
Theorem:
(defthm intersection-eq-exec-is-intersection-equal (equal (intersection-eq-exec l1 l2) (intersection-equal l1 l2)))
Theorem:
(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:
(defthm rationalp-implies-acl2-numberp (implies (rationalp x) (acl2-numberp x)))
Theorem:
(defthm rationalp-unary-/ (implies (rationalp x) (rationalp (/ x))))
Theorem:
(defthm rationalp-unary-- (implies (rationalp x) (rationalp (- x))))
Theorem:
(defthm rationalp-* (implies (and (rationalp x) (rationalp y)) (rationalp (* x y))))
Theorem:
(defthm rationalp-+ (implies (and (rationalp x) (rationalp y)) (rationalp (+ x y))))
Theorem:
(defthm all-boundp-initial-global-table-alt (implies (and (state-p1 state) (assoc-eq x *initial-global-table*)) (boundp-global1 x state)))
Theorem:
(defthm put-assoc-eql-exec-is-put-assoc-equal (equal (put-assoc-eql-exec name val alist) (put-assoc-equal name val alist)))
Theorem:
(defthm put-assoc-eq-exec-is-put-assoc-equal (equal (put-assoc-eq-exec name val alist) (put-assoc-equal name val alist)))
Theorem:
(defthm update-acl2-oracle-preserves-state-p1 (implies (and (state-p1 state) (true-listp x)) (state-p1 (update-acl2-oracle x state))))
Theorem:
(defthm state-p1-read-acl2-oracle (implies (state-p1 state) (state-p1 (mv-nth 2 (read-acl2-oracle state)))))
Theorem:
(defthm pairlis$-true-list-fix (equal (pairlis$ x (true-list-fix y)) (pairlis$ x y)))
Theorem:
(defthm nth-add1 (implies (and (integerp n) (>= n 0)) (equal (nth (+ 1 n) (cons a l)) (nth n l))))
Theorem:
(defthm nth-0-cons (equal (nth 0 (cons a l)) a))
Theorem:
(defthm add-pair-preserves-all-boundp (implies (all-boundp alist1 alist2) (all-boundp alist1 (add-pair sym val alist2))))
Theorem:
(defthm assoc-add-pair (equal (assoc sym1 (add-pair sym2 val alist)) (if (equal sym1 sym2) (cons sym1 val) (assoc sym1 alist))))
Theorem:
(defthm len-update-nth (equal (len (update-nth n val x)) (max (1+ (nfix n)) (len x))))
Theorem:
(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:
(defthm nth-update-nth (equal (nth m (update-nth n val l)) (if (equal (nfix m) (nfix n)) val (nth m l))))
Theorem:
(defthm standard-char-p-nth (implies (and (standard-char-listp chars) (<= 0 i) (< i (len chars))) (standard-char-p (nth i chars))))
Theorem:
(defthm character-listp-string-upcase1-1 (character-listp (string-upcase1 x)))
Theorem:
(defthm character-listp-string-downcase-1 (character-listp (string-downcase1 x)))
Theorem:
(defthm upper-case-p-char-upcase (implies (lower-case-p x) (upper-case-p (char-upcase x))))
Theorem:
(defthm lower-case-p-char-downcase (implies (upper-case-p x) (lower-case-p (char-downcase x))))
Theorem:
(defthm ordered-symbol-alistp-getprops (implies (plist-worldp w) (ordered-symbol-alistp (getprops key world-name w))))
Theorem:
(defthm ordered-symbol-alistp-add-pair (implies (and (ordered-symbol-alistp gs) (symbolp w5)) (ordered-symbol-alistp (add-pair w5 w6 gs))))
Theorem:
(defthm symbol<-irreflexive (implies (symbolp x) (not (symbol< x x))))
Theorem:
(defthm ordered-symbol-alistp-remove1-assoc-eq (implies (ordered-symbol-alistp l) (ordered-symbol-alistp (remove1-assoc-eq key l))))
Theorem:
(defthm symbol<-trichotomy (implies (and (symbolp x) (symbolp y) (not (symbol< x y))) (iff (symbol< y x) (not (equal x y)))))
Theorem:
(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:
(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:
(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:
(defthm symbol<-asymmetric (implies (symbol< sym1 sym2) (not (symbol< sym2 sym1))))
Theorem:
(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:
(defthm default-symbol-package-name (implies (not (symbolp x)) (equal (symbol-package-name x) "")))
Theorem:
(defthm default-symbol-name (implies (not (symbolp x)) (equal (symbol-name x) "")))
Theorem:
(defthm state-p-implies-and-forward-to-state-p1 (implies (state-p state-state) (state-p1 state-state)) :rule-classes (:forward-chaining :rewrite))
Theorem:
(defthm all-boundp-initial-global-table (implies (and (state-p1 state) (assoc-eq x *initial-global-table*)) (assoc-equal x (nth 2 state))))
Theorem:
(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:
(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:
(defthm remove-assoc-eql-exec-is-remove-assoc-equal (equal (remove-assoc-eql-exec x l) (remove-assoc-equal x l)))
Theorem:
(defthm remove-assoc-eq-exec-is-remove-assoc-equal (equal (remove-assoc-eq-exec x l) (remove-assoc-equal x l)))
Theorem:
(defthm remove1-assoc-eql-exec-is-remove1-assoc-equal (equal (remove1-assoc-eql-exec key lst) (remove1-assoc-equal key lst)))
Theorem:
(defthm remove1-assoc-eq-exec-is-remove1-assoc-equal (equal (remove1-assoc-eq-exec key lst) (remove1-assoc-equal key lst)))
Theorem:
(defthm string<-irreflexive (not (string< s s)))
Theorem:
(defthm string<-l-irreflexive (not (string<-l x x i)))
Theorem:
(defthm position-eql-exec-is-position-equal (equal (position-eql-exec item lst) (position-equal item lst)))
Theorem:
(defthm position-eq-exec-is-position-equal (implies (not (stringp lst)) (equal (position-eq-exec item lst) (position-equal item lst))))
Theorem:
(defthm position-ac-eql-exec-is-position-equal-ac (equal (position-ac-eql-exec item lst acc) (position-equal-ac item lst acc)))
Theorem:
(defthm position-ac-eq-exec-is-position-equal-ac (equal (position-ac-eq-exec item lst acc) (position-equal-ac item lst acc)))
Theorem:
(defthm intersectp-eql-exec-is-intersectp-equal (equal (intersectp-eql-exec x y) (intersectp-equal x y)))
Theorem:
(defthm intersectp-eq-exec-is-intersectp-equal (equal (intersectp-eq-exec x y) (intersectp-equal x y)))
Theorem:
(defthm union-eql-exec-is-union-equal (equal (union-eql-exec l1 l2) (union-equal l1 l2)))
Theorem:
(defthm union-eq-exec-is-union-equal (equal (union-eq-exec l1 l2) (union-equal l1 l2)))
Theorem:
(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:
(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:
(defthm last-cdr-is-nil (implies (true-listp x) (equal (last-cdr x) nil)))
Theorem:
(defthm set-difference-eql-exec-is-set-difference-equal (equal (set-difference-eql-exec l1 l2) (set-difference-equal l1 l2)))
Theorem:
(defthm set-difference-eq-exec-is-set-difference-equal (equal (set-difference-eq-exec l1 l2) (set-difference-equal l1 l2)))
Theorem:
(defthm pairlis$-tailrec-is-pairlis$ (implies (true-listp acc) (equal (pairlis$-tailrec x y acc) (revappend acc (pairlis$ x y)))))
Theorem:
(defthm character-listp-revappend (implies (true-listp x) (equal (character-listp (revappend x y)) (and (character-listp x) (character-listp y)))))
Theorem:
(defthm character-listp-remove-duplicates (implies (character-listp x) (character-listp (remove-duplicates x))))
Theorem:
(defthm remove-duplicates-eql-exec-is-remove-duplicates-equal (equal (remove-duplicates-eql-exec x) (remove-duplicates-equal x)))
Theorem:
(defthm remove-duplicates-eq-exec-is-remove-duplicates-equal (equal (remove-duplicates-eq-exec x) (remove-duplicates-equal x)))
Theorem:
(defthm remove1-eql-exec-is-remove1-equal (equal (remove1-eql-exec x l) (remove1-equal x l)))
Theorem:
(defthm remove1-eq-exec-is-remove1-equal (equal (remove1-eq-exec x l) (remove1-equal x l)))
Theorem:
(defthm remove-eql-exec-is-remove-equal (equal (remove-eql-exec x l) (remove-equal x l)))
Theorem:
(defthm remove-eq-exec-is-remove-equal (equal (remove-eq-exec x l) (remove-equal x l)))
Theorem:
(defthm character-listp-append (implies (true-listp x) (equal (character-listp (append x y)) (and (character-listp x) (character-listp y)))))
Theorem:
(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:
(defthm default-pkg-imports (implies (not (stringp x)) (equal (pkg-imports x) nil)))
Theorem:
(defthm characterp-nth (implies (and (character-listp x) (<= 0 i) (< i (len x))) (characterp (nth i x))))
Theorem:
(defthm o-p-implies-o<g (implies (o-p a) (o<g a)))
Theorem:
(defthm rassoc-eql-exec-is-rassoc-equal (equal (rassoc-eql-exec x alist) (rassoc-equal x alist)))
Theorem:
(defthm rassoc-eq-exec-is-rassoc-equal (equal (rassoc-eq-exec x alist) (rassoc-equal x alist)))
Theorem:
(defthm no-duplicatesp-eql-exec-is-no-duplicatesp-equal (equal (no-duplicatesp-eql-exec x) (no-duplicatesp-equal x)))
Theorem:
(defthm no-duplicatesp-eq-exec-is-no-duplicatesp-equal (equal (no-duplicatesp-eq-exec x) (no-duplicatesp-equal x)))
Theorem:
(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:
(defthm boolean-listp-cons (equal (boolean-listp (cons x y)) (and (booleanp x) (boolean-listp y))))
Theorem:
(defthm zip-open (implies (syntaxp (not (variablep x))) (equal (zip x) (or (not (integerp x)) (equal x 0)))))
Theorem:
(defthm zp-open (implies (syntaxp (not (variablep x))) (equal (zp x) (if (integerp x) (<= x 0) t))))
Theorem:
(defthm assoc-eql-exec-is-assoc-equal (equal (assoc-eql-exec x l) (assoc-equal x l)))
Theorem:
(defthm assoc-eq-exec-is-assoc-equal (equal (assoc-eq-exec x l) (assoc-equal x l)))
Theorem:
(defthm subsetp-eql-exec-is-subsetp-equal (equal (subsetp-eql-exec x y) (subsetp-equal x y)))
Theorem:
(defthm subsetp-eq-exec-is-subsetp-equal (equal (subsetp-eq-exec x y) (subsetp-equal x y)))
Theorem:
(defthm member-eql-exec-is-member-equal (equal (member-eql-exec x l) (member-equal x l)))
Theorem:
(defthm member-eq-exec-is-member-equal (equal (member-eq-exec x l) (member-equal x l)))
Theorem:
(defthm append-to-nil (implies (true-listp x) (equal (append x nil) x)))
Theorem:
(defthm dfp-constrained-df-pi (dfp (constrained-df-pi)))
Theorem:
(defthm dfp-constrained-df-atanh-fn (dfp (constrained-df-atanh-fn x)))
Theorem:
(defthm dfp-constrained-df-acosh-fn (dfp (constrained-df-acosh-fn x)))
Theorem:
(defthm dfp-constrained-df-asinh-fn (dfp (constrained-df-asinh-fn x)))
Theorem:
(defthm dfp-constrained-df-tanh-fn (dfp (constrained-df-tanh-fn x)))
Theorem:
(defthm dfp-constrained-df-cosh-fn (dfp (constrained-df-cosh-fn x)))
Theorem:
(defthm dfp-constrained-df-sinh-fn (dfp (constrained-df-sinh-fn x)))
Theorem:
(defthm dfp-constrained-df-atan-fn (dfp (constrained-df-atan-fn x)))
Theorem:
(defthm dfp-constrained-df-acos-fn (dfp (constrained-df-acos-fn x)))
Theorem:
(defthm dfp-constrained-df-asin-fn (dfp (constrained-df-asin-fn x)))
Theorem:
(defthm dfp-constrained-df-tan-fn (dfp (constrained-df-tan-fn x)))
Theorem:
(defthm dfp-constrained-df-cos-fn (dfp (constrained-df-cos-fn x)))
Theorem:
(defthm dfp-constrained-df-sin-fn (dfp (constrained-df-sin-fn x)))
Theorem:
(defthm dfp-constrained-df-abs-fn (dfp (constrained-df-abs-fn x)))
Theorem:
(defthm dfp-constrained-unary-df-log (dfp (constrained-unary-df-log x)))
Theorem:
(defthm dfp-constrained-binary-df-log (dfp (constrained-binary-df-log x y)))
Theorem:
(defthm dfp-constrained-df-sqrt-fn (dfp (constrained-df-sqrt-fn x)))
Theorem:
(defthm dfp-constrained-df-exp-fn (dfp (constrained-df-exp-fn x)))
Theorem:
(defthm dfp-constrained-df-expt-fn (dfp (constrained-df-expt-fn x y)))
Theorem:
(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:
(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:
(defthm to-df-of-constrained-df-rationalize (implies (dfp x) (equal (to-df (constrained-df-rationalize x)) x)))
Theorem:
(defthm df-round-monotonicity (implies (and (<= x y) (rationalp x) (rationalp y)) (<= (df-round x) (df-round y))) :rule-classes (:linear :rewrite))
Theorem:
(defthm df-round-is-identity-for-dfp (implies (dfp r) (equal (df-round r) r)))
Theorem:
(defthm dfp-df-round (dfp (df-round r)))
Theorem:
(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:
(defthm constrained-to-df-0 (equal (constrained-to-df 0) 0))
Theorem:
(defthm constrained-to-df-default (implies (not (rationalp x)) (equal (constrained-to-df x) 0)))
Theorem:
(defthm to-df-minus (implies (and (rationalp x) (equal (constrained-to-df x) x)) (equal (constrained-to-df (- x)) (- x))))
Theorem:
(defthm constrained-to-df-idempotent (equal (constrained-to-df (constrained-to-df x)) (constrained-to-df x)))
Theorem:
(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:
(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:
(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:
(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:
(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:
(defthm distributivity-of-minus-over-+ (equal (- (+ x y)) (+ (- x) (- y))))
Theorem:
(defthm fold-consts-in-+ (implies (and (syntaxp (quotep x)) (syntaxp (quotep y))) (equal (+ x (+ y z)) (+ (+ x y) z))))
Theorem:
(defthm commutativity-2-of-+ (equal (+ x (+ y z)) (+ y (+ x z))))