Proof technique: show two lists are equal by showing that their nth elements are always the same.
This is a powerful rule that can be functionally instantiated to
prove that two lists are equal when their
Theorem:
(defthm equal-by-nths (implies (and (equal-by-nths-hyp) (true-listp (equal-by-nths-lhs)) (true-listp (equal-by-nths-rhs))) (equal (equal (equal-by-nths-lhs) (equal-by-nths-rhs)) (equal (len (equal-by-nths-lhs)) (len (equal-by-nths-rhs))))))
Where the
Definition:
(encapsulate (((equal-by-nths-hyp) => *) ((equal-by-nths-lhs) => *) ((equal-by-nths-rhs) => *)) (local (value-triple :elided)) (local (value-triple :elided)) (local (value-triple :elided)) (defthmd equal-by-nths-constraint (implies (and (equal-by-nths-hyp) (natp n) (< n (len (equal-by-nths-lhs)))) (equal (nth n (equal-by-nths-lhs)) (nth n (equal-by-nths-rhs))))))
For some bare-bones automation, see also equal-by-nths-hint.