|
|
|---|
|
|
|
|---|
Recognizer for BED operators.
(bed-op-p x) → *
We use a simple truth-table based encoding, i.e., each operator is a binary, Boolean connective; it is represented as a four-bit natural, where the bits of the representation are the truth table for the operator.
Function:
(defun bed-op-p (x) (declare (xargs :guard t)) (let ((__function__ 'bed-op-p)) (declare (ignorable __function__)) (unsigned-byte-p 4 x)))
Theorem:
(defthm unsigned-byte-p-when-bed-op-p (implies (bed-op-p x) (unsigned-byte-p 4 x)))
Theorem:
(defthm type-when-bed-op-p (implies (bed-op-p x) (natp x)) :rule-classes :compound-recognizer)