(vl-dimension-compare-sizes a b) → *
Function:
(defun vl-dimension-compare-sizes (a b) (declare (xargs :guard (and (vl-dimension-p a) (vl-dimension-p b)))) (let ((__function__ 'vl-dimension-compare-sizes)) (declare (ignorable __function__)) (vl-dimension-case a :unsized (vl-dimension-case b :unsized) :range (vl-dimension-case b :range (and (vl-range-resolved-p a.range) (vl-range-resolved-p b.range) (equal (vl-range-size a.range) (vl-range-size b.range))) :otherwise nil) :datatype nil :star nil :queue nil)))
Theorem:
(defthm vl-dimension-compare-sizes-of-vl-dimension-fix-a (equal (vl-dimension-compare-sizes (vl-dimension-fix a) b) (vl-dimension-compare-sizes a b)))
Theorem:
(defthm vl-dimension-compare-sizes-vl-dimension-equiv-congruence-on-a (implies (vl-dimension-equiv a a-equiv) (equal (vl-dimension-compare-sizes a b) (vl-dimension-compare-sizes a-equiv b))) :rule-classes :congruence)
Theorem:
(defthm vl-dimension-compare-sizes-of-vl-dimension-fix-b (equal (vl-dimension-compare-sizes a (vl-dimension-fix b)) (vl-dimension-compare-sizes a b)))
Theorem:
(defthm vl-dimension-compare-sizes-vl-dimension-equiv-congruence-on-b (implies (vl-dimension-equiv b b-equiv) (equal (vl-dimension-compare-sizes a b) (vl-dimension-compare-sizes a b-equiv))) :rule-classes :congruence)