		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-first-solo-occ

Signature
(vl-lucid-first-solo-occ x) → occ?
Arguments: x — Guard (vl-lucidocclist-p x).
Returns: occ? — Type (and (iff (vl-lucidocc-p occ?) (vl-lucid-some-solo-occp x)) (iff occ? (vl-lucid-some-solo-occp x))) .

Definitions and Theorems

Function: vl-lucid-first-solo-occ

(defun vl-lucid-first-solo-occ (x)
  (declare (xargs :guard (vl-lucidocclist-p x)))
  (let ((__function__ 'vl-lucid-first-solo-occ))
    (declare (ignorable __function__))
    (cond ((atom x) nil)
          ((eq (vl-lucidocc-kind (car x)) :solo)
           (vl-lucidocc-fix (car x)))
          (t (vl-lucid-first-solo-occ (cdr x))))))

Theorem: return-type-of-vl-lucid-first-solo-occ

(defthm return-type-of-vl-lucid-first-solo-occ
  (b* ((occ? (vl-lucid-first-solo-occ x)))
    (and (iff (vl-lucidocc-p occ?)
              (vl-lucid-some-solo-occp x))
         (iff occ? (vl-lucid-some-solo-occp x))))
  :rule-classes :rewrite)

Theorem: vl-lucid-first-solo-occ-of-vl-lucidocclist-fix-x

(defthm vl-lucid-first-solo-occ-of-vl-lucidocclist-fix-x
  (equal (vl-lucid-first-solo-occ (vl-lucidocclist-fix x))
         (vl-lucid-first-solo-occ x)))

Theorem: vl-lucid-first-solo-occ-vl-lucidocclist-equiv-congruence-on-x

(defthm
      vl-lucid-first-solo-occ-vl-lucidocclist-equiv-congruence-on-x
  (implies (vl-lucidocclist-equiv x x-equiv)
           (equal (vl-lucid-first-solo-occ x)
                  (vl-lucid-first-solo-occ x-equiv)))
  :rule-classes :congruence)