Kind function for lhprobe/4vec type
(lhprobe/4vec-kind x) → kind
Function:
(defun lhprobe/4vec-kind (x) (declare (xargs :guard (lhprobe/4vec-p x))) (let ((__function__ 'lhprobe/4vec-kind)) (declare (ignorable __function__)) (if (or (atom x) (integerp (car x))) :4vec :lhprobe)))
Theorem:
(defthm return-type-of-lhprobe/4vec-kind (b* ((kind (lhprobe/4vec-kind x))) (and (symbolp kind) (not (booleanp kind)))) :rule-classes :type-prescription)
Theorem:
(defthm lhprobe/4vec-kind-possibilities (or (equal (lhprobe/4vec-kind x) :4vec) (equal (lhprobe/4vec-kind x) :lhprobe)) :rule-classes ((:forward-chaining :trigger-terms ((lhprobe/4vec-kind x)))))
Theorem:
(defthm lhprobe/4vec-p-when-when-kind-is-4vec (implies (equal (lhprobe/4vec-kind x) :4vec) (equal (lhprobe/4vec-p x) (4vec-p x))))
Theorem:
(defthm lhprobe/4vec-p-when-when-kind-is-lhprobe (implies (equal (lhprobe/4vec-kind x) :lhprobe) (equal (lhprobe/4vec-p x) (lhprobe-p x))))
Theorem:
(defthm lhprobe/4vec-kind-when-lhprobe-p (implies (lhprobe-p x) (equal (lhprobe/4vec-kind x) :lhprobe)))
Theorem:
(defthm lhprobe/4vec-kind-when-4vec-p (implies (4vec-p x) (equal (lhprobe/4vec-kind x) :4vec)))