Check if two lists of paths are related by variable renaming.
(path-list-renamevar old new ren) → _
The two lists must have the same length, and corresponding elements must be related.
Function:
(defun path-list-renamevar (old new ren) (declare (xargs :guard (and (path-listp old) (path-listp new) (renamingp ren)))) (let ((__function__ 'path-list-renamevar)) (declare (ignorable __function__)) (b* (((when (endp old)) (if (endp new) nil (reserrf (list :mismatch-extra-new (path-list-fix new))))) ((when (endp new)) (reserrf (list :mismatch-extra-old (path-list-fix old)))) ((okf &) (path-renamevar (car old) (car new) ren))) (path-list-renamevar (cdr old) (cdr new) ren))))
Theorem:
(defthm reserr-optionp-of-path-list-renamevar (b* ((_ (path-list-renamevar old new ren))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm same-len-when-path-list-renamevar (implies (not (reserrp (path-list-renamevar old new ren))) (equal (len new) (len old))))
Theorem:
(defthm path-list-renamevar-of-path-list-fix-old (equal (path-list-renamevar (path-list-fix old) new ren) (path-list-renamevar old new ren)))
Theorem:
(defthm path-list-renamevar-path-list-equiv-congruence-on-old (implies (path-list-equiv old old-equiv) (equal (path-list-renamevar old new ren) (path-list-renamevar old-equiv new ren))) :rule-classes :congruence)
Theorem:
(defthm path-list-renamevar-of-path-list-fix-new (equal (path-list-renamevar old (path-list-fix new) ren) (path-list-renamevar old new ren)))
Theorem:
(defthm path-list-renamevar-path-list-equiv-congruence-on-new (implies (path-list-equiv new new-equiv) (equal (path-list-renamevar old new ren) (path-list-renamevar old new-equiv ren))) :rule-classes :congruence)
Theorem:
(defthm path-list-renamevar-of-renaming-fix-ren (equal (path-list-renamevar old new (renaming-fix ren)) (path-list-renamevar old new ren)))
Theorem:
(defthm path-list-renamevar-renaming-equiv-congruence-on-ren (implies (renaming-equiv ren ren-equiv) (equal (path-list-renamevar old new ren) (path-list-renamevar old new ren-equiv))) :rule-classes :congruence)