(vl-dimensionlist-compare-sizes a b) → *
Function:
(defun vl-dimensionlist-compare-sizes (a b) (declare (xargs :guard (and (vl-dimensionlist-p a) (vl-dimensionlist-p b)))) (let ((__function__ 'vl-dimensionlist-compare-sizes)) (declare (ignorable __function__)) (if (atom a) (atom b) (and (consp b) (vl-dimension-compare-sizes (car a) (car b)) (vl-dimensionlist-compare-sizes (cdr a) (cdr b))))))
Theorem:
(defthm vl-dimensionlist-compare-sizes-of-vl-dimensionlist-fix-a (equal (vl-dimensionlist-compare-sizes (vl-dimensionlist-fix a) b) (vl-dimensionlist-compare-sizes a b)))
Theorem:
(defthm vl-dimensionlist-compare-sizes-vl-dimensionlist-equiv-congruence-on-a (implies (vl-dimensionlist-equiv a a-equiv) (equal (vl-dimensionlist-compare-sizes a b) (vl-dimensionlist-compare-sizes a-equiv b))) :rule-classes :congruence)
Theorem:
(defthm vl-dimensionlist-compare-sizes-of-vl-dimensionlist-fix-b (equal (vl-dimensionlist-compare-sizes a (vl-dimensionlist-fix b)) (vl-dimensionlist-compare-sizes a b)))
Theorem:
(defthm vl-dimensionlist-compare-sizes-vl-dimensionlist-equiv-congruence-on-b (implies (vl-dimensionlist-equiv b b-equiv) (equal (vl-dimensionlist-compare-sizes a b) (vl-dimensionlist-compare-sizes a b-equiv))) :rule-classes :congruence)