Built-in axioms and theorems about apply$.
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 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 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 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 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 badge-userfn-type (implies (badge-userfn fn) (apply$-badgep (badge-userfn fn))) :rule-classes ((:forward-chaining)))
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 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$-equivalence-necc (implies (not (equal (ec-call (apply$ fn1 args)) (ec-call (apply$ fn2 args)))) (not (apply$-equivalence fn1 fn2))))
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 natp-from-to-by-measure (natp (from-to-by-measure i j)) :rule-classes :type-prescription)
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 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$-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 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$-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 apply$-warrant-until$-necc (implies (not (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'until$) '(apply$-badge 2 1 :fn nil)) (equal (apply$-userfn 'until$ args) (until$ (car args) (car (cdr args))))))) (not (apply$-warrant-until$))))
Theorem:
(defthm apply$-until$ (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 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$-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 apply$-warrant-until$+-ac-necc (implies (not (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'until$+-ac) '(apply$-badge 4 1 :fn nil nil nil)) (equal (apply$-userfn 'until$+-ac args) (until$+-ac (car args) (car (cdr args)) (car (cdr (cdr args))) (car (cdr (cdr (cdr args))))))))) (not (apply$-warrant-until$+-ac))))
Theorem:
(defthm apply$-until$+-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 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$-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 apply$-warrant-until$+-necc (implies (not (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'until$+) '(apply$-badge 3 1 :fn nil nil)) (equal (apply$-userfn 'until$+ args) (until$+ (car args) (car (cdr args)) (car (cdr (cdr args)))))))) (not (apply$-warrant-until$+))))
Theorem:
(defthm apply$-until$+ (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 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$-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 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$-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 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$-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 apply$-warrant-when$-necc (implies (not (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'when$) '(apply$-badge 2 1 :fn nil)) (equal (apply$-userfn 'when$ args) (when$ (car args) (car (cdr args))))))) (not (apply$-warrant-when$))))
Theorem:
(defthm apply$-when$ (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 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$-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 apply$-warrant-when$+-ac-necc (implies (not (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'when$+-ac) '(apply$-badge 4 1 :fn nil nil nil)) (equal (apply$-userfn 'when$+-ac args) (when$+-ac (car args) (car (cdr args)) (car (cdr (cdr args))) (car (cdr (cdr (cdr args))))))))) (not (apply$-warrant-when$+-ac))))
Theorem:
(defthm apply$-when$+-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 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$-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 apply$-warrant-when$+-necc (implies (not (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'when$+) '(apply$-badge 3 1 :fn nil nil)) (equal (apply$-userfn 'when$+ args) (when$+ (car args) (car (cdr args)) (car (cdr (cdr args)))))))) (not (apply$-warrant-when$+))))
Theorem:
(defthm apply$-when$+ (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 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$-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 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$-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 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$-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 apply$-warrant-sum$-necc (implies (not (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'sum$) '(apply$-badge 2 1 :fn nil)) (equal (apply$-userfn 'sum$ args) (sum$ (car args) (car (cdr args))))))) (not (apply$-warrant-sum$))))
Theorem:
(defthm apply$-sum$ (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 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$-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 apply$-warrant-sum$+-ac-necc (implies (not (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'sum$+-ac) '(apply$-badge 4 1 :fn nil nil nil)) (equal (apply$-userfn 'sum$+-ac args) (sum$+-ac (car args) (car (cdr args)) (car (cdr (cdr args))) (car (cdr (cdr (cdr args))))))))) (not (apply$-warrant-sum$+-ac))))
Theorem:
(defthm apply$-sum$+-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 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$-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 apply$-warrant-sum$+-necc (implies (not (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'sum$+) '(apply$-badge 3 1 :fn nil nil)) (equal (apply$-userfn 'sum$+ args) (sum$+ (car args) (car (cdr args)) (car (cdr (cdr args)))))))) (not (apply$-warrant-sum$+))))
Theorem:
(defthm apply$-sum$+ (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 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$-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 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$-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 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$-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 apply$-warrant-always$+-necc (implies (not (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'always$+) '(apply$-badge 3 1 :fn nil nil)) (equal (apply$-userfn 'always$+ args) (always$+ (car args) (car (cdr args)) (car (cdr (cdr args)))))))) (not (apply$-warrant-always$+))))
Theorem:
(defthm apply$-always$+ (and (implies (force (apply$-warrant-always$+)) (equal (badge 'always$+) '(apply$-badge 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 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$-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 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$-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 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$-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 apply$-warrant-thereis$+-necc (implies (not (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'thereis$+) '(apply$-badge 3 1 :fn nil nil)) (equal (apply$-userfn 'thereis$+ args) (thereis$+ (car args) (car (cdr args)) (car (cdr (cdr args)))))))) (not (apply$-warrant-thereis$+))))
Theorem:
(defthm apply$-thereis$+ (and (implies (force (apply$-warrant-thereis$+)) (equal (badge 'thereis$+) '(apply$-badge 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 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$-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 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$-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 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$-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 apply$-warrant-collect$-necc (implies (not (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'collect$) '(apply$-badge 2 1 :fn nil)) (equal (apply$-userfn 'collect$ args) (collect$ (car args) (car (cdr args))))))) (not (apply$-warrant-collect$))))
Theorem:
(defthm apply$-collect$ (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 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$-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 apply$-warrant-collect$+-ac-necc (implies (not (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'collect$+-ac) '(apply$-badge 4 1 :fn nil nil nil)) (equal (apply$-userfn 'collect$+-ac args) (collect$+-ac (car args) (car (cdr args)) (car (cdr (cdr args))) (car (cdr (cdr (cdr args))))))))) (not (apply$-warrant-collect$+-ac))))
Theorem:
(defthm apply$-collect$+-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 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$-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 apply$-warrant-collect$+-necc (implies (not (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'collect$+) '(apply$-badge 3 1 :fn nil nil)) (equal (apply$-userfn 'collect$+ args) (collect$+ (car args) (car (cdr args)) (car (cdr (cdr args)))))))) (not (apply$-warrant-collect$+))))
Theorem:
(defthm apply$-collect$+ (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 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$-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 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$-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 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$-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 apply$-warrant-append$-necc (implies (not (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'append$) '(apply$-badge 2 1 :fn nil)) (equal (apply$-userfn 'append$ args) (append$ (car args) (car (cdr args))))))) (not (apply$-warrant-append$))))
Theorem:
(defthm apply$-append$ (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 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$-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 apply$-warrant-append$+-ac-necc (implies (not (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'append$+-ac) '(apply$-badge 4 1 :fn nil nil nil)) (equal (apply$-userfn 'append$+-ac args) (append$+-ac (car args) (car (cdr args)) (car (cdr (cdr args))) (car (cdr (cdr (cdr args))))))))) (not (apply$-warrant-append$+-ac))))
Theorem:
(defthm apply$-append$+-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 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$-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 apply$-warrant-append$+-necc (implies (not (implies (tamep-functionp (car args)) (and (equal (badge-userfn 'append$+) '(apply$-badge 3 1 :fn nil nil)) (equal (apply$-userfn 'append$+ args) (append$+ (car args) (car (cdr args)) (car (cdr (cdr args)))))))) (not (apply$-warrant-append$+))))
Theorem:
(defthm apply$-append$+ (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 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$-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 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$-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-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$-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$-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-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$-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$-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-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$-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$-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-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$-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$-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-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$-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$-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-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$-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$-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 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 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$-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 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$-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)