Transform a function definition.
Function:
(defun simpadd0-fundef (fundef) (declare (xargs :guard (fundefp fundef))) (declare (xargs :guard (fundef-unambp fundef))) (let ((__function__ 'simpadd0-fundef)) (declare (ignorable __function__)) (b* (((fundef fundef) fundef)) (make-fundef :extension fundef.extension :spec (simpadd0-declspec-list fundef.spec) :declor (simpadd0-declor fundef.declor) :decls (simpadd0-decl-list fundef.decls) :body (simpadd0-stmt fundef.body)))))
Theorem:
(defthm fundefp-of-simpadd0-fundef (b* ((new-fundef (simpadd0-fundef fundef))) (fundefp new-fundef)) :rule-classes :rewrite)
Theorem:
(defthm fundef-unambp-of-simpadd0-fundef (b* ((?new-fundef (simpadd0-fundef fundef))) (fundef-unambp new-fundef)))
Theorem:
(defthm simpadd0-fundef-of-fundef-fix-fundef (equal (simpadd0-fundef (fundef-fix fundef)) (simpadd0-fundef fundef)))
Theorem:
(defthm simpadd0-fundef-fundef-equiv-congruence-on-fundef (implies (c$::fundef-equiv fundef fundef-equiv) (equal (simpadd0-fundef fundef) (simpadd0-fundef fundef-equiv))) :rule-classes :congruence)