Construct a list of equalities between two lists of expressions, element-wise.
(equate-expression-lists lefts rights) → equalities
Function:
(defun equate-expression-lists (lefts rights) (declare (xargs :guard (and (expression-listp lefts) (expression-listp rights)))) (declare (xargs :guard (= (len lefts) (len rights)))) (let ((__function__ 'equate-expression-lists)) (declare (ignorable __function__)) (cond ((endp lefts) nil) (t (cons (equate-expressions (car lefts) (car rights)) (equate-expression-lists (cdr lefts) (cdr rights)))))))
Theorem:
(defthm expression-listp-of-equate-expression-lists (b* ((equalities (equate-expression-lists lefts rights))) (expression-listp equalities)) :rule-classes :rewrite)
Theorem:
(defthm equate-expression-lists-of-expression-list-fix-lefts (equal (equate-expression-lists (expression-list-fix lefts) rights) (equate-expression-lists lefts rights)))
Theorem:
(defthm equate-expression-lists-expression-list-equiv-congruence-on-lefts (implies (expression-list-equiv lefts lefts-equiv) (equal (equate-expression-lists lefts rights) (equate-expression-lists lefts-equiv rights))) :rule-classes :congruence)
Theorem:
(defthm equate-expression-lists-of-expression-list-fix-rights (equal (equate-expression-lists lefts (expression-list-fix rights)) (equate-expression-lists lefts rights)))
Theorem:
(defthm equate-expression-lists-expression-list-equiv-congruence-on-rights (implies (expression-list-equiv rights rights-equiv) (equal (equate-expression-lists lefts rights) (equate-expression-lists lefts rights-equiv))) :rule-classes :congruence)