Function:
(defun s4vec-== (x y) (declare (xargs :guard (and (s4vec-p x) (s4vec-p y)))) (let ((__function__ 's4vec-==)) (declare (ignorable __function__)) (s3vec-== (s3vec-fix x) (s3vec-fix y))))
Theorem:
(defthm s4vec-p-of-s4vec-== (b* ((res (s4vec-== x y))) (s4vec-p res)) :rule-classes :rewrite)
Theorem:
(defthm s4vec-==-correct (b* ((?res (s4vec-== x y))) (equal (s4vec->4vec res) (4vec-== (s4vec->4vec x) (s4vec->4vec y)))))
Theorem:
(defthm s4vec-==-of-s4vec-fix-x (equal (s4vec-== (s4vec-fix x) y) (s4vec-== x y)))
Theorem:
(defthm s4vec-==-s4vec-equiv-congruence-on-x (implies (s4vec-equiv x x-equiv) (equal (s4vec-== x y) (s4vec-== x-equiv y))) :rule-classes :congruence)
Theorem:
(defthm s4vec-==-of-s4vec-fix-y (equal (s4vec-== x (s4vec-fix y)) (s4vec-== x y)))
Theorem:
(defthm s4vec-==-s4vec-equiv-congruence-on-y (implies (s4vec-equiv y y-equiv) (equal (s4vec-== x y) (s4vec-== x y-equiv))) :rule-classes :congruence)