		Search-engine friendly clone of the ACL2 documentation.

Lhprobe/4vec-p

Lhprobe/4vec-kind

Kind function for lhprobe/4vec type

Signature
(lhprobe/4vec-kind x) → kind
Arguments: x — Guard (lhprobe/4vec-p x).
Returns: kind — Type (and (symbolp kind) (not (booleanp kind))).

Definitions and Theorems

Function: lhprobe/4vec-kind

(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: return-type-of-lhprobe/4vec-kind

(defthm return-type-of-lhprobe/4vec-kind
  (b* ((kind (lhprobe/4vec-kind x)))
    (and (symbolp kind)
         (not (booleanp kind))))
  :rule-classes :type-prescription)

Theorem: lhprobe/4vec-kind-possibilities

(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: lhprobe/4vec-p-when-when-kind-is-4vec

(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: lhprobe/4vec-p-when-when-kind-is-lhprobe

(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: lhprobe/4vec-kind-when-lhprobe-p

(defthm lhprobe/4vec-kind-when-lhprobe-p
  (implies (lhprobe-p x)
           (equal (lhprobe/4vec-kind x) :lhprobe)))

Theorem: lhprobe/4vec-kind-when-4vec-p

(defthm lhprobe/4vec-kind-when-4vec-p
  (implies (4vec-p x)
           (equal (lhprobe/4vec-kind x) :4vec)))