Theorems about variable renaming for paths.
If two paths or lists of paths are related by variable renaming, extracting their underlying variables causes no errors. This is what the first two theorems below say.
If two paths or lists of paths are related by variable renaming, so are the underlying variables. This is what the last two theorems below say.
Theorem:
(defthm path-to-var-not-error-when-path-renamevar (implies (not (reserrp (path-renamevar old new ren))) (and (not (reserrp (path-to-var old))) (not (reserrp (path-to-var new))))))
Theorem:
(defthm paths-to-vars-not-error-when-path-list-renamevar (implies (not (reserrp (path-list-renamevar old new ren))) (and (not (reserrp (paths-to-vars old))) (not (reserrp (paths-to-vars new))))))
Theorem:
(defthm var-renamevar-not-error-when-path-renamevar (implies (not (reserrp (path-renamevar old new ren))) (not (reserrp (var-renamevar (path-to-var old) (path-to-var new) ren)))))
Theorem:
(defthm var-list-renamevar-not-error-when-path-list-renamevar (implies (not (reserrp (path-list-renamevar old new ren))) (not (reserrp (var-list-renamevar (paths-to-vars old) (paths-to-vars new) ren)))))