Theorems about function tables and related concepts for code related by variable renaming.
If two function definitions are related by variable renaming, their correpsonding function types are the same, because they do not depend on variables.
Consequently, if two lists of function definitions are related by variable renaming, their corresponding function tables are the same.
That implies that add-funtypes yields the same result, starting with the same function table, for lists of function definitions related by variable renaming.
Theorem:
(defthm same-funtype-for-fundef-when-fundef-renamevar (implies (not (reserrp (fundef-renamevar old new))) (equal (funtype-for-fundef new) (funtype-for-fundef old))))
Theorem:
(defthm same-funtable-for-fundefs-when-fundef-list-renamevar (implies (and (not (reserrp (fundef-list-renamevar old new))) (not (reserrp (funtable-for-fundefs old)))) (equal (funtable-for-fundefs new) (funtable-for-fundefs old))))
Theorem:
(defthm same-add-funtypes-when-fundef-list-renamevar (implies (and (not (reserrp (fundef-list-renamevar old new))) (not (reserrp (add-funtypes old funtab)))) (equal (add-funtypes new funtab) (add-funtypes old funtab))))