|
|
|---|
|
|
|
|---|
All built-in theorems.
Theorem:
(defthm fn-equal-implies-equal-do$-4 (implies (fn-equal finally-fn finally-fn-equiv) (equal (do$ measure-fn alist do-fn finally-fn values dolia) (do$ measure-fn alist do-fn finally-fn-equiv values dolia))) :rule-classes (:congruence))
Theorem:
(defthm fn-equal-implies-equal-do$-3 (implies (fn-equal do-fn do-fn-equiv) (equal (do$ measure-fn alist do-fn finally-fn values dolia) (do$ measure-fn alist do-fn-equiv finally-fn values dolia))) :rule-classes (:congruence))
Theorem:
(defthm fn-equal-implies-equal-do$-1 (implies (fn-equal measure-fn measure-fn-equiv) (equal (do$ measure-fn alist do-fn finally-fn values dolia) (do$ measure-fn-equiv alist do-fn finally-fn values dolia))) :rule-classes (:congruence))
Theorem:
(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:
(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:
(defthm apply$-warrant-do$-definition (equal (apply$-warrant-do$) (let ((args (apply$-warrant-do$-witness))) (implies (and (tamep-functionp (car args)) (tamep-functionp (car (cdr (cdr args)))) (tamep-functionp (car (cdr (cdr (cdr args)))))) (and (equal (badge-userfn 'do$) '(apply$-badge 6 1 :fn nil :fn :fn nil nil)) (equal (apply$-userfn 'do$ args) (do$ (car args) (car (cdr args)) (car (cdr (cdr args))) (car (cdr (cdr (cdr args)))) (car (cdr (cdr (cdr (cdr args))))) (car (cdr (cdr (cdr (cdr (cdr args)))))))))))) :rule-classes :definition)
Theorem:
(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$-warrant-loop$-default-values-definition (equal (apply$-warrant-loop$-default-values) (let ((args (apply$-warrant-loop$-default-values-witness))) (and (equal (badge-userfn 'loop$-default-values) '(apply$-badge 2 1 . t)) (equal (apply$-userfn 'loop$-default-values args) (loop$-default-values (car args) (car (cdr args))))))) :rule-classes :definition)
Theorem:
(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$-warrant-loop$-default-values1-definition (equal (apply$-warrant-loop$-default-values1) (let ((args (apply$-warrant-loop$-default-values1-witness))) (and (equal (badge-userfn 'loop$-default-values1) '(apply$-badge 2 1 . t)) (equal (apply$-userfn 'loop$-default-values1 args) (loop$-default-values1 (car args) (car (cdr args))))))) :rule-classes :definition)
Theorem:
(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:
(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:
(defthm apply$-warrant-eviscerate-do$-alist-definition (equal (apply$-warrant-eviscerate-do$-alist) (let ((args (apply$-warrant-eviscerate-do$-alist-witness))) (and (equal (badge-userfn 'eviscerate-do$-alist) '(apply$-badge 2 1 . t)) (equal (apply$-userfn 'eviscerate-do$-alist args) (eviscerate-do$-alist (car args) (car (cdr args))))))) :rule-classes :definition)
Theorem:
(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$-warrant-stobj-print-name-definition (equal (apply$-warrant-stobj-print-name) (let ((args (apply$-warrant-stobj-print-name-witness))) (and (equal (badge-userfn 'stobj-print-name) '(apply$-badge 1 1 . t)) (equal (apply$-userfn 'stobj-print-name args) (stobj-print-name (car args)))))) :rule-classes :definition)
Theorem:
(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$-warrant-lexp-definition (equal (apply$-warrant-lexp) (let ((args (apply$-warrant-lexp-witness))) (and (equal (badge-userfn 'lexp) '(apply$-badge 1 1 . t)) (equal (apply$-userfn 'lexp args) (lexp (car args)))))) :rule-classes :definition)
Theorem:
(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$-warrant-lex-fix-definition (equal (apply$-warrant-lex-fix) (let ((args (apply$-warrant-lex-fix-witness))) (and (equal (badge-userfn 'lex-fix) '(apply$-badge 1 1 . t)) (equal (apply$-userfn 'lex-fix args) (lex-fix (car args)))))) :rule-classes :definition)
Theorem:
(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$-warrant-nfix-list-definition (equal (apply$-warrant-nfix-list) (let ((args (apply$-warrant-nfix-list-witness))) (and (equal (badge-userfn 'nfix-list) '(apply$-badge 1 1 . t)) (equal (apply$-userfn 'nfix-list args) (nfix-list (car args)))))) :rule-classes :definition)
Theorem:
(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$-warrant-l<-definition (equal (apply$-warrant-l<) (let ((args (apply$-warrant-l<-witness))) (and (equal (badge-userfn 'l<) '(apply$-badge 2 1 . t)) (equal (apply$-userfn 'l< args) (l< (car args) (car (cdr args))))))) :rule-classes :definition)
Theorem:
(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$-warrant-d<-definition (equal (apply$-warrant-d<) (let ((args (apply$-warrant-d<-witness))) (and (equal (badge-userfn 'd<) '(apply$-badge 2 1 . t)) (equal (apply$-userfn 'd< args) (d< (car args) (car (cdr args))))))) :rule-classes :definition)
Theorem:
(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$-warrant-mempos-definition (equal (apply$-warrant-mempos) (let ((args (apply$-warrant-mempos-witness))) (and (equal (badge-userfn 'mempos) '(apply$-badge 2 1 . t)) (equal (apply$-userfn 'mempos args) (mempos (car args) (car (cdr args))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-append$+-1 (implies (fn-equal fn fn-equiv) (equal (append$+ fn globals lst) (append$+ fn-equiv globals lst))) :rule-classes (:congruence))
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$-warrant-append$+-definition (equal (apply$-warrant-append$+) (let ((args (apply$-warrant-append$+-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'append$+) '(apply$-badge 3 1 :fn nil nil)) (equal (apply$-userfn 'append$+ args) (append$+ (car args) (car (cdr args)) (car (cdr (cdr args))))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-append$+-ac-1 (implies (fn-equal fn fn-equiv) (equal (append$+-ac fn globals lst ac) (append$+-ac fn-equiv globals lst ac))) :rule-classes (:congruence))
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$-warrant-append$+-ac-definition (equal (apply$-warrant-append$+-ac) (let ((args (apply$-warrant-append$+-ac-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'append$+-ac) '(apply$-badge 4 1 :fn nil nil nil)) (equal (apply$-userfn 'append$+-ac args) (append$+-ac (car args) (car (cdr args)) (car (cdr (cdr args))) (car (cdr (cdr (cdr args)))))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-append$-1 (implies (fn-equal fn fn-equiv) (equal (append$ fn lst) (append$ fn-equiv lst))) :rule-classes (:congruence))
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$-warrant-append$-definition (equal (apply$-warrant-append$) (let ((args (apply$-warrant-append$-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'append$) '(apply$-badge 2 1 :fn nil)) (equal (apply$-userfn 'append$ args) (append$ (car args) (car (cdr args)))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-append$-ac-1 (implies (fn-equal fn fn-equiv) (equal (append$-ac fn lst ac) (append$-ac fn-equiv lst ac))) :rule-classes (:congruence))
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$-warrant-append$-ac-definition (equal (apply$-warrant-append$-ac) (let ((args (apply$-warrant-append$-ac-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'append$-ac) '(apply$-badge 3 1 :fn nil nil)) (equal (apply$-userfn 'append$-ac args) (append$-ac (car args) (car (cdr args)) (car (cdr (cdr args))))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-collect$+-1 (implies (fn-equal fn fn-equiv) (equal (collect$+ fn globals lst) (collect$+ fn-equiv globals lst))) :rule-classes (:congruence))
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$-warrant-collect$+-definition (equal (apply$-warrant-collect$+) (let ((args (apply$-warrant-collect$+-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'collect$+) '(apply$-badge 3 1 :fn nil nil)) (equal (apply$-userfn 'collect$+ args) (collect$+ (car args) (car (cdr args)) (car (cdr (cdr args))))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-collect$+-ac-1 (implies (fn-equal fn fn-equiv) (equal (collect$+-ac fn globals lst ac) (collect$+-ac fn-equiv globals lst ac))) :rule-classes (:congruence))
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$-warrant-collect$+-ac-definition (equal (apply$-warrant-collect$+-ac) (let ((args (apply$-warrant-collect$+-ac-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'collect$+-ac) '(apply$-badge 4 1 :fn nil nil nil)) (equal (apply$-userfn 'collect$+-ac args) (collect$+-ac (car args) (car (cdr args)) (car (cdr (cdr args))) (car (cdr (cdr (cdr args)))))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-collect$-1 (implies (fn-equal fn fn-equiv) (equal (collect$ fn lst) (collect$ fn-equiv lst))) :rule-classes (:congruence))
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$-warrant-collect$-definition (equal (apply$-warrant-collect$) (let ((args (apply$-warrant-collect$-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'collect$) '(apply$-badge 2 1 :fn nil)) (equal (apply$-userfn 'collect$ args) (collect$ (car args) (car (cdr args)))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-collect$-ac-1 (implies (fn-equal fn fn-equiv) (equal (collect$-ac fn lst ac) (collect$-ac fn-equiv lst ac))) :rule-classes (:congruence))
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$-warrant-collect$-ac-definition (equal (apply$-warrant-collect$-ac) (let ((args (apply$-warrant-collect$-ac-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'collect$-ac) '(apply$-badge 3 1 :fn nil nil)) (equal (apply$-userfn 'collect$-ac args) (collect$-ac (car args) (car (cdr args)) (car (cdr (cdr args))))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-thereis$+-1 (implies (fn-equal fn fn-equiv) (equal (thereis$+ fn globals lst) (thereis$+ fn-equiv globals lst))) :rule-classes (:congruence))
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$-warrant-thereis$+-definition (equal (apply$-warrant-thereis$+) (let ((args (apply$-warrant-thereis$+-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'thereis$+) '(apply$-badge 3 1 :fn nil nil)) (equal (apply$-userfn 'thereis$+ args) (thereis$+ (car args) (car (cdr args)) (car (cdr (cdr args))))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-thereis$-1 (implies (fn-equal fn fn-equiv) (equal (thereis$ fn lst) (thereis$ fn-equiv lst))) :rule-classes (:congruence))
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$-warrant-thereis$-definition (equal (apply$-warrant-thereis$) (let ((args (apply$-warrant-thereis$-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'thereis$) '(apply$-badge 2 1 :fn nil)) (equal (apply$-userfn 'thereis$ args) (thereis$ (car args) (car (cdr args)))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-always$+-1 (implies (fn-equal fn fn-equiv) (equal (always$+ fn globals lst) (always$+ fn-equiv globals lst))) :rule-classes (:congruence))
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$-warrant-always$+-definition (equal (apply$-warrant-always$+) (let ((args (apply$-warrant-always$+-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'always$+) '(apply$-badge 3 1 :fn nil nil)) (equal (apply$-userfn 'always$+ args) (always$+ (car args) (car (cdr args)) (car (cdr (cdr args))))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-always$-1 (implies (fn-equal fn fn-equiv) (equal (always$ fn lst) (always$ fn-equiv lst))) :rule-classes (:congruence))
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$-warrant-always$-definition (equal (apply$-warrant-always$) (let ((args (apply$-warrant-always$-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'always$) '(apply$-badge 2 1 :fn nil)) (equal (apply$-userfn 'always$ args) (always$ (car args) (car (cdr args)))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-sum$+-1 (implies (fn-equal fn fn-equiv) (equal (sum$+ fn globals lst) (sum$+ fn-equiv globals lst))) :rule-classes (:congruence))
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$-warrant-sum$+-definition (equal (apply$-warrant-sum$+) (let ((args (apply$-warrant-sum$+-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'sum$+) '(apply$-badge 3 1 :fn nil nil)) (equal (apply$-userfn 'sum$+ args) (sum$+ (car args) (car (cdr args)) (car (cdr (cdr args))))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-sum$+-ac-1 (implies (fn-equal fn fn-equiv) (equal (sum$+-ac fn globals lst ac) (sum$+-ac fn-equiv globals lst ac))) :rule-classes (:congruence))
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$-warrant-sum$+-ac-definition (equal (apply$-warrant-sum$+-ac) (let ((args (apply$-warrant-sum$+-ac-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'sum$+-ac) '(apply$-badge 4 1 :fn nil nil nil)) (equal (apply$-userfn 'sum$+-ac args) (sum$+-ac (car args) (car (cdr args)) (car (cdr (cdr args))) (car (cdr (cdr (cdr args)))))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-sum$-1 (implies (fn-equal fn fn-equiv) (equal (sum$ fn lst) (sum$ fn-equiv lst))) :rule-classes (:congruence))
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$-warrant-sum$-definition (equal (apply$-warrant-sum$) (let ((args (apply$-warrant-sum$-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'sum$) '(apply$-badge 2 1 :fn nil)) (equal (apply$-userfn 'sum$ args) (sum$ (car args) (car (cdr args)))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-sum$-ac-1 (implies (fn-equal fn fn-equiv) (equal (sum$-ac fn lst ac) (sum$-ac fn-equiv lst ac))) :rule-classes (:congruence))
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$-warrant-sum$-ac-definition (equal (apply$-warrant-sum$-ac) (let ((args (apply$-warrant-sum$-ac-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'sum$-ac) '(apply$-badge 3 1 :fn nil nil)) (equal (apply$-userfn 'sum$-ac args) (sum$-ac (car args) (car (cdr args)) (car (cdr (cdr args))))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-when$+-1 (implies (fn-equal fn fn-equiv) (equal (when$+ fn globals lst) (when$+ fn-equiv globals lst))) :rule-classes (:congruence))
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$-warrant-when$+-definition (equal (apply$-warrant-when$+) (let ((args (apply$-warrant-when$+-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'when$+) '(apply$-badge 3 1 :fn nil nil)) (equal (apply$-userfn 'when$+ args) (when$+ (car args) (car (cdr args)) (car (cdr (cdr args))))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-when$+-ac-1 (implies (fn-equal fn fn-equiv) (equal (when$+-ac fn globals lst ac) (when$+-ac fn-equiv globals lst ac))) :rule-classes (:congruence))
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$-warrant-when$+-ac-definition (equal (apply$-warrant-when$+-ac) (let ((args (apply$-warrant-when$+-ac-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'when$+-ac) '(apply$-badge 4 1 :fn nil nil nil)) (equal (apply$-userfn 'when$+-ac args) (when$+-ac (car args) (car (cdr args)) (car (cdr (cdr args))) (car (cdr (cdr (cdr args)))))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-when$-1 (implies (fn-equal fn fn-equiv) (equal (when$ fn lst) (when$ fn-equiv lst))) :rule-classes (:congruence))
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$-warrant-when$-definition (equal (apply$-warrant-when$) (let ((args (apply$-warrant-when$-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'when$) '(apply$-badge 2 1 :fn nil)) (equal (apply$-userfn 'when$ args) (when$ (car args) (car (cdr args)))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-when$-ac-1 (implies (fn-equal fn fn-equiv) (equal (when$-ac fn lst ac) (when$-ac fn-equiv lst ac))) :rule-classes (:congruence))
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$-warrant-when$-ac-definition (equal (apply$-warrant-when$-ac) (let ((args (apply$-warrant-when$-ac-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'when$-ac) '(apply$-badge 3 1 :fn nil nil)) (equal (apply$-userfn 'when$-ac args) (when$-ac (car args) (car (cdr args)) (car (cdr (cdr args))))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-until$+-1 (implies (fn-equal fn fn-equiv) (equal (until$+ fn globals lst) (until$+ fn-equiv globals lst))) :rule-classes (:congruence))
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$-warrant-until$+-definition (equal (apply$-warrant-until$+) (let ((args (apply$-warrant-until$+-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'until$+) '(apply$-badge 3 1 :fn nil nil)) (equal (apply$-userfn 'until$+ args) (until$+ (car args) (car (cdr args)) (car (cdr (cdr args))))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-until$+-ac-1 (implies (fn-equal fn fn-equiv) (equal (until$+-ac fn globals lst ac) (until$+-ac fn-equiv globals lst ac))) :rule-classes (:congruence))
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$-warrant-until$+-ac-definition (equal (apply$-warrant-until$+-ac) (let ((args (apply$-warrant-until$+-ac-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'until$+-ac) '(apply$-badge 4 1 :fn nil nil nil)) (equal (apply$-userfn 'until$+-ac args) (until$+-ac (car args) (car (cdr args)) (car (cdr (cdr args))) (car (cdr (cdr (cdr args)))))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-until$-1 (implies (fn-equal fn fn-equiv) (equal (until$ fn lst) (until$ fn-equiv lst))) :rule-classes (:congruence))
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$-warrant-until$-definition (equal (apply$-warrant-until$) (let ((args (apply$-warrant-until$-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'until$) '(apply$-badge 2 1 :fn nil)) (equal (apply$-userfn 'until$ args) (until$ (car args) (car (cdr args)))))))) :rule-classes :definition)
Theorem:
(defthm fn-equal-implies-equal-until$-ac-1 (implies (fn-equal fn fn-equiv) (equal (until$-ac fn lst ac) (until$-ac fn-equiv lst ac))) :rule-classes (:congruence))
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$-warrant-until$-ac-definition (equal (apply$-warrant-until$-ac) (let ((args (apply$-warrant-until$-ac-witness))) (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'until$-ac) '(apply$-badge 3 1 :fn nil nil)) (equal (apply$-userfn 'until$-ac args) (until$-ac (car args) (car (cdr args)) (car (cdr (cdr args))))))))) :rule-classes :definition)
Theorem:
(defthm natp-from-to-by-measure (natp (from-to-by-measure i j)) :rule-classes :type-prescription)
Theorem:
(defthm fn-equal-is-an-equivalence (and (booleanp (fn-equal x y)) (fn-equal x x) (implies (fn-equal x y) (fn-equal y x)) (implies (and (fn-equal x y) (fn-equal y z)) (fn-equal x z))) :rule-classes (:equivalence))
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 apply$-userfn-takes-arity-args (implies (badge-userfn fn) (equal (apply$-userfn fn args) (apply$-userfn fn (take (apply$-badge-arity (badge-userfn fn)) args)))) :rule-classes nil)
Theorem:
(defthm badge-userfn-type (implies (badge-userfn fn) (apply$-badgep (badge-userfn fn))) :rule-classes ((:forward-chaining)))
Theorem:
(defthm stringp-df-string (stringp (df-string x)) :rule-classes :type-prescription)
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 rationalp-df-rationalize (rationalp (df-rationalize x)) :rule-classes :type-prescription)
Theorem:
(defthm rationalp-df-pi (rationalp (df-pi)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-df-pi (dfp (df-pi)))
Theorem:
(defthm rationalp-df-atanh-fn (rationalp (df-atanh-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-df-atanh-fn (dfp (df-atanh-fn x)))
Theorem:
(defthm rationalp-df-acosh-fn (rationalp (df-acosh-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-df-acosh-fn (dfp (df-acosh-fn x)))
Theorem:
(defthm rationalp-df-asinh-fn (rationalp (df-asinh-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-df-asinh-fn (dfp (df-asinh-fn x)))
Theorem:
(defthm rationalp-df-tanh-fn (rationalp (df-tanh-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-df-tanh-fn (dfp (df-tanh-fn x)))
Theorem:
(defthm rationalp-df-cosh-fn (rationalp (df-cosh-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-df-cosh-fn (dfp (df-cosh-fn x)))
Theorem:
(defthm rationalp-df-sinh-fn (rationalp (df-sinh-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-df-sinh-fn (dfp (df-sinh-fn x)))
Theorem:
(defthm rationalp-df-atan-fn (rationalp (df-atan-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-df-atan-fn (dfp (df-atan-fn x)))
Theorem:
(defthm rationalp-df-acos-fn (rationalp (df-acos-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-df-acos-fn (dfp (df-acos-fn x)))
Theorem:
(defthm rationalp-df-asin-fn (rationalp (df-asin-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-df-asin-fn (dfp (df-asin-fn x)))
Theorem:
(defthm rationalp-df-tan-fn (rationalp (df-tan-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-df-tan-fn (dfp (df-tan-fn x)))
Theorem:
(defthm rationalp-df-cos-fn (rationalp (df-cos-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-df-cos-fn (dfp (df-cos-fn x)))
Theorem:
(defthm rationalp-df-sin-fn (rationalp (df-sin-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-df-sin-fn (dfp (df-sin-fn x)))
Theorem:
(defthm rationalp-df-abs-fn (rationalp (df-abs-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-df-abs-fn (dfp (df-abs-fn x)))
Theorem:
(defthm rationalp-unary-df-log (rationalp (unary-df-log x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-unary-df-log (dfp (unary-df-log x)))
Theorem:
(defthm rationalp-binary-df-log (rationalp (binary-df-log x y)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-binary-df-log (dfp (binary-df-log x y)))
Theorem:
(defthm rationalp-df-sqrt-fn (rationalp (df-sqrt-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-df-sqrt-fn (dfp (df-sqrt-fn x)))
Theorem:
(defthm rationalp-df-exp-fn (rationalp (df-exp-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-df-exp-fn (dfp (df-exp-fn x)))
Theorem:
(defthm rationalp-df-expt-fn (rationalp (df-expt-fn x y)) :rule-classes :type-prescription)
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-implies-rationalp (implies (dfp x) (rationalp x)) :rule-classes :compound-recognizer)
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 rationalp-to-df (rationalp (to-df x)) :rule-classes :type-prescription)
Theorem:
(defthm symbol-listp-strict-merge-sort-symbol< (implies (symbol-listp x) (symbol-listp (strict-merge-sort-symbol< x))))
Theorem:
(defthm true-listp-explode-atom (true-listp (explode-atom n print-base)) :rule-classes :type-prescription)
Theorem:
(defthm true-listp-chars-for-tilde-@-clause-id-phrase/periods (true-listp (chars-for-tilde-@-clause-id-phrase/periods lst)) :rule-classes :type-prescription)
Theorem:
(defthm pos-listp-forward-to-integer-listp (implies (pos-listp x) (integer-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm d-pos-listp-forward-to-true-listp (implies (d-pos-listp x) (true-listp x)) :rule-classes :forward-chaining)
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 integerp-nth-2-var-fn-count-1 (implies (integerp p-fn-count-acc) (integerp (nth 2 (var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table)))) :rule-classes ((:forward-chaining :trigger-terms ((var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table)) :corollary (implies (integerp p-fn-count-acc) (and (integerp (nth 2 (var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table))) (integerp (mv-nth 2 (var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table))))))))
Theorem:
(defthm integerp-nth-1-var-fn-count-1 (implies (integerp fn-count-acc) (integerp (nth 1 (var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table)))) :rule-classes ((:forward-chaining :trigger-terms ((var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table)) :corollary (implies (integerp fn-count-acc) (and (integerp (nth 1 (var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table))) (integerp (mv-nth 1 (var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table))))))))
Theorem:
(defthm integerp-nth-0-var-fn-count-1 (implies (integerp var-count-acc) (integerp (nth 0 (var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table)))) :rule-classes ((:forward-chaining :trigger-terms ((var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table)) :corollary (implies (integerp var-count-acc) (and (integerp (nth 0 (var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table))) (integerp (mv-nth 0 (var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table))) (integerp (car (var-fn-count-1 flg x var-count-acc fn-count-acc p-fn-count-acc invisible-fns invisible-fns-table))))))))
Theorem:
(defthm symbol-listp-cdr-assoc-equal (implies (symbol-list-listp x) (symbol-listp (cdr (assoc-equal key x)))))
Theorem:
(defthm fn-count-1-type (implies (and (integerp fn-count-acc) (integerp p-fn-count-acc)) (and (integerp (car (fn-count-1 flag term fn-count-acc p-fn-count-acc))) (integerp (mv-nth 0 (fn-count-1 flag term fn-count-acc p-fn-count-acc))) (integerp (mv-nth 1 (fn-count-1 flag term fn-count-acc p-fn-count-acc))) (integerp (nth 0 (fn-count-1 flag term fn-count-acc p-fn-count-acc))) (integerp (nth 1 (fn-count-1 flag term fn-count-acc p-fn-count-acc))))) :rule-classes ((:forward-chaining :trigger-terms ((fn-count-1 flag term fn-count-acc p-fn-count-acc)))))
Theorem:
(defthm fn-count-evg-rec-bound (< (fn-count-evg-rec evg acc calls) 536870912) :rule-classes :linear)
Theorem:
(defthm fn-count-evg-rec-type-prescription (implies (natp acc) (natp (fn-count-evg-rec evg acc calls))) :rule-classes :type-prescription)
Theorem:
(defthm canonical-pathname-type (or (equal (canonical-pathname x dir-p state) nil) (stringp (canonical-pathname x dir-p state))) :rule-classes :type-prescription)
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 acl2-count-car-cdr-linear (implies (consp x) (equal (acl2-count x) (+ 1 (acl2-count (car x)) (acl2-count (cdr x))))) :rule-classes :linear)
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 true-listp-merge-sort-lexorder (implies (and (true-listp l1) (true-listp l2)) (true-listp (merge-lexorder l1 l2 acc))) :rule-classes :type-prescription)
Theorem:
(defthm lexorder-total (or (lexorder x y) (lexorder y x)) :rule-classes ((:forward-chaining :corollary (implies (not (lexorder x y)) (lexorder y x)))))
Theorem:
(defthm lexorder-transitive (implies (and (lexorder x y) (lexorder y z)) (lexorder x z)) :rule-classes ((:rewrite :match-free :all)))
Theorem:
(defthm lexorder-anti-symmetric (implies (and (lexorder x y) (lexorder y x)) (equal x y)) :rule-classes :forward-chaining)
Theorem:
(defthm lexorder-reflexive (lexorder x x))
Theorem:
(defthm alphorder-total (implies (and (not (consp x)) (not (consp y))) (or (alphorder x y) (alphorder y x))) :rule-classes ((:forward-chaining :corollary (implies (and (not (alphorder x y)) (not (consp x)) (not (consp y))) (alphorder y x)))))
Theorem:
(defthm alphorder-anti-symmetric (implies (and (not (consp x)) (not (consp y)) (alphorder x y) (alphorder y x)) (equal x y)) :rule-classes ((:forward-chaining :corollary (implies (and (alphorder x y) (not (consp x)) (not (consp y))) (iff (alphorder y x) (equal x y))) :hints (("Goal" :in-theory (disable alphorder))))))
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 bad-atom-compound-recognizer (iff (bad-atom x) (not (or (consp x) (acl2-numberp x) (symbolp x) (characterp x) (stringp x)))) :rule-classes :compound-recognizer)
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 add-def-complex (equal (+ x y) (complex (+ (realpart x) (realpart y)) (+ (imagpart x) (imagpart y)))) :rule-classes nil)
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 state-p1-update-print-base (implies (and (state-p1 state) (force (print-base-p val))) (state-p1 (update-nth 2 (add-pair 'print-base val (nth 2 state)) state))) :rule-classes ((:forward-chaining :trigger-terms ((update-nth 2 (add-pair 'print-base val (nth 2 state)) state)))))
Theorem:
(defthm state-p1-update-main-timer (implies (state-p1 state) (state-p1 (update-nth 2 (add-pair 'main-timer val (nth 2 state)) state))) :rule-classes ((:forward-chaining :trigger-terms ((update-nth 2 (add-pair 'main-timer val (nth 2 state)) state)))))
Theorem:
(defthm ordered-symbol-alistp-add-pair-forward (implies (and (symbolp key) (ordered-symbol-alistp l)) (ordered-symbol-alistp (add-pair key value l))) :rule-classes ((:forward-chaining :trigger-terms ((add-pair key value l)))))
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 nth-0-read-run-time-type-prescription (implies (state-p1 state) (rationalp (nth 0 (read-run-time state)))) :rule-classes ((:type-prescription :typed-term (nth 0 (read-run-time state)))))
Theorem:
(defthm read-acl2-oracle-preserves-state-p1 (implies (state-p1 state) (state-p1 (nth 2 (read-acl2-oracle state)))) :rule-classes ((:forward-chaining :trigger-terms ((nth 2 (read-acl2-oracle state))))))
Theorem:
(defthm read-run-time-preserves-state-p1 (implies (state-p1 state) (state-p1 (nth 1 (read-run-time state)))) :rule-classes ((:forward-chaining :trigger-terms ((nth 1 (read-run-time state))))))
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 random$-linear (and (<= 0 (car (random$ n state))) (implies (posp n) (< (car (random$ n state)) n))) :rule-classes :linear)
Theorem:
(defthm natp-random$ (natp (car (random$ n state))) :rule-classes :type-prescription)
Theorem:
(defthm true-listp-subseq-type-prescription (implies (not (stringp seq)) (true-listp (subseq seq start end))) :rule-classes :type-prescription)
Theorem:
(defthm stringp-subseq-type-prescription (implies (stringp seq) (stringp (subseq seq start end))) :rule-classes :type-prescription)
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 true-listp-update-nth (implies (true-listp l) (true-listp (update-nth key val l))) :rule-classes :type-prescription)
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 string-alistp-forward-to-alistp (implies (string-alistp x) (alistp x)) :rule-classes :forward-chaining)
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 characterp-char-upcase (characterp (char-upcase x)) :rule-classes :type-prescription)
Theorem:
(defthm characterp-char-downcase (characterp (char-downcase x)) :rule-classes :type-prescription)
Theorem:
(defthm standard-char-p-forward-to-characterp (implies (standard-char-p x) (characterp x)) :rule-classes :forward-chaining)
Theorem:
(defthm upper-case-p-forward-to-alpha-char-p (implies (upper-case-p x) (alpha-char-p x)) :rule-classes :forward-chaining)
Theorem:
(defthm lower-case-p-forward-to-alpha-char-p (implies (lower-case-p x) (alpha-char-p x)) :rule-classes :forward-chaining)
Theorem:
(defthm natp-position-ac (implies (and (integerp acc) (<= 0 acc)) (or (equal (position-ac item lst acc) nil) (and (integerp (position-ac item lst acc)) (<= 0 (position-ac item lst acc))))) :rule-classes :type-prescription)
Theorem:
(defthm true-listp-cadr-assoc-eq-for-open-channels-p (implies (open-channels-p alist) (true-listp (cadr (assoc-eq key alist)))) :rule-classes ((:forward-chaining :trigger-terms ((cadr (assoc-eq key alist))))))
Theorem:
(defthm true-list-listp-forward-to-true-listp-assoc-equal (implies (true-list-listp l) (true-listp (assoc-equal key l))) :rule-classes (:type-prescription (:forward-chaining :trigger-terms ((assoc-equal key l)))))
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 symbol-equality (implies (and (or (symbolp s1) (symbolp s2)) (equal (symbol-name s1) (symbol-name s2)) (equal (symbol-package-name s1) (symbol-package-name s2))) (equal s1 s2)) :rule-classes nil)
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 unsigned-byte-p-forward-to-nonnegative-integerp (implies (unsigned-byte-p n x) (and (integerp x) (<= 0 x))) :rule-classes :forward-chaining)
Theorem:
(defthm signed-byte-p-forward-to-integerp (implies (signed-byte-p n x) (integerp x)) :rule-classes :forward-chaining)
Theorem:
(defthm integer-range-p-forward (implies (and (integer-range-p lower (1+ upper-1) x) (integerp upper-1)) (and (integerp x) (<= lower x) (<= x upper-1))) :rule-classes :forward-chaining)
Theorem:
(defthm true-listp-explode-nonnegative-integer (implies (true-listp ans) (true-listp (explode-nonnegative-integer n print-base ans))) :rule-classes :type-prescription)
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 all-boundp-preserves-assoc-equal (implies (and (all-boundp tbl1 tbl2) (assoc-equal x tbl1)) (assoc-equal x tbl2)) :rule-classes nil)
Theorem:
(defthm state-p1-forward (implies (state-p1 x) (and (true-listp x) (equal (length x) 11) (open-channels-p (nth 0 x)) (open-channels-p (nth 1 x)) (ordered-symbol-alistp (nth 2 x)) (all-boundp *initial-global-table* (nth 2 x)) (plist-worldp (cdr (assoc 'current-acl2-world (nth 2 x)))) (symbol-alistp (getpropc 'acl2-defaults-table 'table-alist nil (cdr (assoc 'current-acl2-world (nth 2 x))))) (timer-alistp (cdr (assoc 'timer-alist (nth 2 x)))) (print-base-p (cdr (assoc 'print-base (nth 2 x)))) (known-package-alistp (getpropc 'known-package-alist 'global-value nil (cdr (assoc 'current-acl2-world (nth 2 x))))) (integer-listp (nth 3 x)) (true-listp (nth 4 x)) (file-clock-p (nth 5 x)) (readable-files-p (nth 6 x)) (written-files-p (nth 7 x)) (read-files-p (nth 8 x)) (writeable-files-p (nth 9 x)) (symbol-alistp (nth 10 x)))) :rule-classes :forward-chaining)
Theorem:
(defthm writeable-files-p-forward-to-writable-file-listp (implies (writeable-files-p x) (writable-file-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm writable-file-listp-forward-to-true-list-listp (implies (writable-file-listp x) (true-list-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm writable-file-listp1-forward-to-true-listp-and-consp (implies (writable-file-listp1 x) (and (true-listp x) (consp x))) :rule-classes :forward-chaining)
Theorem:
(defthm read-files-p-forward-to-read-file-listp (implies (read-files-p x) (read-file-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm read-file-listp-forward-to-true-list-listp (implies (read-file-listp x) (true-list-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm read-file-listp1-forward-to-true-listp-and-consp (implies (read-file-listp1 x) (and (true-listp x) (consp x))) :rule-classes :forward-chaining)
Theorem:
(defthm written-files-p-forward-to-written-file-listp (implies (written-files-p x) (written-file-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm written-file-listp-forward-to-true-list-listp-and-alistp (implies (written-file-listp x) (and (true-list-listp x) (alistp x))) :rule-classes :forward-chaining)
Theorem:
(defthm written-file-forward-to-true-listp-and-consp (implies (written-file x) (and (true-listp x) (consp x))) :rule-classes :forward-chaining)
Theorem:
(defthm readable-files-p-forward-to-readable-files-listp (implies (readable-files-p x) (readable-files-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm readable-files-listp-forward-to-true-list-listp-and-alistp (implies (readable-files-listp x) (and (true-list-listp x) (alistp x))) :rule-classes :forward-chaining)
Theorem:
(defthm readable-file-forward-to-true-listp-and-consp (implies (readable-file x) (and (true-listp x) (consp x))) :rule-classes :forward-chaining)
Theorem:
(defthm file-clock-p-forward-to-integerp (implies (file-clock-p x) (natp x)) :rule-classes :forward-chaining)
Theorem:
(defthm open-channels-p-forward (implies (open-channels-p x) (and (ordered-symbol-alistp x) (true-list-listp x))) :rule-classes :forward-chaining)
Theorem:
(defthm open-channel1-forward-to-true-listp-and-consp (implies (open-channel1 x) (and (true-listp x) (consp x))) :rule-classes :forward-chaining)
Theorem:
(defthm typed-io-listp-forward-to-true-listp (implies (typed-io-listp x typ) (true-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm timer-alistp-forward-to-true-list-listp-and-symbol-alistp (implies (timer-alistp x) (and (true-list-listp x) (symbol-alistp x))) :rule-classes :forward-chaining)
Theorem:
(defthm known-package-alistp-forward-to-true-list-listp-and-alistp (implies (known-package-alistp x) (and (true-list-listp x) (alistp x))) :rule-classes :forward-chaining)
Theorem:
(defthm nat-listp-forward-to-integer-listp (implies (nat-listp x) (integer-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm integer-listp-forward-to-rational-listp (implies (integer-listp x) (rational-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm rational-listp-forward-to-acl2-number-listp (implies (rational-listp x) (acl2-number-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm acl2-number-listp-forward-to-true-listp (implies (acl2-number-listp x) (true-listp x)) :rule-classes :forward-chaining)
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 array2p-linear (implies (array2p name l) (and (< 0 (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (< 0 (cadr (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (< (* (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))) (cadr (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (cadr (assoc-keyword :maximum-length (cdr (assoc-eq :header l))))) (<= (cadr (assoc-keyword :maximum-length (cdr (assoc-eq :header l)))) (array-maximum-length-bound)))) :rule-classes ((:linear :match-free :all)))
Theorem:
(defthm array2p-forward (implies (array2p name l) (and (symbolp name) (alistp l) (keyword-value-listp (cdr (assoc-eq :header l))) (true-listp (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))) (equal (length (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))) 2) (integerp (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (integerp (cadr (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (integerp (cadr (assoc-keyword :maximum-length (cdr (assoc-eq :header l))))) (< 0 (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (< 0 (cadr (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (< (* (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))) (cadr (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (cadr (assoc-keyword :maximum-length (cdr (assoc-eq :header l))))) (<= (cadr (assoc-keyword :maximum-length (cdr (assoc-eq :header l)))) (array-maximum-length-bound)) (bounded-integer-alistp2 l (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))) (cadr (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))))) :rule-classes :forward-chaining)
Theorem:
(defthm array1p-linear (implies (array1p name l) (and (< 0 (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (< (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))) (cadr (assoc-keyword :maximum-length (cdr (assoc-eq :header l))))) (<= (cadr (assoc-keyword :maximum-length (cdr (assoc-eq :header l)))) (array-maximum-length-bound)))) :rule-classes ((:linear :match-free :all)))
Theorem:
(defthm array1p-forward (implies (array1p name l) (and (symbolp name) (alistp l) (keyword-value-listp (cdr (assoc-eq :header l))) (true-listp (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))) (equal (length (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))) 1) (integerp (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (integerp (cadr (assoc-keyword :maximum-length (cdr (assoc-eq :header l))))) (< 0 (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))) (< (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l))))) (cadr (assoc-keyword :maximum-length (cdr (assoc-eq :header l))))) (<= (cadr (assoc-keyword :maximum-length (cdr (assoc-eq :header l)))) (array-maximum-length-bound)) (bounded-integer-alistp l (car (cadr (assoc-keyword :dimensions (cdr (assoc-eq :header l)))))))) :rule-classes :forward-chaining)
Theorem:
(defthm consp-assoc-equal (implies (alistp l) (or (consp (assoc-equal name l)) (equal (assoc-equal name l) nil))) :rule-classes (:type-prescription (:forward-chaining :trigger-terms ((assoc-equal name l)))))
Theorem:
(defthm keyword-value-listp-assoc-keyword (implies (keyword-value-listp l) (keyword-value-listp (assoc-keyword key l))) :rule-classes ((:forward-chaining :trigger-terms ((assoc-keyword key l)))))
Theorem:
(defthm bounded-integer-alistp-forward-to-eqlable-alistp (implies (bounded-integer-alistp x n) (eqlable-alistp x)) :rule-classes :forward-chaining)
Theorem:
(defthm fixnat-alistp-forward-to-nat-alistp (implies (fixnat-alistp x) (nat-alistp x)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-char-code (implies (and (characterp x) (characterp y)) (implies (equal (char-code x) (char-code y)) (equal x y))) :rule-classes nil)
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 ordered-symbol-alistp-forward-to-symbol-alistp (implies (ordered-symbol-alistp x) (symbol-alistp x)) :rule-classes :forward-chaining)
Theorem:
(defthm plist-worldp-forward-to-assoc-eq-equal-alistp (implies (plist-worldp x) (assoc-eq-equal-alistp x)) :rule-classes :forward-chaining)
Theorem:
(defthm true-listp-substitute-type-prescription (implies (not (stringp seq)) (true-listp (substitute new old seq))) :rule-classes :type-prescription)
Theorem:
(defthm stringp-substitute-type-prescription (implies (stringp seq) (stringp (substitute new old seq))) :rule-classes :type-prescription)
Theorem:
(defthm string<-irreflexive (not (string< s s)))
Theorem:
(defthm string<-l-irreflexive (not (string<-l x x i)))
Theorem:
(defthm rationalp-expt-type-prescription (implies (rationalp r) (rationalp (expt r i))) :rule-classes :type-prescription)
Theorem:
(defthm expt-type-prescription-non-zero-base (implies (and (acl2-numberp r) (not (equal r 0))) (not (equal (expt r i) 0))) :rule-classes :type-prescription)
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 natp-position-equal-ac (implies (natp acc) (or (natp (position-equal-ac item lst acc)) (equal (position-equal-ac item lst acc) nil))) :rule-classes :type-prescription)
Theorem:
(defthm natp-position-ac-eql-exec (implies (natp acc) (or (natp (position-ac-eql-exec item lst acc)) (equal (position-ac-eql-exec item lst acc) nil))) :rule-classes :type-prescription)
Theorem:
(defthm natp-position-ac-eq-exec (implies (natp acc) (or (natp (position-ac-eq-exec item lst acc)) (equal (position-ac-eq-exec item lst acc) nil))) :rule-classes :type-prescription)
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 pseudo-termp-consp-forward (implies (and (pseudo-termp x) (consp x)) (true-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm pseudo-term-listp-forward-to-true-listp (implies (pseudo-term-listp x) (true-listp x)) :rule-classes :forward-chaining)
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 true-listp-nthcdr-type-prescription (implies (true-listp x) (true-listp (nthcdr n x))) :rule-classes :type-prescription)
Theorem:
(defthm true-list-listp-forward-to-true-listp (implies (true-list-listp x) (true-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm keyword-value-listp-forward-to-true-listp (implies (keyword-value-listp x) (true-listp x)) :rule-classes :forward-chaining)
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 true-listp-first-n-ac-type-prescription (true-listp (first-n-ac i l ac)) :rule-classes :type-prescription)
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 true-listp-revappend-type-prescription (implies (true-listp y) (true-listp (revappend x y))) :rule-classes :type-prescription)
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 symbol-package-name-of-symbol-is-not-empty-string (implies (symbolp x) (not (equal (symbol-package-name x) ""))) :rule-classes ((:forward-chaining :trigger-terms ((symbol-package-name x)))))
Theorem:
(defthm keywordp-forward-to-symbolp (implies (keywordp x) (symbolp x)) :rule-classes :forward-chaining)
Theorem:
(defthm characterp-nth (implies (and (character-listp x) (<= 0 i) (< i (len x))) (characterp (nth i x))))
Theorem:
(defthm eqlable-listp-forward-to-atom-listp (implies (eqlable-listp x) (atom-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm atom-listp-forward-to-true-listp (implies (atom-listp x) (true-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm standard-char-listp-forward-to-character-listp (implies (standard-char-listp x) (character-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm character-listp-forward-to-eqlable-listp (implies (character-listp x) (eqlable-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm o-p-implies-o<g (implies (o-p a) (o<g a)))
Theorem:
(defthm posp-compound-recognizer (equal (posp x) (and (integerp x) (< 0 x))) :rule-classes :compound-recognizer)
Theorem:
(defthm bitp-as-inequality (implies (bitp x) (and (natp x) (< x 2))) :rule-classes :tau-system)
Theorem:
(defthm bitp-compound-recognizer (equal (bitp x) (or (equal x 0) (equal x 1))) :rule-classes :compound-recognizer)
Theorem:
(defthm nat-alistp-forward-to-eqlable-alistp (implies (nat-alistp x) (eqlable-alistp x)) :rule-classes :forward-chaining)
Theorem:
(defthm natp-compound-recognizer (equal (natp x) (and (integerp x) (<= 0 x))) :rule-classes :compound-recognizer)
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 basic-tau-rules (and (implies (natp v) (not (minusp v))) (implies (natp v) (integerp v)) (implies (posp v) (natp v)) (implies (minusp v) (acl2-numberp v)) (implies (integerp v) (rationalp v)) (implies (rationalp v) (not (complex-rationalp v))) (implies (rationalp v) (not (characterp v))) (implies (rationalp v) (not (stringp v))) (implies (rationalp v) (not (consp v))) (implies (rationalp v) (not (symbolp v))) (implies (complex-rationalp v) (not (characterp v))) (implies (complex-rationalp v) (not (stringp v))) (implies (complex-rationalp v) (not (consp v))) (implies (complex-rationalp v) (not (symbolp v))) (implies (characterp v) (not (stringp v))) (implies (characterp v) (not (consp v))) (implies (characterp v) (not (symbolp v))) (implies (stringp v) (not (consp v))) (implies (stringp v) (not (symbolp v))) (implies (consp v) (not (symbolp v))) (implies (booleanp v) (symbolp v)) (booleanp (equal x y)) (booleanp (< x y))) :rule-classes :tau-system)
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-forward-to-symbol-listp (implies (boolean-listp x) (symbol-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm boolean-listp-forward (implies (boolean-listp (cons a lst)) (and (booleanp a) (boolean-listp lst))) :rule-classes :forward-chaining)
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 zip-compound-recognizer (equal (zip x) (or (not (integerp x)) (equal x 0))) :rule-classes :compound-recognizer)
Theorem:
(defthm zp-open (implies (syntaxp (not (variablep x))) (equal (zp x) (if (integerp x) (<= x 0) t))))
Theorem:
(defthm zp-compound-recognizer (equal (zp x) (or (not (integerp x)) (<= x 0))) :rule-classes :compound-recognizer)
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 character-alistp-forward-to-eqlable-alistp (implies (character-alistp x) (eqlable-alistp x)) :rule-classes :forward-chaining)
Theorem:
(defthm symbol-alistp-forward-to-eqlable-alistp (implies (symbol-alistp x) (eqlable-alistp x)) :rule-classes :forward-chaining)
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 true-listp-append (implies (true-listp b) (true-listp (append a b))) :rule-classes :type-prescription)
Theorem:
(defthm symbol-listp-forward-to-eqlable-listp (implies (symbol-listp x) (eqlable-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm eqlable-alistp-forward-to-alistp (implies (eqlable-alistp x) (alistp x)) :rule-classes :forward-chaining)
Theorem:
(defthm alistp-forward-to-true-listp (implies (alistp x) (true-listp x)) :rule-classes :forward-chaining)
Theorem:
(defthm eqlablep-recog (equal (eqlablep x) (or (acl2-numberp x) (symbolp x) (characterp x))) :rule-classes :compound-recognizer)
Theorem:
(defthm booleanp-compound-recognizer (equal (booleanp x) (or (equal x t) (equal x nil))) :rule-classes :compound-recognizer)
Theorem:
(defthm iff-implies-equal-not (implies (iff x x-equiv) (equal (not x) (not x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm iff-implies-equal-implies-2 (implies (iff y y-equiv) (equal (implies x y) (implies x y-equiv))) :rule-classes (:congruence))
Theorem:
(defthm iff-implies-equal-implies-1 (implies (iff x x-equiv) (equal (implies x y) (implies x-equiv y))) :rule-classes (:congruence))
Theorem:
(defthm iff-is-an-equivalence (and (booleanp (iff x y)) (iff x x) (implies (iff x y) (iff y x)) (implies (and (iff x y) (iff y z)) (iff x z))) :rule-classes (:equivalence))
Theorem:
(defthm rationalp-constrained-df-pi (rationalp (constrained-df-pi)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-constrained-df-pi (dfp (constrained-df-pi)))
Theorem:
(defthm rationalp-constrained-df-atanh-fn (rationalp (constrained-df-atanh-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-constrained-df-atanh-fn (dfp (constrained-df-atanh-fn x)))
Theorem:
(defthm rationalp-constrained-df-acosh-fn (rationalp (constrained-df-acosh-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-constrained-df-acosh-fn (dfp (constrained-df-acosh-fn x)))
Theorem:
(defthm rationalp-constrained-df-asinh-fn (rationalp (constrained-df-asinh-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-constrained-df-asinh-fn (dfp (constrained-df-asinh-fn x)))
Theorem:
(defthm rationalp-constrained-df-tanh-fn (rationalp (constrained-df-tanh-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-constrained-df-tanh-fn (dfp (constrained-df-tanh-fn x)))
Theorem:
(defthm rationalp-constrained-df-cosh-fn (rationalp (constrained-df-cosh-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-constrained-df-cosh-fn (dfp (constrained-df-cosh-fn x)))
Theorem:
(defthm rationalp-constrained-df-sinh-fn (rationalp (constrained-df-sinh-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-constrained-df-sinh-fn (dfp (constrained-df-sinh-fn x)))
Theorem:
(defthm rationalp-constrained-df-atan-fn (rationalp (constrained-df-atan-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-constrained-df-atan-fn (dfp (constrained-df-atan-fn x)))
Theorem:
(defthm rationalp-constrained-df-acos-fn (rationalp (constrained-df-acos-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-constrained-df-acos-fn (dfp (constrained-df-acos-fn x)))
Theorem:
(defthm rationalp-constrained-df-asin-fn (rationalp (constrained-df-asin-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-constrained-df-asin-fn (dfp (constrained-df-asin-fn x)))
Theorem:
(defthm rationalp-constrained-df-tan-fn (rationalp (constrained-df-tan-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-constrained-df-tan-fn (dfp (constrained-df-tan-fn x)))
Theorem:
(defthm rationalp-constrained-df-cos-fn (rationalp (constrained-df-cos-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-constrained-df-cos-fn (dfp (constrained-df-cos-fn x)))
Theorem:
(defthm rationalp-constrained-df-sin-fn (rationalp (constrained-df-sin-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-constrained-df-sin-fn (dfp (constrained-df-sin-fn x)))
Theorem:
(defthm rationalp-constrained-df-abs-fn (rationalp (constrained-df-abs-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-constrained-df-abs-fn (dfp (constrained-df-abs-fn x)))
Theorem:
(defthm rationalp-constrained-unary-df-log (rationalp (constrained-unary-df-log x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-constrained-unary-df-log (dfp (constrained-unary-df-log x)))
Theorem:
(defthm rationalp-constrained-binary-df-log (rationalp (constrained-binary-df-log x y)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-constrained-binary-df-log (dfp (constrained-binary-df-log x y)))
Theorem:
(defthm rationalp-constrained-df-sqrt-fn (rationalp (constrained-df-sqrt-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-constrained-df-sqrt-fn (dfp (constrained-df-sqrt-fn x)))
Theorem:
(defthm rationalp-constrained-df-exp-fn (rationalp (constrained-df-exp-fn x)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-constrained-df-exp-fn (dfp (constrained-df-exp-fn x)))
Theorem:
(defthm rationalp-constrained-df-expt-fn (rationalp (constrained-df-expt-fn x y)) :rule-classes :type-prescription)
Theorem:
(defthm dfp-constrained-df-expt-fn (dfp (constrained-df-expt-fn x y)))
Theorem:
(defthm doppelganger-apply$-userfn-takes-arity-args (implies (doppelganger-badge-userfn fn) (equal (doppelganger-apply$-userfn fn args) (doppelganger-apply$-userfn fn (take (caddr (doppelganger-badge-userfn fn)) args)))) :rule-classes nil)
Theorem:
(defthm doppelganger-badge-userfn-type (or (null (doppelganger-badge-userfn fn)) (let ((x (doppelganger-badge-userfn fn))) (and (weak-apply$-badge-p x) (natp (access apply$-badge x :arity)) (natp (access apply$-badge x :out-arity)) (or (eq (access apply$-badge x :ilks) t) (and (true-listp (access apply$-badge x :ilks)) (equal (len (access apply$-badge x :ilks)) (access apply$-badge x :arity)) (not (all-nils (access apply$-badge x :ilks))) (subsetp (access apply$-badge x :ilks) '(nil :fn :expr))))))) :rule-classes nil)
Theorem:
(defthm natp-conjoin-clause-sets-bound (natp (conjoin-clause-sets-bound)) :rule-classes :type-prescription)
Theorem:
(defthm function-symbolp-ev-fncall+-fns-strictp (let ((fn (ev-fncall+-fns fn args wrld big-n safe-mode gc-off t))) (and (symbolp fn) (or (null fn) (function-symbolp fn wrld)))) :rule-classes nil)
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 rationalp-constrained-df-rationalize (rationalp (constrained-df-rationalize x)) :rule-classes :type-prescription)
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 rationalp-df-round (rationalp (df-round x)) :rule-classes :type-prescription)
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 rationalp-constrained-to-df (rationalp (constrained-to-df x)) :rule-classes :type-prescription)
Theorem:
(defthm stringp-constrained-df-string (stringp (constrained-df-string x)) :rule-classes :type-prescription)
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 lower/upper-case-p-non-standard-disjointness (not (and (lower-case-p-non-standard x) (upper-case-p-non-standard x))) :rule-classes nil)
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 alpha-char-p-non-standard-implies-characterp (implies (alpha-char-p-non-standard x) (characterp x)) :rule-classes :forward-chaining)
Theorem:
(defthm lower-case-p-non-standard-implies-alpha-char-p-non-standard (implies (lower-case-p-non-standard x) (alpha-char-p-non-standard x)) :rule-classes :forward-chaining)
Theorem:
(defthm upper-case-p-non-standard-implies-alpha-char-p-non-standard (implies (upper-case-p-non-standard x) (alpha-char-p-non-standard x)) :rule-classes :forward-chaining)
Theorem:
(defthm characterp-char-downcase-non-standard (characterp (char-downcase-non-standard x)) :rule-classes :type-prescription)
Theorem:
(defthm characterp-char-upcase-non-standard (characterp (char-upcase-non-standard x)) :rule-classes :type-prescription)
Theorem:
(defthm booleanp-lower-case-p-non-standard (booleanp (lower-case-p-non-standard x)) :rule-classes :type-prescription)
Theorem:
(defthm booleanp-upper-case-p-non-standard (booleanp (upper-case-p-non-standard x)) :rule-classes :type-prescription)
Theorem:
(defthm booleanp-alpha-char-p-non-standard (booleanp (alpha-char-p-non-standard x)) :rule-classes :type-prescription)
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))))