(vl-portdecl-or-blockitem-strip x) → new-x
Function:
(defun vl-portdecl-or-blockitem-strip (x) (declare (xargs :guard (vl-portdecl-or-blockitem-p x))) (let ((__function__ 'vl-portdecl-or-blockitem-strip)) (declare (ignorable __function__)) (let ((x (vl-portdecl-or-blockitem-fix x))) (common-lisp::case (tag x) ((:vl-portdecl) (b* ((x.vl-portdecl (vl-portdecl-strip x))) x.vl-portdecl)) (otherwise (b* ((x.vl-blockitem (vl-blockitem-strip x))) x.vl-blockitem))))))
Theorem:
(defthm vl-portdecl-or-blockitem-p-of-vl-portdecl-or-blockitem-strip (b* ((new-x (vl-portdecl-or-blockitem-strip x))) (vl-portdecl-or-blockitem-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-portdecl-or-blockitem-strip-of-vl-portdecl-or-blockitem-fix-x (equal (vl-portdecl-or-blockitem-strip (vl-portdecl-or-blockitem-fix x)) (vl-portdecl-or-blockitem-strip x)))
Theorem:
(defthm vl-portdecl-or-blockitem-strip-vl-portdecl-or-blockitem-equiv-congruence-on-x (implies (vl-portdecl-or-blockitem-equiv x x-equiv) (equal (vl-portdecl-or-blockitem-strip x) (vl-portdecl-or-blockitem-strip x-equiv))) :rule-classes :congruence)