		Search-engine friendly clone of the ACL2 documentation.

Lhatom-var

Lhatom-var->rsh

Get the rsh field from a lhatom-var.

Signature
(lhatom-var->rsh x) → rsh
Arguments: x — Guard (lhatom-p x).
Returns: rsh — Type (natp rsh).

This is an ordinary field accessor created by defprod.

Definitions and Theorems

Function: lhatom-var->rsh$inline

(defun lhatom-var->rsh$inline (x)
  (declare (xargs :guard (lhatom-p x)))
  (declare (xargs :guard (equal (lhatom-kind x) :var)))
  (let ((__function__ 'lhatom-var->rsh))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((x (and (equal (lhatom-kind x) :var) x)))
           (nfix (if (or (atom x)
                         (and (eq (car x) :var) (consp (cdr x))))
                     0
                   (cdr x))))
         :exec
         (if (or (atom x)
                 (and (eq (car x) :var) (consp (cdr x))))
             0
           (cdr x)))))

Theorem: natp-of-lhatom-var->rsh

(defthm natp-of-lhatom-var->rsh
  (b* ((rsh (lhatom-var->rsh$inline x)))
    (natp rsh))
  :rule-classes (:rewrite :type-prescription))

Theorem: lhatom-var->rsh$inline-of-lhatom-fix-x

(defthm lhatom-var->rsh$inline-of-lhatom-fix-x
  (equal (lhatom-var->rsh$inline (lhatom-fix x))
         (lhatom-var->rsh$inline x)))

Theorem: lhatom-var->rsh$inline-lhatom-equiv-congruence-on-x

(defthm lhatom-var->rsh$inline-lhatom-equiv-congruence-on-x
  (implies (lhatom-equiv x x-equiv)
           (equal (lhatom-var->rsh$inline x)
                  (lhatom-var->rsh$inline x-equiv)))
  :rule-classes :congruence)

Theorem: lhatom-var->rsh-when-wrong-kind

(defthm lhatom-var->rsh-when-wrong-kind
  (implies (not (equal (lhatom-kind x) :var))
           (equal (lhatom-var->rsh x) (nfix nil))))