Get the orig field from a sd-key.
This is an ordinary field accessor created by defprod.
Function:
(defun sd-key->orig$inline (x) (declare (xargs :guard (sd-key-p x))) (declare (xargs :guard t)) (let ((__function__ 'sd-key->orig)) (declare (ignorable __function__)) (mbe :logic (b* ((x (and t x))) (str-fix (cdr (cdr (cdr x))))) :exec (cdr (cdr (cdr x))))))
Theorem:
(defthm stringp-of-sd-key->orig (b* ((orig (sd-key->orig$inline x))) (stringp orig)) :rule-classes :type-prescription)
Theorem:
(defthm sd-key->orig$inline-of-sd-key-fix-x (equal (sd-key->orig$inline (sd-key-fix x)) (sd-key->orig$inline x)))
Theorem:
(defthm sd-key->orig$inline-sd-key-equiv-congruence-on-x (implies (sd-key-equiv x x-equiv) (equal (sd-key->orig$inline x) (sd-key->orig$inline x-equiv))) :rule-classes :congruence)