# Equal-by-nths

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 nth elements are always the
same. The theorem to instantiate is:

**Theorem: **equal-by-nths

(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 hyp, lhs, and rhs must satisfy the encapsulated
constraint, essentially that the nth element of lhs is always the
same as the nth element of rhs when the hyp is satisfied:

**Definition: **equal-by-nths-hyp

(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.

### Subtopics

- Equal-by-nths-hint
- A computed-hint that automates basic applications of equal-by-nths.