(vl-lucidocc->ss x) → ss
Function:
(defun vl-lucidocc->ss$inline (x) (declare (xargs :guard (vl-lucidocc-p x))) (let ((__function__ 'vl-lucidocc->ss)) (declare (ignorable __function__)) (vl-lucidocc-case x :solo x.ss :slice x.ss :tail x.ss)))
Theorem:
(defthm vl-scopestack-p-of-vl-lucidocc->ss (b* ((ss (vl-lucidocc->ss$inline x))) (vl-scopestack-p ss)) :rule-classes :rewrite)
Theorem:
(defthm vl-lucidocc->ss$inline-of-vl-lucidocc-fix-x (equal (vl-lucidocc->ss$inline (vl-lucidocc-fix x)) (vl-lucidocc->ss$inline x)))
Theorem:
(defthm vl-lucidocc->ss$inline-vl-lucidocc-equiv-congruence-on-x (implies (vl-lucidocc-equiv x x-equiv) (equal (vl-lucidocc->ss$inline x) (vl-lucidocc->ss$inline x-equiv))) :rule-classes :congruence)