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 7 1 :fn nil :fn :fn nil nil nil)) (equal (apply$-userfn 'do$ args) (do$ (car args) (car (cdr args)) (car (cdr (cdr args))) (car (cdr (cdr (cdr args)))) (car (cdr (cdr (cdr (cdr args))))) (car (cdr (cdr (cdr (cdr (cdr args)))))) (car (cdr (cdr (cdr (cdr (cdr (cdr args))))))))))))) :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 7 1 :fn nil :fn :fn nil nil nil)) (equal (apply$-userfn 'do$ args) (do$ (car args) (car (cdr args)) (car (cdr (cdr args))) (car (cdr (cdr (cdr args)))) (car (cdr (cdr (cdr (cdr args))))) (car (cdr (cdr (cdr (cdr (cdr args)))))) (car (cdr (cdr (cdr (cdr (cdr (cdr args)))))))))))) (not (apply$-warrant-do$))))
Theorem:
(defthm apply$-do$ (and (implies (force (apply$-warrant-do$)) (equal (badge 'do$) '(apply$-badge 7 1 :fn nil :fn :fn nil nil nil))) (implies (and (force (apply$-warrant-do$)) (and (tamep-functionp (car args)) (tamep-functionp (car (cdr (cdr args)))) (tamep-functionp (car (cdr (cdr (cdr args))))))) (equal (apply$ 'do$ args) (do$ (car args) (car (cdr args)) (car (cdr (cdr args))) (car (cdr (cdr (cdr args)))) (car (cdr (cdr (cdr (cdr args))))) (car (cdr (cdr (cdr (cdr (cdr args)))))) (car (cdr (cdr (cdr (cdr (cdr (cdr args))))))))))))
Theorem:
(defthm fn-equal-implies-equal-do$-1 (implies (fn-equal measure-fn measure-fn-equiv) (equal (do$ measure-fn alist do-fn finally-fn values untrans-measure untrans-do-loop$) (do$ measure-fn-equiv alist do-fn finally-fn values untrans-measure untrans-do-loop$))) :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 untrans-measure untrans-do-loop$) (do$ measure-fn alist do-fn-equiv finally-fn values untrans-measure untrans-do-loop$))) :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 untrans-measure untrans-do-loop$) (do$ measure-fn alist do-fn finally-fn-equiv values untrans-measure untrans-do-loop$))) :rule-classes (:congruence))
Theorem:
(defthm apply$-eviscerate-do$-alist (implies (force (apply$-warrant-eviscerate-do$-alist)) (and (equal (badge 'eviscerate-do$-alist) '(apply$-badge 1 1 . t)) (equal (apply$ 'eviscerate-do$-alist args) (eviscerate-do$-alist (car args))))))
Theorem:
(defthm apply$-warrant-eviscerate-do$-alist-necc (implies (not (and (equal (badge-userfn 'eviscerate-do$-alist) '(apply$-badge 1 1 . t)) (equal (apply$-userfn 'eviscerate-do$-alist args) (eviscerate-do$-alist (car args))))) (not (apply$-warrant-eviscerate-do$-alist))))
Theorem:
(defthm apply$-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 1 1 . t)) (equal (apply$-userfn 'eviscerate-do$-alist args) (eviscerate-do$-alist (car 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)