Remove all occurrences that are from
(vl-lucidocclist-drop-initials x) → new-x
Function:
(defun vl-lucidocclist-drop-initials (x) (declare (xargs :guard (vl-lucidocclist-p x))) (let ((__function__ 'vl-lucidocclist-drop-initials)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) (elem (vl-context1->elem (vl-lucidocc->ctx (car x)))) (initial-p (mbe :logic (vl-initial-p elem) :exec (eq (tag elem) :vl-initial))) ((when initial-p) (vl-lucidocclist-drop-initials (cdr x)))) (cons (vl-lucidocc-fix (car x)) (vl-lucidocclist-drop-initials (cdr x))))))
Theorem:
(defthm vl-lucidocclist-p-of-vl-lucidocclist-drop-initials (b* ((new-x (vl-lucidocclist-drop-initials x))) (vl-lucidocclist-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-lucidocclist-drop-initials-of-vl-lucidocclist-fix-x (equal (vl-lucidocclist-drop-initials (vl-lucidocclist-fix x)) (vl-lucidocclist-drop-initials x)))
Theorem:
(defthm vl-lucidocclist-drop-initials-vl-lucidocclist-equiv-congruence-on-x (implies (vl-lucidocclist-equiv x x-equiv) (equal (vl-lucidocclist-drop-initials x) (vl-lucidocclist-drop-initials x-equiv))) :rule-classes :congruence)