		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucidocclist-drop-initials/finals

Remove all occurrences that are from initial statements.

Signature
(vl-lucidocclist-drop-initials/finals x) → new-x
Arguments: x — Guard (vl-lucidocclist-p x).
Returns: new-x — Type (vl-lucidocclist-p new-x).

Definitions and Theorems

Function: vl-lucidocclist-drop-initials/finals

(defun vl-lucidocclist-drop-initials/finals (x)
  (declare (xargs :guard (vl-lucidocclist-p x)))
  (let ((__function__ 'vl-lucidocclist-drop-initials/finals))
    (declare (ignorable __function__))
    (b* (((when (atom x)) nil)
         (elem (vl-lucidctx->elem (vl-lucidocc->ctx (car x))))
         (initial-p (mbe :logic (vl-initial-p elem)
                         :exec (eq (tag elem) :vl-initial)))
         (final-p (mbe :logic (vl-final-p elem)
                       :exec (eq (tag elem) :vl-final)))
         ((when (or initial-p final-p))
          (vl-lucidocclist-drop-initials/finals (cdr x))))
      (cons (vl-lucidocc-fix (car x))
            (vl-lucidocclist-drop-initials/finals (cdr x))))))

Theorem: vl-lucidocclist-p-of-vl-lucidocclist-drop-initials/finals

(defthm vl-lucidocclist-p-of-vl-lucidocclist-drop-initials/finals
  (b* ((new-x (vl-lucidocclist-drop-initials/finals x)))
    (vl-lucidocclist-p new-x))
  :rule-classes :rewrite)

Theorem: vl-lucidocclist-drop-initials/finals-of-vl-lucidocclist-fix-x

(defthm
      vl-lucidocclist-drop-initials/finals-of-vl-lucidocclist-fix-x
 (equal
      (vl-lucidocclist-drop-initials/finals (vl-lucidocclist-fix x))
      (vl-lucidocclist-drop-initials/finals x)))

Theorem: vl-lucidocclist-drop-initials/finals-vl-lucidocclist-equiv-congruence-on-x

(defthm
 vl-lucidocclist-drop-initials/finals-vl-lucidocclist-equiv-congruence-on-x
 (implies (vl-lucidocclist-equiv x x-equiv)
          (equal (vl-lucidocclist-drop-initials/finals x)
                 (vl-lucidocclist-drop-initials/finals x-equiv)))
 :rule-classes :congruence)