Add the function names in a list to a function renaming list.
(add-funs-to-fun-renaming old new ren) → new-ren
Function:
(defun add-funs-to-fun-renaming (old new ren) (declare (xargs :guard (and (identifier-listp old) (identifier-listp new) (renamingp ren)))) (let ((__function__ 'add-funs-to-fun-renaming)) (declare (ignorable __function__)) (b* (((when (endp old)) (if (endp new) (renaming-fix ren) (reserrf (list :mismatch-extra-new (identifier-list-fix new))))) ((when (endp new)) (reserrf (list :mismatch-extra-old (identifier-list-fix old)))) ((okf ren) (add-fun-to-fun-renaming (car old) (car new) ren))) (add-funs-to-fun-renaming (cdr old) (cdr new) ren))))
Theorem:
(defthm renaming-resultp-of-add-funs-to-fun-renaming (b* ((new-ren (add-funs-to-fun-renaming old new ren))) (renaming-resultp new-ren)) :rule-classes :rewrite)
Theorem:
(defthm same-len-when-add-funs-to-fun-renaming (implies (not (reserrp (add-funs-to-fun-renaming old new ren))) (equal (len new) (len old))))
Theorem:
(defthm add-funs-to-fun-renaming-of-identifier-list-fix-old (equal (add-funs-to-fun-renaming (identifier-list-fix old) new ren) (add-funs-to-fun-renaming old new ren)))
Theorem:
(defthm add-funs-to-fun-renaming-identifier-list-equiv-congruence-on-old (implies (identifier-list-equiv old old-equiv) (equal (add-funs-to-fun-renaming old new ren) (add-funs-to-fun-renaming old-equiv new ren))) :rule-classes :congruence)
Theorem:
(defthm add-funs-to-fun-renaming-of-identifier-list-fix-new (equal (add-funs-to-fun-renaming old (identifier-list-fix new) ren) (add-funs-to-fun-renaming old new ren)))
Theorem:
(defthm add-funs-to-fun-renaming-identifier-list-equiv-congruence-on-new (implies (identifier-list-equiv new new-equiv) (equal (add-funs-to-fun-renaming old new ren) (add-funs-to-fun-renaming old new-equiv ren))) :rule-classes :congruence)
Theorem:
(defthm add-funs-to-fun-renaming-of-renaming-fix-ren (equal (add-funs-to-fun-renaming old new (renaming-fix ren)) (add-funs-to-fun-renaming old new ren)))
Theorem:
(defthm add-funs-to-fun-renaming-renaming-equiv-congruence-on-ren (implies (renaming-equiv ren ren-equiv) (equal (add-funs-to-fun-renaming old new ren) (add-funs-to-fun-renaming old new ren-equiv))) :rule-classes :congruence)