Coerces an arbitrary 4vec to a 2vecx, by forcing any non-2vecs to an just be infinite Xes.
(2vecx-fix x) → x-fix
Function:
(defun 2vecx-fix$inline (x) (declare (xargs :guard (4vec-p x))) (let ((__function__ '2vecx-fix)) (declare (ignorable __function__)) (if (2vec-p x) (4vec-fix x) (4vec-x))))
Theorem:
(defthm 2vecx-p!-of-2vecx-fix (b* ((x-fix (2vecx-fix$inline x))) (2vecx-p! x-fix)) :rule-classes :rewrite)
Theorem:
(defthm 2vecx-fix-of-2vecx-p (implies (2vecx-p x) (equal (2vecx-fix x) (4vec-fix x))))
Theorem:
(defthm 2vecx-fix$inline-of-3vec-fix-x (equal (2vecx-fix$inline (3vec-fix x)) (2vecx-fix$inline x)))
Theorem:
(defthm 2vecx-fix$inline-3vec-equiv-congruence-on-x (implies (3vec-equiv x x-equiv) (equal (2vecx-fix$inline x) (2vecx-fix$inline x-equiv))) :rule-classes :congruence)